[ci] [gh-actions] Run the platform job using Github Actions

[ejgallego]

We move the CI job creating the platform windows installer from Gitlab-driven Inria custom runners to standard Github actions one.

While we are at it, we significantly cleanup the build script, trying to avoid as much hackery as possible, and splitting it in logical stages.

Notwithstanding, the current system is still not very satisfactory, in particular:

• build time is very long, we should cache cygwin folder at least, and only rebuild if the coq-platform ref we use has changed; fortunately GH actions do support this
• verbosity of the script is out of control
• we can still cleanup way more things

Please review the list of chosen bugs below, and speak if you think it is too wide.

closes #6807 , closes #7428 , closes #8046 , closes #8622 , closes #9401 , closes #11073

Kind: infrastructure.

• Added / updated test-suite
• Corresponding documentation was added / updated
• Entry added in the changelog

Note: this PR was originally started from the nice setup of Jason Gross [1] for windows CI setup, but it was updated to actually use the platform after #13598

[1] https://github.com/mit-plv/fiat-crypto/blob/master/.github/workflows/coq-windows.yml

[gares]

Yes, but is this job supposed to test?

[MSoegtropIMC]

@ejgallego : for sure one could add an option to run the test suite. The platform CI runs a very simple "smoke test" - that is one or two selected examples from each provided package. The idea is that Coq Platform is a kind of meta build and relies on that the packages it builds are OK. The idea of the "smoke test" kit is to check if e.g. installation of packages went fine.

[ejgallego]

@MSoegtropIMC , another question, how difficult would it be to split the cygwin setup to its own script?

This way we could run it in its separate step, and have an easier time caching.

Similarly for opam, would be very interesting to separate opam install --deps-only coq from the actual opam install coq

Caching for opam should work fine and be reproducible as soon as you folks start using opam lock files.

[MSoegtropIMC]

@ejgallego : this is already supported:

• pass -build=n to coq_platform_make_windows.bat - this will just setup cygwin but do not run the script
• start up the generated cygwin and run coq_platform_make.sh from the copied coq_platform folder or alternatively git clone something else and start the script.

But I must admit, this is not tested much and also the cygwin setup sometimes changes.

[ejgallego]

But I must admit, this is not tested much and also the cygwin setup sometimes changes.

Thanks for the feedback, will try!

I guess the way to make this more reliable would be to structure the platform build as a sequential call of these scripts from a top-level driver.

[Zimmi48]

That's not something that we typically document in the user-facing changelog (which is already long enough without these kinds of details). It would make more sense in the dev changelog.

[ejgallego]

As you prefer, I was under the impression that some users were downloading the windows artifacts for master, so I signaled it.

[Zimmi48]

That's a good point. Maybe reformulate to put this aspect forward (and maybe do not link to the fixed issues which are not really relevant for users).

[ejgallego]

Ok, I did tweak it.

[Zimmi48]

Will merge when CI passes.

@gares can I add you to the @coq/windows-build-maintainers team?

[gares]

no

[Zimmi48]

OK, I figured that you were the best person to be in this team (more suited than me anyway) given that you've authored most of the code that is being moved in dev/ci/platform. Maybe we should just remove the @coq/windows-build-maintainers team and leave this under the ownership of @coq/ci-maintainers then.

[gares]

I'm not fluent in .bat, and I don't even have a windows PC at hand...

[Zimmi48]

Yeah, me neither. Anyway, let's keep things as they are for the time being.

@coqbot merge now