Bug#919461: ssreflect ftbfs in unstable
Hi, On Thu, Feb 07, 2019 at 12:51:54PM -0500, Benjamin Barenblat wrote: > Control: retitle 919461 ssreflect FTBFS in unstable > Control: noowner 919461 > > I’m guessing this is just that 1.6.1 is not compatible with Coq 8.9. > Uploading 1.7.0 might resolve the issue, but I’m uninterested in doing > that work, particularly since the package is licensed under CeCILL-B, > which I believe to be nonfree [1]. > > Would anybody else like to do an upload of this? If not, we should just > let it drop out of testing. It seems that ssreflect is now distributed as part of the coq sources (in plugins/ssr) under LGPL 2.1. So I guess this means that the ssreflect source package can simply be removed. If someone who knows coq and ssreflect could please confirm. -Ralf.
Bug#919461: ssreflect ftbfs in unstable
Control: retitle 919461 ssreflect FTBFS in unstable Control: noowner 919461 I’m guessing this is just that 1.6.1 is not compatible with Coq 8.9. Uploading 1.7.0 might resolve the issue, but I’m uninterested in doing that work, particularly since the package is licensed under CeCILL-B, which I believe to be nonfree [1]. Would anybody else like to do an upload of this? If not, we should just let it drop out of testing. [1] https://lists.debian.org/msgid-search/875zvih02a@benwick.benjamin.barenblat.name
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
Bug#919461: ssreflect ftbfs in unstable
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. [1] https://salsa.debian.org/ocaml-team/coq/commit/4181269ff800d58e60b886d0aaa289a9cd0d [2] https://github.com/coq/coq/commit/a92e4fbe88e16c312fe57a6f00ccba94322ee111
Bug#919461: ssreflect ftbfs in unstable
Package: src:ssreflect Version: 1.6.1-3 Severity: serious Tags: sid buster [...] debian/rules override_dh_auto_install make[1]: Entering directory '/home/packages/tmp/ssreflect-1.6.1' /usr/bin/make -C mathcomp make[2]: Entering directory '/home/packages/tmp/ssreflect-1.6.1/mathcomp' Generating Makefile.coq for Coq v8.8 with COQBIN=/usr/bin/ # Override COQDEP to find only the "right" copy .ml files COQDEP VFILES *** Warning: in file ssreflect/ssreflect.v, library ssrmatching is required and has not been found in the loadpath! *** Warning: in file ssreflect/ssreflect.v, declared ML module ssreflect_plugin has not been found! *** Warning: in file ssreflect/ssreflect.v, library ssrmatching is required and has not been found in the loadpath! *** Warning: in file ssreflect/ssreflect.v, declared ML module ssreflect_plugin has not been found! COQC ssreflect/ssreflect.v File "./ssreflect/ssreflect.v", line 4, characters 15-26: Error: Unable to locate library ssrmatching. make[4]: *** [Makefile.coq:657: ssreflect/ssreflect.vo] Error 1 make[3]: *** [Makefile.coq:318: all] Error 2 make[2]: *** [Makefile:26: all] Error 2 make[2]: Leaving directory '/home/packages/tmp/ssreflect-1.6.1/mathcomp' make[1]: *** [debian/rules:41: override_dh_auto_install] Error 2 make[1]: Leaving directory '/home/packages/tmp/ssreflect-1.6.1' make: *** [debian/rules:22: binary] Error 2
