Add opam package for new version coq-unimath.20240923

[MSoegtropIMC]

I didn't test the Coq lower bound - this is taken from the previous package.

I tested that this works with Coq 8.20.0.

@benediktahrens : if you have evidence on the Coq lower bound, please let me know. Otherwise I would suggest to keep it like this until someone fonds out that it does not work.

I guess CI will time out (not sure).

[benediktahrens]

@MSoegtropIMC : thanks a lot for preparing this.

I think that 8.18 is a good lower bound for now: we know that 8.17 does not work, and I am not sure about 8.18. 8.19 works.

[MSoegtropIMC]

All CI tests timed out. Unimath is the longest running package in Coq Platform so this is expected.

IMHO this is good to merge.

[palmskog]

Could someone please try this locally on 8.18?

[ybertot]

I just started a compilation of the zip archive obtained at https://github.com/UniMath/UniMath/archive/refs/tags/v20240923.zip

Remind if I forget to report on the result in due time.

[ybertot]

Compilation failed on my machine, here is the error message.

COQC UniMath/AlgebraicTheories/Combinators.v
File "./UniMath/AlgebraicTheories/Combinators.v", line 108, characters 10-17:
Error: Unknown Ltac2 variable quotation kind pattern

make[2]: *** [build/CoqMakefile.make:838: UniMath/AlgebraicTheories/Combinators.vo] Error 1
make[2]: *** [UniMath/AlgebraicTheories/Combinators.vo] Deleting file 'UniMath/AlgebraicTheories/Combinators.glob'
make[1]: *** [build/CoqMakefile.make:409: all] Error 2
make[1]: Leaving directory '/workspaces/bertot/UniMath-20240923'
make: *** [Makefile:102: all] Error 2

[benediktahrens]

@ybertot : thanks a lot for checking compilation with 8.18!

[ybertot]

Don't mention it, I believe the energy used to make this verification contributed to making my office warmer!

[MSoegtropIMC]

Yes, unimath is one of the longer running builds - indeed it is usually the last one running in a Coq Platform build. Thanks for going through this!

[palmskog]

Could you please bump the Coq bound? It would also be very useful if we confirmed that package works on 8.19.

[MSoegtropIMC]

I am currently too busy with other Coq Platform things to check it on 8.19.

[benediktahrens]

Could you please bump the Coq bound? It would also be very useful if we confirmed that package works on 8.19.

I confirm that it works on 8.19.

[MSoegtropIMC]

OK, then I change the lower bound to 8.19.

[MSoegtropIMC]

This should be good to merge now.

@palmskog : I am a bist astonished that CI didn't time out (it took 54min). What are the current time limits for CI?

[palmskog]

@MSoegtropIMC Gaëtan changed recently to better runners for opam CI.