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