Stream: Coq devs & plugin devs

Topic: bignums test breakage


view this post on Zulip Karl Palmskog (Sep 18 2021 at 08:39):

the run-tests clause in the repo opam package for bignums is broken, since it requires the .vo files for the package to already be installed

view this post on Zulip Karl Palmskog (Sep 18 2021 at 08:41):

the CI for the bignums repo uses the coqorg Docker images, which already have the coq-bignums package installed. The latter is used for the testing in CI when executing run-tests, not actual repo contents


Last updated: Oct 16 2021 at 07:02 UTC