Bug#919461: ssreflect ftbfs in unstable
On Wed, Jan 16, 2019 at 08:50:51AM -0500, Benjamin Barenblat wrote:
> Control: retitle 919461 ssreflect FTBFS in unstable due to missing ssrmatching
> Control: owner 919461 !
>
> That’s my fault. In my most recent Coq upload, I disabled ssrmatching
> and a couple of other plugins due to license concerns [1]. Those have
> now been resolved upstream [2]. I’m going to backport the changes to
> 8.8.2 and do another upload in the next few days, after which this bug
> should go away.
>...
There is now a different error:
https://tests.reproducible-builds.org/debian/rb-pkg/unstable/amd64/ssreflect.html
...
Generating Makefile.coq for Coq v8.9 with COQBIN=/usr/bin/
# Override COQDEP to find only the "right" copy .ml files
COQDEP VFILES
*** Warning: in file ssreflect/ssreflect.v, declared ML module ssreflect_plugin has not been found!
*** Warning: in file ssreflect/ssreflect.v, declared ML module ssreflect_plugin has not been found!
COQC ssreflect/ssreflect.v
File "./ssreflect/ssreflect.v", line 6, characters 0-18:
Warning: There is no option SsrAstVersion. [unknown-option,option]
File "./ssreflect/ssreflect.v", line 269, characters 9-18:
Error:
Syntax error: 'Type' or 'Types' expected after 'Implicit' (in [vernac:gallina_ext]).
make[4]: *** [Makefile.coq:663: ssreflect/ssreflect.vo] Error 1
cu
Adrian
--
"Is there not promise of rain?" Ling Tan asked suddenly out
of the darkness. There had been need of rain for many days.
"Only a promise," Lao Er said.
Pearl S. Buck - Dragon Seed
Reply to: