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 , 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 : 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 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 and -o 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 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 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 to suppress productions or rules with the specified category string. 2017-02-13 Add command-line option -tex_suppress_ntr 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 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