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
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.
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.
After a second try my registration was successful but I'm still waiting on the confirmation email.
Thanks for your effort!
Just liking the post counts as a vote?
I think you need to write a message as I did
Thanks! Just in case, more than 2 votes are actually a plus, if anyone else has the time.
BTW, will you be able to request more aliases in the future (like for Dune)?
coqtop be required for VSCoq / PG to work?
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.
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.
IIRC dune is a self contained binary, no extra file is needed I think
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.
what about a
yeah, without that everyone who doesn't use
coq_makefile will see their projects fail, right?
let's just say that there are many horrible makefiles out there that directly use coqc
coq_makefile even deal with different names? or do you mean
make COQC=... will work?
but I'm sure makefiles hard-coding
coq_makefile exist, and if that's bad I never knew it
coq_makefile uses $(COQBIN)coqc, and I believe he sets $(COQBIN) in the snap
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.
I see the snap package as a things for beginners. If you run your own build system, then you are not one IMO.
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").
Anyway, feel free to ask for more aliases in the forum if you think you will need it. I'm not against it.
coq_makefile (and dune) work that’s likely more than good enough, in case you download some project and want to
make install libraries. I’d also check Software Foundations, since it’s the primary use-case for beginners.
Last updated: Jan 29 2023 at 09:30 UTC