* Package name : coq-menhirlib
Version : 20200123-1
Upstream Author : Jacques-Henri Jourdan <jacques-henri.jourdan@lri.fr>
* URL : http://gallium.inria.fr/~fpottier/menhir/
* License : LGPL3+
Programming Lang: Coq
Description : Support library for verified Coq parsers produced by Menhir
The Menhir parser generator, when invoked with the --coq option, produces
parser code in the Coq language.
.
These parsers must be linked against this library, which provides
both an interpreter (which allows running the generated parser) and
a validator (which allows verifying, at parser construction time,
that the generated parser is correct and complete with respect to
the grammar).
This package will be maintained by ocaml-team.
Rationale: this is currently part of the menhir package. The plan is to
split the menhir source package into two source packages: menhir, and
the new coq-menhirlib, with the objective to drop the build-dependency
on coq from the menhir package. This will resolve two problems:
- having menhir build-depend on coq increases considerably the depth
of the dependency graph for ocaml-related packages. Removing this
build-dependency for menhir itself will make things easier, in particular
for transitions to new versions of ocaml or coq.
- coq does not build on all architectures, and the situation for building
coq has become worse starting with 8.11. Menhir however is a parser
generator, like bison, and should be available on all architectures.