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

gares · 2020-12-15T10:20:14Z

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 · 2020-12-15T10:39:17Z

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 · 2020-12-15T10:58:07Z

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

gares · 2020-12-15T12:52:16Z

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 · 2020-12-15T10:33:09Z

shell_scripts/generate_coq_platform_packages_ci.sh

+  mkdir -p opam/packages/$package/$package.dev/
+  if [ -e $TMP/git/$cip/$package.opam ]; then
+    cp $TMP/git/$cip/$package.opam opam/packages/$package/$package.dev/opam
+  elif [ -e $TMP/git/$cip/*.opam ]; then


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?

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 · 2020-12-15T20:24:06Z

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 · 2021-02-26T08:14:01Z

@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 · 2021-02-26T08:36:31Z

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 · 2021-02-26T09:20:27Z

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 · 2021-02-26T15:56:15Z

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 · 2021-02-26T16:27:19Z

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 · 2021-02-26T17:00:31Z

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 · 2021-02-26T17:05:44Z

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

MSoegtropIMC · 2021-11-22T21:20:49Z

@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 · 2021-11-23T06:31:37Z

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

MSoegtropIMC · 2021-11-23T08:50:32Z

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 · 2021-11-23T09:24:05Z

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 · 2021-11-23T09:53:51Z

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 · 2021-11-23T10:14:30Z

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 · 2021-11-24T08:41:55Z

@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 · 2021-11-24T11:10:57Z

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 · 2021-11-24T11:18:42Z

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 · 2022-01-23T14:43:20Z

@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 · 2022-01-25T09:25:15Z

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

MSoegtropIMC · 2022-01-25T09:51:09Z

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.

Zimmi48 reviewed Dec 15, 2020

View reviewed changes

Zimmi48 and others added 2 commits December 15, 2020 19:58

[ci] GH actions for windows, linux and osx

3cb4dc3

[wip] script to pin Coq's ci

9cc0d58

gares force-pushed the ci branch from 5edba24 to 9cc0d58 Compare December 15, 2020 19:00

gares mentioned this pull request Dec 15, 2020

[ci] GH actions for windows, linux and osx #46

Merged

2 tasks

Base automatically changed from v8.13 to 2021.02 February 24, 2021 20:23

gares marked this pull request as draft February 26, 2021 17:05

This comment has been minimized.

Sign in to view

MSoegtropIMC mentioned this pull request Jan 24, 2022

Split github CI actions into 2 workflows + disable windows while it's broken coq/coq#15535

Merged

gares closed this Jan 25, 2022

MSoegtropIMC reopened this Jan 25, 2022

MSoegtropIMC mentioned this pull request Mar 21, 2022

Support a "CoqCI" package pick, which mimics Coq CI #227

Open

MSoegtropIMC mentioned this pull request Jun 22, 2022

[build] Consolidation of build system infrastructure coq/coq#15560

Merged

6 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

gares commented Dec 15, 2020

Zimmi48 commented Dec 15, 2020

gares commented Dec 15, 2020

gares commented Dec 15, 2020

Zimmi48 Dec 15, 2020

gares Dec 15, 2020

MSoegtropIMC commented Dec 15, 2020

MSoegtropIMC commented Feb 26, 2021

gares commented Feb 26, 2021 •

edited

Loading

MSoegtropIMC commented Feb 26, 2021

Zimmi48 commented Feb 26, 2021

gares commented Feb 26, 2021

MSoegtropIMC commented Feb 26, 2021

gares commented Feb 26, 2021

MSoegtropIMC commented Nov 22, 2021

gares commented Nov 23, 2021

MSoegtropIMC commented Nov 23, 2021

gares commented Nov 23, 2021

MSoegtropIMC commented Nov 23, 2021

Zimmi48 commented Nov 23, 2021

This comment has been minimized.

MSoegtropIMC commented Nov 24, 2021

Zimmi48 commented Nov 24, 2021

MSoegtropIMC commented Nov 24, 2021

MSoegtropIMC commented Jan 23, 2022

gares commented Jan 25, 2022

MSoegtropIMC commented Jan 25, 2022

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

Are you sure you want to change the base?

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

Conversation

gares commented Dec 15, 2020

Zimmi48 commented Dec 15, 2020

gares commented Dec 15, 2020

gares commented Dec 15, 2020

Zimmi48 Dec 15, 2020

Choose a reason for hiding this comment

gares Dec 15, 2020

Choose a reason for hiding this comment

MSoegtropIMC commented Dec 15, 2020

MSoegtropIMC commented Feb 26, 2021

gares commented Feb 26, 2021 • edited Loading

MSoegtropIMC commented Feb 26, 2021

Zimmi48 commented Feb 26, 2021

gares commented Feb 26, 2021

MSoegtropIMC commented Feb 26, 2021

gares commented Feb 26, 2021

MSoegtropIMC commented Nov 22, 2021

gares commented Nov 23, 2021

MSoegtropIMC commented Nov 23, 2021

gares commented Nov 23, 2021

MSoegtropIMC commented Nov 23, 2021

Zimmi48 commented Nov 23, 2021

This comment has been minimized.

MSoegtropIMC commented Nov 24, 2021

Zimmi48 commented Nov 24, 2021

MSoegtropIMC commented Nov 24, 2021

MSoegtropIMC commented Jan 23, 2022

gares commented Jan 25, 2022

MSoegtropIMC commented Jan 25, 2022

gares commented Feb 26, 2021 •

edited

Loading