Aliases request for coq-prover

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

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

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

+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

+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

+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.

+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