Stream: Coq Platform devs & users

Topic: Snap file


view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Jun 14 2021 at 11:26):

I'm not sure I follow. Which is the failure?

view this post on Zulip Enrico Tassi (Jun 14 2021 at 11:28):

FTR: the build is in 2 steps:

Can you point me to the failure?

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Jun 14 2021 at 11:50):

I don't think it is called:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jun 14 2021 at 13:27):

to call just a part of them

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 13:40):

Indeed, I will look into that

view this post on Zulip 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 `

view this post on Zulip Michael Soegtrop (Jun 14 2021 at 14:30):

Do you have instructions for testing a snap file? I never used it.

view this post on Zulip 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,

view this post on Zulip Enrico Tassi (Jun 14 2021 at 14:36):

you want to put it in ci?

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jun 14 2021 at 14:38):

I'm not 100% sure

view this post on Zulip 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

view this post on Zulip 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 :-/

view this post on Zulip 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: Jan 30 2023 at 12:03 UTC