Enrico Tassi (Jan 05 2021 at 10:57): 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.
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.
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.
Enrico Tassi (Jan 05 2021 at 11:20):Thanks for your effort!
Théo Winterhalter (Jan 05 2021 at 11:58):Just liking the post counts as a vote?
Enrico Tassi (Jan 05 2021 at 12:31):I think you need to write a message as I did
Théo Winterhalter (Jan 05 2021 at 12:46):Done!
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.
Théo Zimmermann (Jan 05 2021 at 15:15):Done.
Théo Zimmermann (Jan 05 2021 at 15:16):BTW, will you be able to request more aliases in the future (like for Dune)?
Théo Zimmermann (Jan 05 2021 at 15:16):And wouldn't coqidetop / coqtop be required for VSCoq / PG to work?
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.
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.
Enrico Tassi (Jan 05 2021 at 15:32):IIRC dune is a self contained binary, no extra file is needed I think
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.
Paolo Giarrusso (Jan 05 2021 at 17:18):what about a coqc alias?
Karl Palmskog (Jan 05 2021 at 17:18):yeah, without that everyone who doesn't use coq_makefile will see their projects fail, right?
Karl Palmskog (Jan 05 2021 at 17:19):let's just say that there are many horrible makefiles out there that directly use coqc
Paolo Giarrusso (Jan 05 2021 at 17:22):does coq_makefile even deal with different names? or do you mean make COQC=... will work?
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
Karl Palmskog (Jan 05 2021 at 17:23):coq_makefile uses $(COQBIN)coqc, and I believe he sets $(COQBIN) in the snap
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.
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.
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").
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.
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: Jun 10 2023 at 06:31 UTC