Add Coq.8.20.0

[proux01]

Cc @silene (coRM) and @palmskog (who did many previous Coq packages)

[proux01]

@MSoegtropIMC you're certainly our best Windows expert, does the CI error here ring a bell:

Uncaught exception: Invalid_argument("index out of bounds")
Error while running 'D:\opamroot\default\bin/ocamlfind.exe ocamlc -version' (exit code 3)
Configuration script failed!

[MSoegtropIMC]

No, sorry. If the same stuff works elsewhere it is likely an issue with handling absolute paths. Note that in Coq Platform I am using a patched version of ocamlfind which handles paths very differently. The main reason for the patch is to make ocamlfind relocatable, but it is also avoids a lot of issues with paths on Windows.

[proux01]

Ok, thanks for the answer.
By the way, do you have any plan to sbmit you ocamlfind patch upstream?

[MSoegtropIMC]

I proposed the patch in ocaml/ocamlfind#60 but OCaml wants to follow a different approach (which does not work for Coq Platform - at least not without quite a bit of extra work).

[MSoegtropIMC]

I reviewed the discussion there and I still think we won't converge on this. Making Windows / MacOS installers for OCaml software still seems to be a niche application.

[proux01]

So, CI seems green except:

• the framac reverse dependencies but that looks like some unrelated lablgtk3 issue
• Windows: according to the above discussion, it seems we have no hope to rapidly solve this, so the current PR should probably be merged so that users not using opam on windows (probably a vast majority of users currently) get the latest Coq release (and we can still try to fix windows later)

[MSoegtropIMC]

@proux01 : any idea why it did work for 8.19? Also note that Coq Platform does build Coq via opam on Windows. I think we should at least test if this works with the patched ocamlfind.

[proux01]

Are you sure it worked for 8.19? My understanding is that OPAM for windows is a recent thing and it just wan't tested then.

[MSoegtropIMC]

Coq Platform builds Coq using opam on Windows since 8.13, so yes I am sure this works. But we are using cygwin as build host - otherwise many opam packages won't build because they need a Posix shell (e.g. for configure scripts).

[MSoegtropIMC]

See e.g. https://github.com/coq/platform/actions/runs/10693583167/job/29643963688.

[proux01]

Yes, that's what I meant, Coq CI for windows based on the platform is green but this precise OPAM CI was probably just never tested before.

[MSoegtropIMC]

Indeed if this is a direct opam on WIndows CI I wouldn't expect that it works. How far does it get?

[proux01]

As you can see, it doesn't go past ocamlc -version in the configure script.

[avsm]

This is indeed a new test, and not a blocker. The other builds look fine to me to merge.

[mseri]

Thanks

[proux01]

Thanks!