[wip] script to copy Coq's CI info into the platform

[gares]

This is a draft script which:

• reads ci info from Coq (which upstream branch is tracked for Coq, may not be the same metadata called dev-repo of opam packages)
• builds a opam/packages/package/package.dev/opam file for each package using the upstream opam package (may need fixing, to be seen) and pins the hash currently tested by Coq
• builds coq_platform_packages_ci.sh containing the list of PACKAGES built that way

The objective is to be able to test the platform scripts on Coq's master on a regular basis.

@Zimmi48 @MSoegtropIMC I think the next step is to hook into some CI infrastructure and see how it goes.
Preferences/Ideas?

Example output:

========================== platform version CI ==================
PACKAGES="${PACKAGES} coq.dev"                       # https://github.com/coq/coq.git#6c35e25 (on branch master)
PACKAGES="${PACKAGES} coqide.dev"                    # https://github.com/coq/coq.git#6c35e25 (on branch master)
PACKAGES="${PACKAGES} coq-unicoq.dev"                # https://github.com/unicoq/unicoq#8ea4f91 (on branch master)
PACKAGES="${PACKAGES} coq-ext-lib.dev"               # https://github.com/coq-community/coq-ext-lib#159c361 (on branch master)
PACKAGES="${PACKAGES} coq-equations.dev"             # https://github.com/mattam82/Coq-Equations#3d44714 (on branch master)
PACKAGES="${PACKAGES} coq-bignums.dev"               # https://github.com/coq/bignums#2b3492f (on branch master)
PACKAGES="${PACKAGES} coq-aac-tactics.dev"           # https://github.com/coq-community/aac-tactics#ea63306 (on branch master)
PACKAGES="${PACKAGES} coq-mtac2.dev"                 # https://github.com/Mtac2/Mtac2#9a9956d (on branch master)
PACKAGES="${PACKAGES} coq-simple-io.dev"             # https://github.com/Lysxia/coq-simple-io#09c164d (on branch master)
PACKAGES="${PACKAGES} coq-quickchick.dev"            # https://github.com/QuickChick/QuickChick#cef4740 (on branch master)
PACKAGES="${PACKAGES} coq-flocq.dev"                 # https://gitlab.inria.fr/flocq/flocq#8fdb8b1 (on branch master)
PACKAGES="${PACKAGES} coq-coquelicot.dev"            # https://gitlab.inria.fr/coquelicot/coquelicot#88a9e56 (on branch master)
PACKAGES="${PACKAGES} coq-gappa.dev"                 # https://gitlab.inria.fr/gappa/coq#3935dfe (on branch master)
PACKAGES="${PACKAGES} coq-interval.dev"              # https://gitlab.inria.fr/coqinterval/interval#86aa3c0 (on branch master)
PACKAGES="${PACKAGES} coq-elpi.dev"                  # https://github.com/LPCIC/coq-elpi#29d18e4 (on branch coq-master)
PACKAGES="${PACKAGES} coq-hierarchy-builder.dev"     # https://github.com/math-comp/hierarchy-builder#dc171e0 (on branch coq-master)
PACKAGES="${PACKAGES} coq-mathcomp-ssreflect.dev"    # https://github.com/math-comp/math-comp#7da602f (on branch master)
PACKAGES="${PACKAGES} coq-mathcomp-fingroup.dev"     # https://github.com/math-comp/math-comp#7da602f (on branch master)
PACKAGES="${PACKAGES} coq-mathcomp-algebra.dev"      # https://github.com/math-comp/math-comp#7da602f (on branch master)
PACKAGES="${PACKAGES} coq-mathcomp-solvable.dev"     # https://github.com/math-comp/math-comp#7da602f (on branch master)
PACKAGES="${PACKAGES} coq-mathcomp-field.dev"        # https://github.com/math-comp/math-comp#7da602f (on branch master)
PACKAGES="${PACKAGES} coq-mathcomp-character.dev"    # https://github.com/math-comp/math-comp#7da602f (on branch master)
#PACKAGES="${PACKAGES} coq-mathcomp-bigenough.dev"   # no corresponding entry in Coq's ci
#PACKAGES="${PACKAGES} coq-mathcomp-finmap.dev"      # no corresponding entry in Coq's ci
#PACKAGES="${PACKAGES} coq-mathcomp-real-closed.dev" # no corresponding entry in Coq's ci
#PACKAGES="${PACKAGES} coq-menhirlib.dev"            # since no opam package found
#PACKAGES="${PACKAGES} coq-compcert.dev"             # since no opam package found
PACKAGES="${PACKAGES} coq-vst.dev"                   # https://github.com/PrincetonUniversity/VST#7b3946f (on branch master)

[Zimmi48]

Regarding choice of CI provider, I recommend GitHub Actions because it gives a long time limit on shared runners (6 hours).

Note that I've tried setting up some Windows CI but I've not been successful so far because of my lack of understanding of how the scripts work (https://github.com/Zimmi48/coq-platform/tree/windows-action).

[gares]

I'll take it here and see how it goes, thanks!

[gares]

It starts to crawl.
On windows I have a funny error to be understood, on ubuntu I did a hack to get the script start but it seems to kill the output.

@MSoegtropIMC it seems the unix script does not have the COQREGTEST flag, so I had to use yes "" | ... but it does not work well. I can try to add support for it, unless you have a better idea.

[Zimmi48]

What is the use case for this second case?

Could there be a default case where the opam file is taken from the coq-extra-dev repo?

[gares]

Sometimes people call, in their repo, the opam file foo.opam instead of coq-foo, don't ask me why.

Yes, I thought about that, and maybe the ones in the usual repo should have precedence, and we should also look in the local repo with higher precedence... I think we should think carefully about these rule (I did not yet).

[MSoegtropIMC]

Btw.: I plan to make a script which creates a "smoke test kit" - that is one or at most a few files for each package we ship, which should be compilable with coqc. Maybe you can use this in the platform CI.

[MSoegtropIMC]

@gares : How shall we proceed with this PR?

I could live with the current solution of linking all dev packages and correct it here. Or would you prefer to finish this and link the dev-ci content to Coq master?

[gares]

If the .dev packages we have in the main archive point to the branch tracked by Coq, then we can close it. Is it the case?

[MSoegtropIMC]

I don't think the Coq team updates the .dev opam package when they pin something in Coq master, so the tests in dev-ci are independent from what is tested in Coq master. But it is very close, so I still profit from Coq's CI - most issues we have here are fixed within a day without me doing anything. I meanwhile learned that if I wait 24 hours before reporting an issue upstream I have only 1/3 of the work.

In the end the main rationale for tying the versions we test to Coq is saving effort on Coq Platform side. The main rationale for staying independent is conceptual independence and testing if the opam .dev packages actually work - something which has a value on its own. So I would wait and see if the effort is manageable. If yes I would prefer to stay independent, if it is too much work we should tie it together.

[Zimmi48]

For dev-ci, I think the .dev package should be always fine except when for very short periods of time after merging PRs that broke plugins. But in this case, checking for what is tested in Coq's CI wouldn't help either.

[gares]

My only "concern" is that I may want a have, say, coq-elpi.dev which points to my master branch, but Coq's ci points to the coq-master branch. I don't, so the .dev package can point to the branch that fits the platform CI purpose, but this scenario is not impossible. If it happens we will need to add one extra .dev package, eg .platform.dev.

So I think this PR can be closed.

[MSoegtropIMC]

But I would archive the work. It might e.g. happen that one day we have several future looking ci branches - now that dev-ci is no longer the master / default branch.

[gares]

OK, I guess we can then leave this here as a draft

[MSoegtropIMC]

@gares : this has been around for a while and I wonder what to do with it. The general Coq Platform concept for dev builds is a bit different (using the dev opam packages) but it might make sense to also have a "Coq master" package pick, which uses this script. What do you think?

[gares]

given that now the platform is larger than coq ci, I'm not so sure these scripts are that useful

[MSoegtropIMC]

I think the main question is if we want to offer a Coq Platform configuration which mimics the Coq master CI package pick - which is not the same as an opam dev package pick.

Of course one could also think about keeping the opam extra-dev repo more or less in sync with Coq CI, say with a daily action (which is only run if Coq CI passed). As is .dev hardly builds. I think this would be useful for package maintainers.

[gares]

I think the main question is if we want to offer a Coq Platform configuration which mimics the Coq master CI package pick - which is not the same as an opam dev package pick.

I see, but as I was saying, the scripts would only "pin" some parts of the platform. What about the other packages? We pick the .dev and cross fingers? We don't pick them at all?

[MSoegtropIMC]

I think we first should discuss if it is desirable to have a dev pick which mimics Coq CI - and then only includes packages which are in Coq CI. How we implement it then is a different question, but I guess this PR would be part of it. maybe we should have this discussion on Zulip ...

[Zimmi48]

I think we first should discuss if it is desirable to have a dev pick which mimics Coq CI

I don't think this would be useful or desirable.

[MSoegtropIMC]

@Zimmi48 : my thought behind this is that opam dev does not build frequently, while the package pick tested in Coq master CI usually does build.

It might help package maintainers to have an easy way to install a close to master version of Coq Platform, and mimicking Coq master CI would IMO be the least maintenance effort to get there.

Why do you think this wouldn't be useful?

[Zimmi48]

The platform contains things that are not in Coq's CI and Coq's CI contains things that are not in the platform. It could make sense to have a variant of the platform with only the intersection of the two (to have higher chances that everything works). But I don't think it makes sense to have a variant of the platform with everything that is in Coq's CI (but maybe that was not what you were proposing anyway).

[MSoegtropIMC]

I had more in mind that we cut this down to everything which is a dependency of a package in Coq Platform, say CompCert for VST and Flocq for CompCert. This is all what package maintainers need - and this is the intended audience of such a package pick. But then I think we should make sure that all dependencies of packages in Coq Platform are in Coq CI (I think this is the case already, but we should check).

[MSoegtropIMC]

@gares : I am not sure what to do with this PR. The main Coq Platform CI tests only releases. I just made the .dev pick more complete. As of today it compiles fine. I would treat the .dev CI only as informational, so I am not so sure I want to make it equivalent to the Coq CI - which exists for a different purpose. Coq CI is there to check Coq for regressions, while Coq Platform dev CI is there to get early warnings about potential problems.

But I am not sure about this. What do you think?

[gares]

I think we can close this, the dev pick is sufficient IMO.

[MSoegtropIMC]

There was also a recent discussion with @Zimmi48 (after I deleted the dev-ci branch which was still in use in Coq CI). I think in the end I might have 3 picks (all in one branch):

• the current "all latest default" dev pick - mostly to see what the future brings in CI
• a dev pick which matches Coq CI, which should be more likely to build
• a special pick optimized for Coq's Windows CI needs

For the second one I will reuse some of the stuff here, so I will keep it open until this is done.