@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?
I'm not sure I follow. Which is the failure?
FTR: the build is in 2 steps:
Can you point me to the failure?
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?
I don't think it is called:
This line clearly needs fixing in your branch: https://github.com/coq/platform/blob/2021.02/linux/create_linux_installer.sh#L11
also the first and last lines of this selection: https://github.com/coq/platform/blob/2021.02/.github/workflows/snap.yml#L35-L44
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?
There is no good reason for that, other than I don't know well enough the scripts
to call just a part of them
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.
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
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?
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
Indeed, I will look into that
supported markdown syntax
Lists: * Foo
Code: Text indented with 3 spaces or inside `
Do you have instructions for testing a snap file? I never used it.
assuming you have ubuntu,
sudo snap install --dangerous ./coq-prover....snap; ls /snap/bin/coq*; which coqide; coqide,
you want to put it in ci?
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
I'm not 100% sure
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
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 :-/
@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: Jan 30 2023 at 12:03 UTC