[v8.12] Carefully select which versions of add-ons are included in the Windows installer.

[Zimmi48]

Cf. #12360.

@Janno: Should mtac2 get a new master-8.12 branch? The start point could be Mtac2/Mtac2@62071fe.

• bignums
• equations
• mtac2
• mathcomp
• menhir
• menhirlib
• compcert
• extlib
• quickchick
• coquelicot
• vst
• aactactics
• flocq
• interval
• gappa_tool
• gappa
• elpi
• HB

Link to trigger a pipeline with only the Windows build with all addons: https://gitlab.com/coq/coq/pipelines/new?var[ONLY_WINDOWS]=true&var[WINDOWS]=enabled_all_addons&ref=pr-12415

[Zimmi48]

cc @MSoegtropIMC: the part that is already done can already be reviewed. Note that for the beta release, I think this is OK to be approximate and to find a good compromise between effort and quality. For the final (8.12.0) release, we can expect that most libraries will have got new compatibility releases, and we can use these.

[Janno]

@Janno: Should mtac2 get a new master-8.12 branch? The start point could be Mtac2/Mtac2@62071fe.

Done! https://github.com/Mtac2/Mtac2/tree/master-8.12

[gares]

For HB we should soon make a 0.9.1 release for coq-elpi 1.4.
It is not clear how can we help/synchronize in this PR. Do you want us to make a coq-8.12 branch and push he re a commit updating basic-overlay?
CC @CohenCyril @pi8027

[Zimmi48]

@gares Your choice on creating an 8.12-specific branch or not. The important thing for us is that you decide what gets included in the Windows installer. If the tag is ready soon, we can use this.

[gares]

It depends if point releases of Coq are allowed to pick up updates of add-ons. If so making a branch, and have basic-overlays point to a branch rather than a commit, is probably the best option.
(with the policy that you upstream only push fixes on that branch)

[Zimmi48]

Yes, this is fine.

[Zimmi48]

with the policy that you upstream only push fixes on that branch

I assume that by "you upstream" you mean the project's maintainers.

[gares]

Yes (given I'm also an upstream I got messy).

[gares]

WRT HB, I've this PR math-comp/hierarchy-builder#76 updating coq-master to a commit we would be OK to release with Coq. Still waiting for CI.

[gares]

It is merged now

[Zimmi48]

So IIUC you are recommending to use the current head of coq-master, that is math-comp/hierarchy-builder@d450025, not the head of master (math-comp/hierarchy-builder@9d4cc1a), nor the new v0.9.1 tag

[gares]

Indeed using the tag would be best, I got confused. I shoul crete a branch coq-v8.11 from the tag.

[Zimmi48]

I guess you meant coq-v8.12.

[Zimmi48]

In the current state, menhir doesn't build. The error message is:

File "src/stage2/dune", line 66, characters 18-21:
66 |   (libraries unix fix menhirLib menhirSdk)
                       ^^^
Error: Library "fix" not found.
Hint: try: dune external-lib-deps --missing -p menhirLib,menhirSdk,menhir @install
File "src/stage1/dune", line 16, characters 18-21:
16 |   (libraries unix fix menhirLib menhirSdk)
                       ^^^
Error: Library "fix" not found.
Hint: try: dune external-lib-deps --missing -p menhirLib,menhirSdk,menhir @install
        pack lib/pack/menhirLib.{ml,mli}
Creating menhirLib.ml...
Creating menhirLib.mli...

in the Dune build step. I've disabled building menhir and its reverse dependencies for now. I don't think I'll spend more time looking into it for the beta.

The other add-ons that still haven't been tested (I've picked their version blindly, and I am not very confident on them building correctly) are gappa and interval (since they are not part of the CI).

Apart from this and the testing of the resulting installer, this PR is virtually ready.

[Zimmi48]

The latest run failed immediately. I expect this is an issue with disk space that may have been polluted by the previous runs.

[ejgallego]

Will wait for windows build to finish, then merge.

[MSoegtropIMC]

@Zimmi48 : I think there is one mistake I made: VST should now depend on CompCert, so that the installer also selects CompCert when VST is installed. But I think for a beta it is OK. One just has to check CompCert when one checks VST - traditionally one did do this anyway becaise most people using VST need clightgen. But now VST likely wouldn't work at all without selecting CompCert.

@ejgallego : please give me some time to test it. I guess it will be finished in less than 1 hour and then I will look at it.

[Zimmi48]

Yep, I think it is OK like this for a beta. The build is still ongoing but should be over in a dozen minutes or so.

[MSoegtropIMC]

Yep, I think it is OK like this for a beta. The build is still ongoing but should be over in a dozen minutes or so.

Hmm you pushed again on hour ago. Usually the full Wundows build takes more like 3..4 hours.

[Zimmi48]

@MSoegtropIMC I gave you above the link to the build that was still running from before the push. It is here: https://gitlab.com/coq/coq/-/jobs/591578678
What I force-pushed is equivalent so no need to wait for its completion.

[MSoegtropIMC]

@gares : do you have a simple test case for Elpi I can run to see if everything is installed properly?

[Zimmi48]

There are some examples in the README of https://github.com/LPCIC/coq-elpi

[MSoegtropIMC]

@Zimmi48 : I did run my little test suite. Basically it seems to work, but I need to adjust my test cases for aac-tactics, quickchick and VST - my tests don't run through any more. For Elpi I picked randomly two of the examples and they work fine. I also need to Check Hierarchy builder and UniCoq.

[ejgallego]

Approving as per github constraints.

[gares]

Coq elpi is a plugin, all the files are morally tests. If make works then it is ok. The same for HB, 1 file is the program, all the rest is test.

[MSoegtropIMC]

@gares : yes I would say Elpi is fine. I will check HB around noon. Btw.: is there an elpi discussion forum on zulip - I couldn't find one. Should I just start a thread there with the questions I have?

[gares]

I don't have a coq-elpi specific stream. I'd say you post in coq user (or coq dev depending on the question) and then we will see.

[MSoegtropIMC]

@Zimmi48 : I did a test of a few examples both on the command line and in CoqIDE for all addons and plugins delivered in the Windows Installer except for menhir and menhirlib. For compcert I tested just clightgen (in a cygwin console where gcc is installed since clightgen needs a preprocessor).

So from the Windows point of view the release is good to go :-)

[MSoegtropIMC]

P.S.: if you have a good way to pusblish my nini test suite ... the main issue is that the files have quite a variety of licenses. One option might be to pull them from the respective repositories.

[Zimmi48]

So from the Windows point of view the release is good to go :-)

Except that no because the Windows 32 bit build is failing with an OOM on Elpi. See the discussion in the release thread on Zulip and the fix being currently tested at #12501.

[Zimmi48]

P.S.: if you have a good way to pusblish my nini test suite ... the main issue is that the files have quite a variety of licenses. One option might be to pull them from the respective repositories.

Yes, pulling them from their respective repository would be the best way of ensuring that these tests are maintained. But you might also have some tests integrating several independent add-ons together?

[MSoegtropIMC]

But you might also have some tests integrating several independent add-ons together?

Thats what I do in my day job ;-) But I think as a test it is not so convenient in case one has to debug it.

[Zimmi48]

It might still make sense as an additional test on top of all the project-specific tests.

[MSoegtropIMC]

It might still make sense as an additional test on top of all the project-specific tests.

Indeed, especially since there are tricky dependencies like insisting that libraries are not copied. I see what I can do.

[Zimmi48]

FTR a new version of the Gappa plugin has already been released and the compatibility commit with 8.12 does the same thing as my patch, except it wraps it in the proper #ifdef.

[Zimmi48]

Cf. #12511

[Zimmi48]

@Janno: Should mtac2 get a new master-8.12 branch? The start point could be Mtac2/Mtac2@62071fe.

Done! https://github.com/Mtac2/Mtac2/tree/master-8.12

This is actually a tag, not a branch. Is that normal? It looks like a branch name to me.

[Janno]

This is actually a tag, not a branch. Is that normal? It looks like a branch name to me.

Well spotted. Thanks! It should be a branch now!