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

[Ralf Treinen <treinen@irif.fr>]

On Wed, Feb 19, 2020 at 10:02:55AM +0100, Stéphane Glondu wrote:
> Le 19/02/2020 à 09:06, Ralf Treinen a écrit :
> > - 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.
> 
> Could you elaborate? What makes coq 8.11 so much worse w.r.t portability?

already 8.10.2:

https://buildd.debian.org/status/package.php?p=coq&suite=experimental

A package for 8.11.0 is in the experimental/master branch, but I haven't
uploaded to experimental yet. It builds on amd64. I also tried

- on an armel porterbox which leads to a compilation error in some
  debug tool. This can be circumvented, but we have not even reached
  the point of running the test suite.
- on an i386 porterbox, leading to failure in the test-suite which
  according to upstream (ejgallego) is critical:

  https://github.com/coq/coq/issues/11624

-Ralf.
-- 
Ralf Treinen
Institut de Recherche en Informatique Fondamentale
Pôle Preuves, Programmes et Systèmes
Université de Paris
http://www.irif.fr/~treinen/