Stream: Miscellaneous

Topic: Snap package


view this post on Zulip Enrico Tassi (Jan 05 2021 at 10:57):

I'm working on a snap package for Coq, so that people can try the system out easily.
The package is still private, here a screenshot of how it looks like: https://github.com/coq/platform/pull/49

Snap packages live in a container, and all installed binaries live in a namespace, eg coq-prover.coqtop.
One can request "aliases", like coqide -> coq-prover.coqide so that command names users are familiar to are not prefixed by the namespace.
I did such a request, but I just discovered that I need 2 votes (a message with a +1 in it) here: https://forum.snapcraft.io/t/aliases-request-for-coq-prover/21925 for the request to be considered.

I should have advertised this earlier, the deadline is today I'm afraid. Help please.

view this post on Zulip Théo Winterhalter (Jan 05 2021 at 11:07):

I tried to register but I got this "We cannot detect if your account was created, please ensure you have cookies enabled." and I have—as of yet—not received a confirmation email.

view this post on Zulip Théo Winterhalter (Jan 05 2021 at 11:07):

After a second try my registration was successful but I'm still waiting on the confirmation email.

view this post on Zulip Enrico Tassi (Jan 05 2021 at 11:20):

Thanks for your effort!

view this post on Zulip Théo Winterhalter (Jan 05 2021 at 11:58):

Just liking the post counts as a vote?

view this post on Zulip Enrico Tassi (Jan 05 2021 at 12:31):

I think you need to write a message as I did

view this post on Zulip Théo Winterhalter (Jan 05 2021 at 12:46):

Done!

view this post on Zulip Enrico Tassi (Jan 05 2021 at 12:55):

Thanks! Just in case, more than 2 votes are actually a plus, if anyone else has the time.

view this post on Zulip Théo Zimmermann (Jan 05 2021 at 15:15):

Done.

view this post on Zulip Théo Zimmermann (Jan 05 2021 at 15:16):

BTW, will you be able to request more aliases in the future (like for Dune)?

view this post on Zulip Théo Zimmermann (Jan 05 2021 at 15:16):

And wouldn't coqidetop / coqtop be required for VSCoq / PG to work?

view this post on Zulip Enrico Tassi (Jan 05 2021 at 15:25):

Thanks!.
Yes I can ask for more aliases later on. It's just that it is a metadata which is global, so it is manually handled (via a forum).

I did forget about PG :-/. For vscode I proposed this: https://github.com/coq-community/vscoq/issues/192 , we can do the same for PG. I'm not so sure that exposing "technical" binaries is in the spirit of snaps, so I did request the minimal amount of them, I believe.

You are welcome to write a message requesting more aliases if you think it's best. I don't have a strong opinion. Maybe the admins there can clarify what is best.

view this post on Zulip Enrico Tassi (Jan 05 2021 at 15:30):

If you think it is a good idea to ship dune, just fix this cleanup line https://github.com/coq/platform/pull/49/files#diff-af2e340f66728cd9ab75bcf765a06fd61cfc707a355ba2203b49759eea6dfa26R25 and add an entry for coq-prover.dune later on in the file following the examples.

view this post on Zulip Enrico Tassi (Jan 05 2021 at 15:32):

IIRC dune is a self contained binary, no extra file is needed I think

view this post on Zulip Théo Zimmermann (Jan 05 2021 at 15:57):

Your strategy for editors sounds good to me. Regarding Dune, I think it can (or even should) wait given that Dune's Coq support is not there yet that we can recommend it to beginners.

view this post on Zulip Paolo Giarrusso (Jan 05 2021 at 17:18):

what about a coqc alias?

view this post on Zulip Karl Palmskog (Jan 05 2021 at 17:18):

yeah, without that everyone who doesn't use coq_makefile will see their projects fail, right?

view this post on Zulip Karl Palmskog (Jan 05 2021 at 17:19):

let's just say that there are many horrible makefiles out there that directly use coqc

view this post on Zulip Paolo Giarrusso (Jan 05 2021 at 17:22):

does coq_makefile even deal with different names? or do you mean make COQC=... will work?

view this post on Zulip Paolo Giarrusso (Jan 05 2021 at 17:23):

but I'm sure makefiles hard-coding coq_makefile exist, and if that's bad I never knew it

view this post on Zulip Karl Palmskog (Jan 05 2021 at 17:23):

coq_makefile uses $(COQBIN)coqc, and I believe he sets $(COQBIN) in the snap

view this post on Zulip Enrico Tassi (Jan 05 2021 at 17:37):

I set up coq-prover.coq_makefile so that is picks the binaries from the internal directory, not the PATH, hence it picks the ones in the snap.

view this post on Zulip Enrico Tassi (Jan 05 2021 at 17:38):

I see the snap package as a things for beginners. If you run your own build system, then you are not one IMO.

view this post on Zulip Enrico Tassi (Jan 05 2021 at 17:39):

The snap really can't be a replacement for an installation with opam/nix, it's too limited in its permissions (which is good for "apps").

view this post on Zulip Enrico Tassi (Jan 05 2021 at 17:40):

Anyway, feel free to ask for more aliases in the forum if you think you will need it. I'm not against it.

view this post on Zulip Paolo Giarrusso (Jan 05 2021 at 19:16):

if coq_makefile (and dune) work that’s likely more than good enough, in case you download some project and want to make or make install libraries. I’d also check Software Foundations, since it’s the primary use-case for beginners.


Last updated: Aug 19 2022 at 20:03 UTC