release infotheo 0.9.0

[affeldt-aist]

This release essentially rely on MathComp-Analysis instead of the Coq standard library.

[palmskog]

@affeldt-aist it looks like the tests don't work on OCaml < 5, which is what we use in the Coq Platform (coq-native is not available on OCaml 5). Maybe disable the tests?

[silene]

Given the error, it does not have anything to do with OCaml < 5. It is an actual bug in infotheo, since the following command is plain wrong:

Extract Inductive ConstructiveCauchyReals.CReal => "float" ["assert false"].

[affeldt-aist]

My bad. I forgot to run the tests locally. The above Extract command is not supposed to be executed.

[palmskog]

@affeldt-aist so how do you want to handle this? We could remove the tests from the opam package and add the avoid-version flag. And then you make a new release with fixed tests. I'd prefer not to have patches to the release, if possible.

[affeldt-aist]

Removing the tests + avoid-version flag seems good to me, I'll release a new version soon (certainly this week), sorry for the trouble :-(

[affeldt-aist]

Removing the tests + avoid-version flag seems good to me, I'll release a new version soon (certainly this week), sorry for the trouble :-(

We released a new version of InfoTheo (0.9.1) (which relies on MathComp-Analysis 1.9.0 which has been released in-between) where the tests ought to go through.
I have also added the "avoid version" flag for 0.9.0 (where tests have simply been removed)
and fixed another incompatibility discovered in-between for 0.7.7.

[silene]

The compilation fails immediately. Could it be that the package is incompatible with MathComp Analysis 1.9.0, which was released yesterday?

make[1]: Entering directory '/builds/coq/opam/opam-root-4.14.0-2.1.2-sandbox/4.14.0/.opam-switch/build/coq-infotheo.0.9.0'
COQDEP VFILES
Warning: in file information_theory/string_entropy.v, library itv is required from root mathcomp and has not been found in the loadpath! [module-not-found,filesystem,default]
COQC lib/coqRE.v
File "./lib/coqRE.v", line 30, characters 0-25:
Error: No such goal.

[affeldt-aist]

Yes, this is at least one problem (I pushed a fix but I feel bad for triggering again a full CI).

[affeldt-aist]

Oh! Thanks for your patience!