Bug#951632: ITP: coq-menhirlib -- Support library for verified Coq parsers produced by Menhir

[Ralf Treinen <treinen@debian.org>]

Package: wnpp
Severity: wishlist
Owner: Ralf Treinen <treinen@debian.org>

* 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.