revision_history.txt

2006.09.13  Version 0.04
2006.11.01  Version 0.04.2
2006.12.20  Version 0.10     initial public release

2006.12.20  Version 0.10.1  
- include missing HOL file ottDefine.sml

2006.12.22  Version 0.10.2  
- include missing ottmode.el

2007.01.19  Version 0.10.3   
- bugfixes
- new examples: various TAPL fragments, and an OCaml fragment with
   concurrency (peterson_caml.ott)
- generation of OCaml code for type definitions and generated
   functions (substitution etc)
- merge option to merge ott source files
- improved HOL support infrastructure

2007.01.24  Version 0.10.4
- bugfix: allow "-" in bindspec lexing
  
2007.02.07  Version 0.10.5
- various bugfixes (mostly w.r.t. Coq list support)
- various improvements to examples
- document generation of OCaml code
- (breaking) source syntax changes: keyword "rules" is now replaced by
   "grammar", and hom "caml" is replaced by "ocaml"

2007.04.06  Version 0.10.6
- fixes and additional examples

2007.07.18  Version 0.10.7
- bug fixes

2007.08.13  Version 0.10.8
- rename module Aux to Auxl, to work around a Windows problem

2007.08.28  Version 0.10.9
- add Windows binary-only release

2007.09.04  Version 0.10.10
- new manual, in browsable html, pdf and postscript
- new tex style for typesetting rules (in the tex/ directory)
- move emacs mode and hol auxiliaries into new emacs/ and hol/ directories

2007.09.28  Version 0.10.11
- fix bug in Windows version: properly open files in binary mode when writesys and readsys

2007.10.05  Version 0.10.12
- add missing file from Coq proof support: ott_list_eq_dec.v

2007.10.18  Version 0.10.13
- new (experimental!) switch -picky_multiple_parses <true>,     
   to allow multiple parses if the generated code is
   identical - at present only for filtered LaTeX
- some source documentation
 
2008.02.15  Version 0.10.14
- new parser, with better performance and better support for disambiguation
   (see Section 14 "Parsing Priorities" in the manual, and changes to 
   Section 20 "Reference: The language of symbolic terms")
- new support for context grammars, with automatically generated
   hole-filling functions (see Section 13 "Context rules" in the manual)
- new syntactic sugar flavour of metaproductions: writing "S" instead
   of "M" gives metaproductions that can be used in concrete terms
- various bugfixes

2008.12.16  Version 0.10.15
- support for Isabelle 2008 (Isabelle 2005 syntax no longer produced)
- new option -isabelle_primrec <true> : if set to false then ott
   generates "fun"s instead of "primrec"s  (though Isabelle can only
   sometimes automatically prove termination of these "fun"s).
- new declaration "phantom" to turn off type generation for metavariables.

2009.3.9  Version 0.10.16
- release of the experimental Coq locally-nameless backend
- aesthetic improvements of the Coq output
- -show-post-sort and -show-defns are now <false> by default to make
    output less noisy

2009.7.19 Version 0.10.17

- fix ocamlvar hom bug
- fix bug in Coq backend when dealing with some kinds of dot forms
- suppress printing of number of good/bad definition rules if 
   there are no rules
- change -tex_show_meta false behaviour to not suppress sugar
   productions
- add % at line ends in rules, to prevent extra spaces (per BCP patch)
- remove doc references to the Windows binary distribution.  It should
   be easy to build from source, but we don't have access to a
   suitable machine.


2010.3.24 Version 0.10.18alpha

- The previous command-line options -coq, -hol, etc., are no longer
  supported; they should be replaced by -o. 

- By default (unless -merge true is set) the order of the input file 
  is preserved, so one can have mixed sequences of definitions of
  grammar, of inductive relations, and of embed blocks.

- New command-line options -i <filename> and -o <filename> for
  specifying multiple input and output files.  Input files with
  non-.ott extensions (.v, .thy, .sml, .ml, .tex) are copied verbatim
  into the respective outputs.  The command-line order of these
  options is significant:  the prover output can be split into
  multiple output files; each prover output file specified with -o
  will contain the material from the previous input files specified
  with -i (since the last -o for this prover).

- Better tex default spacing, distinguishing alphabetic and other
  ("symbolic") terminals based on their ott source strings and
  wrapping them in \ottkw{} and \ottsym{} respectively. 

- Support for in-line prover code in premises, e.g.

   {{ prover code mentioning [[x]] and [[\y.z]] }}
   -----------------------------------------------  ::  rulename
   conclusion

- The {{ phantom }} hom can now be applied to metavariables and to
  nonterminal rules.  In both cases it suppresses generation of a prover
  or OCaml definition, but any type homs are taken into account when
  the metavariable or nonterminal root is output as a type. 

- There is a new hom {{ order ... }} that can be applied to
  productions which lets one specify the order of arguments of a
  prover or OCaml constructor independently of the order in which they
  appear in the production.  For example, one might say:

     | e1 e2   :: :: ReversedApp {{ order [[e2]] [[e1]] }}

- There is a new hom {{ coq-universe UniverseName }} that can be
  applied to metavariable or nonterminal rules, eg to force Ott to
  generate definitions in Type instead of in Set. 

- Changed some debug options (eg show-pre-sort)

- Ocaml list homs on productions are now permitted 

- add coq_lngen option for compatibility with the lngen tool

- Bug fixes:
   - problem with comment line in defns terminated with EOF [Jianzhou Zhao]
   - freshness of identifier in Ott generated functions [Jianzhou Zhao]
   - processing of parse tree for some cases of dot forms [Scott Owens]
   - processing of picky_multiple_parses [Scott Owens]
   - added some error checks
   - several fixes in the Coq locally-nameless backend [Stephanie Weirich]
   - performance issue when using contextrules [Nicolas Pouillard]
   - parens in OCaml substitutions for multiple binders [Vilhelm Sjoberg]


2010.03.29 Version 0.20

- The order among mutually recursive nonterminal definitions in
  grammar blocks is now preserved in prover output. 

2010.04.04 Version 0.20.1

- Support coq-universe hom on blocks of definitions, eg:

    defns
    Jop :: '' ::= {{ coq-universe Type }}

     defn
     t1 --> t2 :: ::reduce::'' by


        --------------------------  :: ax_app
        (\x.t1) v2 -->  {v2/x}t1


2010.06.29

- refactor the generated latex for grammars so that condensed grammars
  can be produced by redefining a couple of latex commands, eg

    \renewcommand{\ottgrammartabular}[1]{{\raggedright #1}}
    \renewcommand{\ottrulehead}[3]{$#1$  $#2$ }
    \renewcommand{\ottprodline}[6]{{}\ ${}#1$\mbox{\ {}$#2$}{}}
    \renewcommand{\ottfirstprodline}[6]{{}\ ${}$\mbox{\ {}$#2$}{}}
    \renewcommand{\ottprodnewline}{}
    \renewcommand{\ottinterrule}{\\[1mm]} 

- add experimental option (-ocaml_include_terminals true) to include, in
   generated OCaml types, an instance of "terminal" in all the places
   where there's a terminal in the AST

- gforge bugtracker now in use:https://gforge.inria.fr/tracker/?group_id=2980

2010.11.28 Version 0.20.3

- fixes to bugs: 

    11367 coq-universe Type problem with non-native lists
    11368 generation of induction principles in Ott 0.20
    11369 0 and O in generated Ott lists
    11377 {{}} hypothesis and ln backend
    11378 context rules and ln backend

- (feature request 11373) Support for explicit naming of premises in
   inductive rules for the Coq backend.  For instance, adding the
   [[:RED]] annotation below

   t1 --> t1' [[:RED]] 
   -------------------- :: ctx_app_arg
   v t1 --> v t1'

   results in:

   | ctx_app_arg : forall (v t1 t1':term)
      (RED: reduce t1 t1'),
      is_val_of_term v ->
      reduce (t_app v t1) (t_app v t1').

   Names of rules cannot contain spaces or other non alpha-numerical
   characters, and must begin with a letter. The name annotation must
   at the rightmost place on the hypothesis line, and must be enclosed
   (without spaces) between the [[: and ]] parentheses.

- (feature request 11372) The Coq backend now tries to preserve the
   names the user specified in the definition of grammar rules.  For
   instance the grammar definition below

     grammar 
     term, t :: 't_' ::=                               
       | x            ::  :: Var                  
       | \ x . t      ::  :: Lam     (+ bind x in t +)
       | t t'         ::  :: App                  
       | ( t )        :: S:: Paren   {{ icho [[t]]  }} 
       | { t / x } t' :: M:: Tsub    {{ icho (tsubst_t [[t]] [[x]] [[t']])}}

   generates

     Inductive term : Set := 
      | t_var (x:var)
      | t_lam (x:var) (t:term)
      | t_app (t:term) (t':term).

   instead of 

     Inductive term : Set := 
      | t_var : var -> term
      | t_lam : var -> term -> term
      | t_app : term -> term -> term.

   The old behaviour can be obtained via the top-level option
   -coq_names_in_rules false.

2011.11.17 Version 0.21

- Bump ocamlgraph version to 1.7, to avoid compilation issues with
  OCaml 3.12.1.

- Ported the Isabelle backend to Isabelle2011 (*).

- Experimental support for function definitions.  As a simple example,
  in the Ott file below:

    grammar
     n :: 'n_' ::= 
       | 0       :: :: Zero
       | S n     :: :: Succ

    funs
      Add ::=  {{ hol-proof ... }}
    fun
      n1 + n2 :: n :: add {{ com a function of type num \to num \to num }} 
    by
      0 + n2 === n2
      S n1 + n2 === n1 + S n2

  the add function is compiled into the following coq code:

    Fixpoint add (x1:num) (x2:num) : num:=
      match x1,x2 with
      | n_zero , n2 => n2
      | (n_succ n1) , n2 =>  (add n1 (n_succ n2) ) 
    end.

  The "fun n1 + n2 :: n :: add by" declaration specifies:

  - the name of the function: add
  - the symbolic term that defines the lhs: n1 + n2
  - the symbolic term that defines the rhs: n

  The type of the arguments of the function is defined by the
  non-terminals appearing in the lhs, the return type by the rhs
  non-terminal (so num -> num -> num in the above example).  Functions
  are then defined by case analysis, where the lhs and the rhs are
  separated by the reserved symbol "===".

  The {{ hol-proof }} hom allows the specification of a termination
  proof.

- A new option -fast_parse <bool> generates a faster parser but
  removes the possibility of disambiguating ambiguous terms using the
  :non_terminal: syntax.

- The generated Coq substitution functions now use the list_minus2
  auxiliary function rather than list_filter, as it is easier to
  reason about (since rewriting under quantifiers does not work in
  Coq).  Added the -coq_use_filter_fn option for backwards
  compatibility (*).

- Introduced a new embed hom 

      embed {{ coq-lib foo1 foo2 foo3 }}

  to avoid generation of functions foo1, foo2, foo3 (*)

- No longer generate auxiliary list types for formula_dots in Coq
  backend with -coq_expand_list_types true because today Coq now knows
  how to generate the right induction principle.

- Parsing of defns or embed is more robust wrt newlines (*).

- Various bug-fixes (including #13487), improvements to error reports,
  and performance optimisations.

Entries labelled with (*) were contributed by Viktor Vafeiadis.

2011.11.18 Version 0.21.1

This version fixes a packaging problem of the version 0.21.

2011.12.9 Version 0.21.2

- fix bug 13645: forced use of :nonterm: syntax in conclusions of defn
  rules in 0.21.1 (thanks to Karl Palmskog for reporting the bug).

- Added new hom syntax {{* ... *}} that permits {{ and }} appearing
  inside.  The existing syntax {{ ... }} is also valid.

- Added embed tex-wrap-pre/tex-wrap-post homs to customize tex
  wrapping: the default LaTeX header can be changed by writing 

    embed {{ tex-wrap-pre ... }} 

  and the default footer by writing 

    embed {{ tex-wrap-post ... }}.  

  In addition, the program option -tex_wrap false can be used to omit
  wraping the tex output (-tex_wrap false overrides any
  tex-wrap-pre/tex-wrap-post embeds).

- minor updates to the Hol backend to target the new Hol syntax.


2012.01.04 fix for HOL multiple definitions bug

2012.06.12 fix for HOL syntax change

2012.11.29 bugfix 14175

2012.12.04 bugfix  15158


2013.04.20 

- experimental support for generating Lem definitions, including new
  homs lem, lemvar, ichlo


2013.06.22  

- New aux-hom feature:

We permit an aux hom on grammar rules. For any rule with such a hom,
we transform that rule by appending an "_aux" to its primary nonterminal
root name. We then add a synthesised rule with the original nonterminal
root name and a single production, with a shape described by the body of 
the aux hom, which must be of the form  

  {{ aux  foo1 foo2 _ bar1 bar2 bar3 }}

with a single _ and any number of strings fooi and barj before and
after, and no Raw_hom_ident's.  The _ is replaced by the original
nonterminal root name.  

For example, given a grammar or metavariable l of source locations, one
might say 

ntr :: 'NTR_'  ::=  {{ aux _ l }}
 | ...

to synthesise grammars ntr_aux and ntr of unannotated and location-annotated 
terms, the first with all the original productions and the second with a 
single production 
 | ntr l :: :: NTR_aux. 

If the rule has an empty production name wrapper (eg with '' in place
of 'NTR_') then the production name is based on the original
nonterminal root, capitalised and with _aux appended (eg Ntr_aux), to
avoid spurious conflicts.

Generation of aux rules is controlled by a command-line option
-generate_aux_rules {true|false}, which one might (eg) set to false
for latex output and true for OCaml output.

- New {{ texlong }} hom on productions, letting long productions
be typeset with the production extending into the space usually used
for comment, pushing that onto the next line. 

2013.07.04

- replace "make" by "$(MAKE)" in Makefile.  Should fix 15719, reported
  by peterbb@ifi.uio.no for OpenBSD

2013.07.04 Version 0.22

- add auxparam hom

2013.10.24 Version 0.23

2013.11.17 

- add command-line option -output_source_locations <i>  to include
  comments in the output giving the source locations:
    i=0 adds no locations
    i=1 adds a location for each inductive definition rule
    i=2 also adds a location for other components of the output
  Location annotations are lines of the form

   (* #source file FILENAME1 lines M1 - N1  and ... and FILENAMEk lines Mk - Nk *) 

  (or with % instead of (* *) for the Latex output).

2014.01.30 fix bug in {{ order }} hom for Lem backend

2014.01.30 Version 0.24

2014-08-28 Version 0.25

- fix incompatibility with OCaml 4.02.0 comment syntax, from Damien
  Doligez/Anil Madhavapeddy

2016-10-27 Snapshot of 0.25 release moved to github at
            https://github.com/ott-lang/ott

2017-02-10 Add command-line option -tex_suppress_category <string> to 
  suppress productions or rules with the specified category string.

2017-02-13 Add command-line option -tex_suppress_ntr <string> to
  suppress the grammar rule with that principal nonterminal root.

2017-05-28 fixes for Coq 8.5 and 8.6, contributed by palmskog

2017-05-29 - 2017-06-14  Add experimental support for generating a
standalone lexer, menhir parser, and pretty printer, as illustrated in 
tests/menhir_tests/test10menhir

2017-07-17 fixes for OCaml safe string, contributed by jpdeplaix

2017-09-07 example of "literate" ott spec, in tests/test10literate

2017-09-21 use Type instead of Set in Coq list functions, contributed by palmskog

2017-09-21 Version 0.26

2017-09-26  [palmskog] fixes for Coq 8.7

2017-10-03  For the generated lexer, metavar definitions should either have an ocamllex hom (specifying how they should be lexed) or an ocamllex-remove hom (specifying that a constructor of the token type should be generated, but without a lexer rule).

2017-10-09

- improve menhir parser and pp generation for combinations of
  {{ aux _  l }} rules (recording source location info) and quotient
  rules.  As in test/menhir/test10menhir_with_aux/.  Probably fragile.

- improve menhir parser and pp generation for {{ phantom }} rules

2017-10-11 

- add highly experimental -aux_style_rules false option,
  adding aux info as extra constructor arguments rather than additional
  rules

- use PPrint instead of OCaml string concatenation in raw and cooked
  generated pp

2017-10-16 [hannesm] use ocamlc/ocamlopt (not .opt)

2017-10-29 add tex file for macros used in -alltt <filename> output

2017-11-26 fixes for Isabelle and for regression testing (in progress)

2017-11-27 Version 0.27

2017-12-05 [Brian Campbell] Bugfix: add missing case of Lem auxparam type name
hack when it's hom 

2018-01 [Peter Sewell, + palmskog for Coq] copy ocaml_light example
  sources from svn (rsem/ott/old_pre_github/examples/caml) and
  partially de-bitrot

2018-02 [JoeyEremondi] add pointer to VSCode plugin
        [hannesm, Blaisorblade] clean opam install of Emacs ott-mode

2018-04-24 Version 0.28

2018-04 @palmskog Coq 8.8 compatibility

2018-05 @alastairreid add -generate_aux_rules false when generating PDF

2019-08 @dstolfa support for comments in Isabelle 2018

2019-08 @JoeyEremondi fix list bounds when subrules are present

2019-08 @JoeyEremondi make error messages consistently formatted with locations

2019-08 @buggymcbugfix explin OTT comment syntax in documentation

2019-08 @rafoo replace `` by $() and add LaTeX packages required by pandoc

2019-08 @Vertmo improvement on generation of lexer and parser
        (metavars at end, sort tokens, precise OCaml type, update location nl)

2019-08 @rmn30 install menhir_library_extra.mly

2019-08 @hannesm update opam file to 2.0

2019-08-01 Version 0.29

2019-10 @palmskog fix Coq library deprecations with Coq 8.10

2019-11 @palmskog HOL library compatibility with kananaskis-13 and master

2019-11 @palmskog explicit Coq universes for metavars, support coq-universe hom for metavars

2019-11 @palmskog fix library and deprecation issues in Coq code from locally-nameless backend

2019-11 @palmskog set -coq_expand_list_types option to false by default

2019-11-24 Version 0.30

Peter Sewell: Some fixes in Tex generation

Peter Sewell (+ Thibaut Pérami): Improve experimental pretty-printing back-end

Peter Sewell: Add "ocamllex-from-string" hom to tweak the lexing of a metavar

Peter Sewell + Thibaut Pérami: Add "menhir-start-type" hom to specify the top level type
                               of a menhir parser

2020-06-15 Version 0.31

2020-10 @mpwassell: Add experimental JSON pretty printing

2022-03 @fpottier: Support most recent version of PPrint

2022-03 @pi8027: Support recent Coq versions tested up to 8.15

2022-03-09 Version 0.32

2022-12 @bacam: OCaml 5 compatibility

2022-12 @palmskog: Coq 8.17 compatibility

2023-01-16 Version 0.33

2023-12 @MSoegtropIMC: Windows opam build fix

2024-04 @palmskog: Coq 8.19 compatibility

2024-09 @palmskog: output simplified HOL4 Inductive syntax for trindemossen-1 and later, modernise HOL4 libraries

2024-11 @bacam: fix marshalling

2024-12 @palmskog: add explicit locality to generated Coq Hint commands

2024-12 @palmskog: move y2l to non-aux directory to avoid Windows problems, fix doc build

2024-12 @palmskog: add coq-notation hom to allow using Coq Notation sentences instead of Definition

2024-12 @palmskog: only output plain comments in generated Coq code

2024-12-30 Version 0.34