Aliases request for coq-prover

store-requests
#1

Hello, I’m working on the coq-prover snap package and I’d like two aliases:

  • coq-prover.coqide -> coqide
  • coq-prover.coq-makefile -> coq_makefile

The former is what Coq users are used to type in order to start the classic Coq UI from a shell.

The latter is the command that the Coq documentation suggests to use in order to build a Coq project, it would be unhandy to use the long name, not to mention that people typically call that utility from Makefiles they write themselves.

Best

3 Likes
#2

Well, I made the request so I clearly vote +1

#3

Hi. I’d like to vote +1 as well. It’s always great to make Coq more accessible.

#4

+1 as reviewer - the publisher graciously agreed to register coq-prover which is more descriptive as a snap name, with the understanding that an alias could be granted so the commands would continue to be simply coq-*.

  • Daniel
1 Like
#5

+1 as a teacher who would benefit from this Snap package to get students install Coq on Linux as easily as it is on Windows and macOS.

2 Likes
#6

+1 for both — coqide is the standard name (also in docs), and coq_makefile is used not just by users, but is also hardcoded in many build scripts.

#7

+1 from me too for these aliases to provide the expected commands for coq. Thanks for the input from community members too.

+2 votes for, 0 votes against auto-aliases of coqide and coq_makefile - these are now live.

1 Like
#8

Is it possible to extend even more the list of aliases for coq-prover to the following ones?

  • coqtop -> coq-prover.coqtop
  • coqc -> coq-prover.coqc
  • coqdep -> coq-prover.coqdep
  • coqidetop.opt -> coq-prover.coqidetop

The plan was initially to have the editor support packages be adapted to know where to find these commands when they come from the Snap package but the maintainers of the one of the most used (the Emacs support package) are not very enthusiastic at the idea of adding logic dedicated to this specific distribution method (see https://github.com/ProofGeneral/PG/issues/541). So I’m coming with this new request that would allow any editor support package to work with the Coq software distributed via Snap out of the box.

#9

@roadmr Do you think this alias request is reasonable enough to grant or should we go back to the maintainers of the editor support plugins and insist that they extend their support to look for coq-prover prefixed binaries?

#10

hi, +1 from me as reviewer, I think it’s reasonable and expected for a well-known package like coq-prover to be able to provide its top level binaries as such, with an alias.

Maybe other @reviewers can chime in and/or look at this, since it’s been 12 days since it was filed.

  • Daniel
1 Like
#11

+1 from me as well, and I don’t see any possible clash with any other binaries.

#12

Thanks for the positive votes! Can we have these aliases live?

We will announce the very first stable release of our platform (namely 2021.02.0) very soon, and we will advertise the Snap package as well!

#13

+1 from me as well.

+3 votes for, 0 votes against, grant auto-aliases:

  • coqtop -> coq-prover.coqtop
  • coqc -> coq-prover.coqc
  • coqdep -> coq-prover.coqdep
  • coqidetop.opt -> coq-prover.coqidetop

for coq-prover - this is now live.

1 Like