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/
