Stream: Coq devs & plugin devs

Topic: bignums test breakage

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

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: May 28 2023 at 13:30 UTC