Michael Soegtrop (Oct 25 2021 at 08:08): Michael Soegtrop (Oct 25 2021 at 08:08):@Enrico Tassi : doing the final review / cleanup round on Coq Platform 2021.09 I came across this:
(https://github.com/coq/platform/tree/main/opam/packages/coq/coq.8.13.2)
I am not sure what to do about this. Is Snap broken without this? I ask because this is likely a merge error (by me) and this folder is not used any more in 2021.09, so I never tested with this.
In case it is needed - should it go into the upstream opam repo? What about Coq 8.14. Do we need the same patches there?
Enrico Tassi (Oct 25 2021 at 08:43):aux_file.patch is needed since coqc otherwise bail out.
the other one is only aesthetic IIRC, but may become a problem if you -w +all.
I completely forgot about these, I should check if I pushed them upstream.
Enrico Tassi (Oct 25 2021 at 08:44):OK, the main one is merged in 8.14 https://github.com/coq/coq/pull/14842
Enrico Tassi (Oct 25 2021 at 08:45):If you point me to a CI run I'll test the snap
Michael Soegtrop (Oct 26 2021 at 09:04):@Enrico Tassi : any recent CI run on the main branch should do, e.g. (https://github.com/coq/platform/actions/runs/1375443070)
Enrico Tassi (Oct 26 2021 at 09:34):OK, I started one so that it saves the artifact : https://github.com/coq/platform/actions/runs/1385008285
I'll test it this afternoon
Enrico Tassi (Oct 26 2021 at 19:41):Hum, the version I compiled picks 8.13.2 which has the bug in question (coqc cannot write .aux file).
From the repo it seems the overlay for coq 8.13 is in the wrong place (not in opam-repo, nor in opm-coq-archive). So maybe it is expected it is not picked up. So IMO this patch should go in opam-repo.
@Michael Soegtrop what should I test else?
Enrico Tassi (Oct 27 2021 at 09:48):Maybe the "workflow template" for snap should let you chose the "pick", so that I can test 8.14 as well? (which is not the default pick apparently)
Théo Zimmermann (Oct 27 2021 at 09:50):Was it plan to have both versions available on Snap? It seemed to me that only 8.13 would be available there until 2021.11.
Enrico Tassi (Oct 27 2021 at 11:15):We can have how many tracks as we like, but I believe that for each track we should have 1 pick. So if .9 defaults to 8.13, I'm ok. But I don't know if I was supposed to test that case, or the .11 default. The snap generated by that run is called .9
Enrico Tassi (Oct 27 2021 at 11:16):So I guess there is a bug in the snap, since the overlay for 8.13.2 is not picked up (not in the right place after a cleanup of the overlay layout).
Michael Soegtrop (Nov 13 2021 at 08:23):@Enrico Tassi : I am just doing another review round and see that this is still open. Did you try the snap package?
Enrico Tassi (Nov 13 2021 at 11:50):Enrico Tassi said:
Hum, the version I compiled picks 8.13.2 which has the bug in question (coqc cannot write .aux file).
From the repo it seems the overlay for coq 8.13 is in the wrong place (not in opam-repo, nor in opm-coq-archive). So maybe it is expected it is not picked up. So IMO this patch should go in opam-repo.Michael Soegtrop what should I test else?
This was my last test
Michael Soegtrop (Nov 13 2021 at 12:40):So the snap release for 2021.09 is broken?
Yes - this is in a wrong place - a merging error between your work on snap and my restructuring of the opam repos.
So for Coq 8.13.2 we need the modified opam package. How about 8.14.0?
Enrico Tassi (Nov 13 2021 at 21:30):8.14 integrates the patch, no need to overlay
Michael Soegtrop (Nov 14 2021 at 11:56):OK I will fix it.
Also @Vincent Semeria found that some links in the Readme files are wrong.
Do you think I should do a 2021.09.1 release - keeping the Windows and Mac installers - or should I change the tag und redo the snap package?
Enrico Tassi (Nov 14 2021 at 11:58):the problem is specific for snap, i would just uplod a new package to the store
Michael Soegtrop (Nov 14 2021 at 11:59):Yes but somehow the tag should match the code ... also the Readme link issue is serious (the download links to the Coq Platform source ZIPs)
Théo Zimmermann (Nov 14 2021 at 19:11):If releases are relatively cheap, then making a 2021.09.1 release could make sense. Keeping the Windows and Mac installers identical, not doing any announcement, would probably make the release sufficiently cheap. On Discourse, we can even edit the link in the announcement to point to 2021.09.1.
Michael Soegtrop (Nov 15 2021 at 10:04):@Théo Zimmermann : OK I will do a new release copying the release notes so that references go to the updated readme files but refer to the previous release for the installers. We anyway will have a new one soon.
Last updated: Jun 03 2023 at 03:01 UTC