Michael Soegtrop (Jun 14 2021 at 10:21): Michael Soegtrop (Jun 14 2021 at 10:21):@Enrico Tassi : I am trying to fix the snap file but I don't see how it could possibly work (in any version / branch). What I miss is a call to build.sh which calls opam install for all the packages. Can you point me (in any branch/version/commit) to this?
Enrico Tassi (Jun 14 2021 at 11:26):I'm not sure I follow. Which is the failure?
Enrico Tassi (Jun 14 2021 at 11:28):FTR: the build is in 2 steps:
Can you point me to the failure?
Michael Soegtrop (Jun 14 2021 at 11:44):Well in my multi version branch it fails but for obvious reasons (I split up the opam archive). The issue is that I don't understand how it works, so I can't fix it. Can you point me to the place at which opam install for the package list is called?
Enrico Tassi (Jun 14 2021 at 11:50):I don't think it is called:
Enrico Tassi (Jun 14 2021 at 11:51):This line clearly needs fixing in your branch: https://github.com/coq/platform/blob/2021.02/linux/create_linux_installer.sh#L11
Enrico Tassi (Jun 14 2021 at 11:52):also the first and last lines of this selection: https://github.com/coq/platform/blob/2021.02/.github/workflows/snap.yml#L35-L44
Michael Soegtrop (Jun 14 2021 at 13:17):I see. So in the first step you could essentially run the complete coq platform script just without building - I guess it would be easiest to add an option for that.
One thing I don't understand is why you setup opam manually rather than with the corresponding script. What is special about the opam setup, so that you can't call the opam setup script?
Enrico Tassi (Jun 14 2021 at 13:27):There is no good reason for that, other than I don't know well enough the scripts
Enrico Tassi (Jun 14 2021 at 13:27):to call just a part of them
Enrico Tassi (Jun 14 2021 at 13:28):An alternative is to completely drop the automatic generation of the snap description using opam.
At the beginning I though that the store would use the one of the latest upload, but it is not the case, one has to update it manually.
Enrico Tassi (Jun 14 2021 at 13:29):So we could just use the OSX readme.html, copy paste it in the snap store description, and completely remove that step from the snap build
Michael Soegtrop (Jun 14 2021 at 13:32):If it is only about creating the description, it would definitely make sense to reuse the Mac HTML file - we put quite some effort into that. So HTML would be OK?
Enrico Tassi (Jun 14 2021 at 13:36):Yes (the html for mac was not there when I wrote the snap). I think the store wants markdown, but from the html to markdown is a matter of minutes IMO
Michael Soegtrop (Jun 14 2021 at 13:40):Indeed, I will look into that
Enrico Tassi (Jun 14 2021 at 13:41):supported markdown syntax
Bold: Foo
URLs: https://foo.bar
Lists: * Foo
Italics: _Foo_
Code: Text indented with 3 spaces or inside `
Michael Soegtrop (Jun 14 2021 at 14:30):Do you have instructions for testing a snap file? I never used it.
Enrico Tassi (Jun 14 2021 at 14:36):assuming you have ubuntu, sudo snap install --dangerous ./coq-prover....snap; ls /snap/bin/coq*; which coqide; coqide,
Enrico Tassi (Jun 14 2021 at 14:36):you want to put it in ci?
Enrico Tassi (Jun 14 2021 at 14:38):I think there is a caveat, if you install the snap from a local file, then the short aliases are not there, so you have to run coq-prover.coqide
Enrico Tassi (Jun 14 2021 at 14:38):I'm not 100% sure
Enrico Tassi (Jun 14 2021 at 14:39):BTW, if you don't run the job by hand, it does not save the artifact by default. You may change this default as well, since it is not very handy
Enrico Tassi (Jun 14 2021 at 14:40):and the job is a minimal one, so it just builds coq and coqide, not the full thing. The rationale was that we test on ubuntu anyway the full build. But if you want to download the snap to test it... you have to start a job manually :-/
Michael Soegtrop (Jun 17 2021 at 08:11):@Enrico Tassi : thanks for the hints - I guess I know enough now to rework it. Will do so in the next days. Maybe I disable it in Coq Platform CI until then (if other things are passing).
Last updated: Jun 03 2023 at 03:01 UTC