coq / opam

Archive for all Coq related OPAM packages organized in various repositories
https://coq.inria.fr/opam/www/
GNU Lesser General Public License v2.1
121 stars 162 forks source link

coq-vcfloat.2.1.1 doesn't work with coq-interval.4.10.0 and later #3122

Closed palmskog closed 1 month ago

palmskog commented 1 month ago

It turns out (checked locally) that VCFloat 2.1.1 neither works with Interval 4.10.0 nor 4.11.0.

cc: @JasonGross @andrew-appel

andrew-appel commented 1 month ago

the opam file for coq-vcfloat.2.2 claims it works with >= coq-interval.4.10.0, so now I conjecture that vcfloat.2.2 might also work with coq-interval.4.11.

palmskog commented 1 month ago

For the record, here is what I tried locally in Coq 8.17:

opam install coq-vcfloat

this installs coq-interval.4.11.0 and coq-vcfloat.2.1.1 and gives the following error:

# File "./Prune.v", line 1175, characters 5-10:
# Error: Not an inductive definition.
# 
# make: *** [Makefile:20: Prune.vo] Error 1

Then I did:

opam pin add coq-interval 4.10.0 && opam install coq-vcfloat

This gives the following (same) error:

# File "./Prune.v", line 1175, characters 5-10:
# Error: Not an inductive definition.
# 
# make: *** [Makefile:20: Prune.vo] Error 1

Then I did:

opam pin add coq-interval 4.9.0 && opam install coq-vcfloat

and this succeeded.

palmskog commented 1 month ago

@andrew-appel CI passed, which at least shows Interval 4.9.0 works, so OK with you to merge?