Michael Soegtrop (Sep 27 2021 at 07:54): Michael Soegtrop (Sep 27 2021 at 07:54):@Enrico Tassi : I did a rework of the snap creation - can you please have a look at https://github.com/coq/platform/pull/143?
I have a question regarding the version: as version field of the snap you are using the coq platform version, which is e.g.g. 2021.09.0. Since Coq Platform does now support several Coq versions and the snap creation also supports this, should we use the full name, say 2021.09.0~8.14+rc1? I guess I need to replace the tilde also with - then, since snap doesn't support + or . either?
Then during generation of the snap file you did COQ_CORE_VERSION=$(coqc --print-version | cut -d ' ' -f 1). The variable is used in the description. At this point in time coq is not installed, so the result is empty (I think it always was like this). It would be a bit wasteful to install coq just to get its version number. In the Coq Platform version files, I set a shell variable to the tag, say "8.13.2". I guess this is usually the same as what --print-version delivers. If the source is a branch, as e.g. for the dev variant, this variable is set to dev. Of course I could define a new variables the the version file called to describe the snap descriptive version.
Also I guess the description should contain a combination of the Coq Platform and the Coq version.
Michael Soegtrop (Sep 27 2021 at 08:13):Btw.: what is the rationale behind these lines in snapcraft.yaml.in
echo "COQ_PLATFORM_VERSION=@@COQ_VERSION@@" >> versions/coq_platform_version.sh
echo "COQ_PLATFORM_SWITCH_NAME=@@COQ_VERSION@@" >> versions/coq_platform_switch_name.sh
echo "COQ_PLATFORM_REPO_NAME=@@COQ_VERSION@@" >> versions/coq_platform_switch_name.sh
Why not use the opam switch and repo names the Coq Platform usually uses?
Enrico Tassi (Sep 27 2021 at 08:45):I don't recall, I probably misunderstood how things had to be done.
Yes, you would need to use - as a separator... But I don't see many changes in the snap creation, did you push that commit?
Michael Soegtrop (Sep 27 2021 at 09:17):It is still in the PR https://github.com/coq/platform/pull/143. There are no fundamental changes, but I removed the duplication of stuff I have in the script. E.g. the opam installation step is gone and I call the script also in the .yaml file generation step (I added an option to abort it after setting the environment variables and installing opam).
So what version name should we use? 2021.09.0 or 2021.09.0~8.13/8.14? Would snap support such multi version stuff at all or would we have to create different - what was the name: streams?
Michael Soegtrop (Sep 27 2021 at 09:18):Let's say the main difference is that now I understand what is going on ;-)
Enrico Tassi (Sep 27 2021 at 09:19):Hum, I'm not so sure it would be acceptable to have so many tracks
Enrico Tassi (Sep 27 2021 at 09:22):IMO the snap store should contain only the default option according to SORTORDER, which I guess would be 8.14 for 2021.09.x. Then you can create a snap if you like with other variants, for teaching, but not expect it to be in the store.
Enrico Tassi (Sep 27 2021 at 09:24):In theory, you could puth both opam roots in the snap, and export coq and coq.old-version in the path... but that would double the size of the snap. I'm not so sure this would be worth it.
Michael Soegtrop (Sep 27 2021 at 09:29):I see. maybe we could do something with the released and beta - what was it channels? Say I could now release 2021.09.0~8.13 and put ~8.14 in the beta and if 8.14 is out change that.
Michael Soegtrop (Sep 27 2021 at 09:31):I got this error in CI:
error: cannot pack "/root/prime": cannot validate snap "coq-prover": description can have up to 4096 codepoints, got 4654
Does this mean the description is too long? Does "codepoints" mean unicode characters?
I guess we should remove the license links and maybe pack a Mac like Readme with detailed information?
Enrico Tassi (Sep 27 2021 at 09:32):yes. (it's unicode "chars")
Enrico Tassi (Sep 27 2021 at 09:32):I'm afraid so. It sucks, I really don't get the point of this limitation.
Michael Soegtrop (Sep 27 2021 at 09:32):Hmm I saw that only one actually has a license link ...
Suggestions?
Michael Soegtrop (Sep 27 2021 at 09:34):I guess we can remove the word version and just use () or [] and maybe restrict the description of each package to some length.
Michael Soegtrop (Sep 27 2021 at 09:35):Anyway I will check the length of the description and abort right away if it is too long.
Enrico Tassi (Sep 27 2021 at 09:36):I think the only way out is to put a list of packages/versions + a single link to the HTML page (to be hosted somewhere).
It is soo silly, you can embed a video and picture... but 4K text
Théo Zimmermann (Sep 27 2021 at 10:00):Michael Soegtrop said:
I see. maybe we could do something with the released and beta - what was it channels? Say I could now release 2021.09.0~8.13 and put ~8.14 in the beta and if 8.14 is out change that.
I agree with Enrico that we should not propose all options via Snap, but only the default Coq version for a given platform pick. And the default version should not change, otherwise people will get a disruptive auto-update, while the whole point of tracks was to avoid that. Therefore, either 8.13 is chosen as the default version for 2021.09 (which means no Snap for Coq 8.14 for a while :cry:) or 8.14 is chosen to be the default version but 2021.09 stays in beta only for as long as needed (my preference).
Michael Soegtrop (Sep 27 2021 at 10:11):Yes tricky. The 8.13 version is also quite nice, because it is substantially extended. Maybe then we should have a Coq Platform 2021.11 or so - as an exception.
Théo Zimmermann (Sep 27 2021 at 10:12):Well, why not indeed?
Michael Soegtrop (Sep 27 2021 at 10:14):I think it is the best option. I don't want to hurry the package maintainers with providing 8.14 versions too much - better have quality than speed. But I also don't want to delay the extended package pick too much - people already waited a long time.
Michael Soegtrop (Sep 27 2021 at 11:58):@Enrico Tassi : regarding the description: I had to remove the license info and cut package descriptions to 80 chars (I add ... in case). Then it just so fits into the 4K.
Enrico Tassi (Sep 27 2021 at 12:02):I'm fine having .09 be for Coq 8.13 and .11 be for 8.14. But we have to update the release doc if this become the habit. For 8.13 I got all the tags in a week or so, and you wrote somewhere that things were converging fast. So now I'm a bit puzzled we need much more time.
Is this because we are adding new packages right now? (ideally, they should have been added before... but maybe it's too demanding)
Michael Soegtrop (Sep 27 2021 at 14:10):Well it is mostly about doing what we said we do. 8.14 is not even released and we said that people will have some time to adopt to 8.14.
And yes, for the new packages I did not even ask for a 8.14 tag - I first need to stabilize them in 8.13.
Michael Soegtrop (Sep 27 2021 at 14:12):@Enrico Tassi : I have one question regarding manual runs. I now did a matrix out of the snap to run two package lists - maybe I should undo this since we discussed that snap anyway only supports one pick. But assuming we keep it, the question arises what to do with manual runs - choose the pick then with run arguments or also run the matrix?
Théo Zimmermann (Sep 27 2021 at 14:17):8.14 is not even released
8.14+rc1 is released and has been for more than a week though.
Enrico Tassi (Sep 27 2021 at 14:20):Hum, manual runs were there mostly to do the final upload to the store. There we don't want a matrix. So I'm fine keeping a matrix if it can be disabled when "upload to the store" is selected.
Enrico Tassi (Sep 27 2021 at 14:20):or if one can say which element of the matrix has to be uploaded.
Enrico Tassi (Sep 27 2021 at 14:21):I don't know which is simpler to do...
Michael Soegtrop (Sep 27 2021 at 15:51):@Enrico Tassi I guess since won't use the other variants, it doesn't make that much sense to test it in CI then. I will remove the matrix.
Michael Soegtrop (Sep 27 2021 at 15:56):@Théo Zimmermann : still the .0 tag of Coq Platform is expected to happen 4 weeks after the .0 release of Coq. If we are faster - fine. But looking at the large number of new packages, I don't see a good reason to hurry it. Of course we can have a beta release quite soon.
One widely used package still missing is equations btw. I can make an opam package pointing to the latest commit tested in Coq CI, but this won't work for a release.
Karl Palmskog (Sep 27 2021 at 16:01):@Michael Soegtrop I already created a tag-based package for Equations for 8.14 that Matthieu has approved: https://github.com/coq/opam-coq-archive/pull/1830
Karl Palmskog (Sep 27 2021 at 16:02):@Michael Soegtrop I can start to cc you in opam archive PRs that may interest you, but I honestly thought you were monotoring the opam archive repo.
Michael Soegtrop (Sep 27 2021 at 16:20):@Karl Palmskog : Thanks for the hint!
I frequently look at the opam archives but I don't search daily for updates for each of the 40 or so packages I am interested in. I would have expected a comment in this issue: (https://github.com/mattam82/Coq-Equations/issues/427).
Michael Soegtrop (Sep 27 2021 at 16:21):And yes, please CC me on opam updates that are Coq Platform related.
Karl Palmskog (Sep 27 2021 at 16:23):as has already become clear, we have some not-entirely-aligned goals in the opam archive vs. the platform. In the archive, we are generally very CI-driven (add a package so it works with CI for someone else). Not sure what we can do besides cc-ing stuff and flagging up here.
Michael Soegtrop (Sep 27 2021 at 16:25):I think that's totally fine. Just when I create an issue to create a tag for 8.14, I somehow expect that people leave a note there when the tag is there. Then I look for an opam package, and if it is not there first create it locally and then batch push these. But without a note in the project, I don't even look for an opam package.
Michael Soegtrop (Sep 27 2021 at 16:26):For all other involved packages the process did work fine. Equations was the only one where obviously it didn't.
Karl Palmskog (Sep 27 2021 at 16:28):maybe we can agree with Matthieu on a backup maintainer for Equations we can ping for tagging during the rc phase (Théo suggested Pierre-Marie)
Karl Palmskog (Sep 27 2021 at 16:30):people's availability is just too random for there not be blockages for rcs/releases of single-maintainer packages, but it's usually independently random
Michael Soegtrop (Sep 27 2021 at 16:31):I don't think this is really required - it all works and also for equations we solved it rather quickly I guess.
But maybe you can have a look at the opens in the Coq Platform tracker issue from time to time (for 8.14 it is https://github.com/coq/platform/issues/139 - there is an extra issue label for tracker issues). If something is open there and you know it is closed, it would help if you ping me.
Michael Soegtrop (Sep 27 2021 at 16:33):Also it is anyway expected that we have a few weeks of time to do the tagging. One of the reasons d'être of the Coq Platform is that this release process can be done in a more relaxed and quality way. There is no need to push people to do a tag today.
Last updated: Jun 03 2023 at 03:01 UTC