The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

If you want to know more about the use of Menhir to develop provably
correct parsers, the relevant publication is
  Validating LR(1) parsers
  Jacques-Henri Jourdan, FrançoisPottier and Xavier Leroy
  2012
  http://pauillac.inria.fr/~xleroy/publi/validated-parser.pdf

A short summary is that, when given a grammar, Menhir generates a
parser automaton (as Coq code), a Coq representation of the grammar
(as a big inductive, with one constructor by grammar production), and
a Coq proof that the Coq automaton is correct with respect to the Coq
grammar. One needs to review the generated Coq grammar to ensure that
it corresponds to the user's intent, but neither Menhir nor its
grammar input need to be trusted.

On Wed, Sep 23, 2015 at 8:52 AM, Francois Pottier
<Francois.Pottier AT inria.fr>
 wrote:
>
> Dear Coq users,
>
> A new release of Menhir (20150921) is available via opam (just run "opam
> install menhir") and from http://gallium.inria.fr/~fpottier/menhir/ .
>
> The relevant chunk of the CHANGES file is appended at the end of this 
> message.
> Here is a summary of the most important changes:
>
> - The Coq back-end (designed and implemented by Jacques-Henri Jourdan) has
>   been documented. Yes, Menhir can produce a provably correct parser, 
> written
>   in Coq's programming language.
>
> - The incremental API has been changed (in an incompatible way), and a new
>   inspection API has appeared. Expect more incompatible changes in the 
> future,
>   as these APIs are not yet mature.
>
> - Added support for anonymous rules. This allows writing, e.g.,
>     list(e = expression SEMI { e })
>   whereas previously one should have written
>     list(terminated(e, SEMI)).
>
> Best regards,
>
> --
> François Pottier
> Francois.Pottier AT inria.fr
> http://gallium.inria.fr/~fpottier/
>
> 2015/09/21:
> Re-established some error messages concerning the mis-use of $i which
> had disappeared on 2015/06/29.
>
> 2015/09/11:
> Fixed the mysterious message that would appear when a nonterminal symbol
> begins with an uppercase letter and --infer is turned on. Clarified the
> documentation to indicate that a (non-start) nonterminal symbol can begin
> with an uppercase letter, but this is not recommended.
>
> 2015/08/27:
> New option --inspection (added last January, documented only now). This
> generates an inspection API which allows inspecting the automaton's stack,
> among other things. This API can in principle be used to write custom code
> for error reporting, error recovery, etc. It is not yet mature and may
> change in the future.
>
> 2015/07/20:
> Added the command line options --unused-token <symbol> and --unused-tokens.
>
> 2015/06/29:
> Changed the treatment of the positional keywords $i. They are now
> rewritten into variables of the form '_i' where 'i' is an integer.
> Users are advised not to use variables of this form inside semantic
> actions.
>
> 2015/02/11:
> Added support for anonymous rules. This allows writing, e.g.,
> list(e = expression SEMI { e })
> whereas previously one should have written
> list(terminated(e, SEMI)).
>
> 2015/02/09:
> Moved all of the demos to ocamlbuild (instead of make).
>
> 2015/01/18:
> Incompatible change of the incremental API.
> The incremental API now exposes shift events too.
>
> 2015/01/16:
> Fixed a couple bugs in Makefile and src/Makefile which would cause
> compilation and installation to fail with "TARGET=byte". (Reported
> by Jérémie Courrèges-Anglas and Daniel Dickman.)
>
> 2015/01/01:
> Incompatible change of the incremental API.
> The entry point main_incremental is now named Incremental.main.
>
> 2014/12/29:
> Incompatible change of the incremental API.
> The API now exposes reduction events.
> The type 'a result is now private.
> The type env is no longer parameterized.
> [handle] is renamed to [resume].
> [offer] and [resume] now expect a result, not an environment.
>
> 2014/12/22:
> Documented the Coq back-end (designed and implemented by Jacques-Henri 
> Jourdan).