Fallback for coqtop

[Zimmi48]

Hello,

The Coq platform is now available as a Snap package. As explained in coq-community/vscoq#192, when Coq is installed that way, the name of the coqtop / coqidetop executables are prepended with coq-prover. It would be great if Proof-General could test these name as default fallbacks when coqtop / coqidetop are not available so that users have a good experience when installing Coq that way.

Thanks!

[cpitclaudel]

I see requests for aliases for coqide on https://forum.snapcraft.io/t/aliases-request-for-coq-prover/21925 ; why not for coqtop/coqidetop?

[Zimmi48]

We could have requested these additional aliases indeed (and we still can), but @gares considered that as these are internal executables, this didn't matter as much. There are not that many user interfaces to adapt either. But feel free to disagree and to open a request for new aliases instead.

[cpitclaudel]

No disagreement — I won't have time to do either ^^

[Zimmi48]

Would some other PG maintainer be available to implement this?

[erikmd]

Hi, as far as I am concerned I'd really prefer we add some additional aliases so that coqtop and coqidetop are in the PATH, to limit the increase of PG's bookkeeping w.r.t. finding the proper path of the coqtop binary (as this code is already involved, and will become further intricate when finalizing/integrating PG/xml − in particular depending on the output of coqtop -v, PG can adjust its behavior w.r.t. the version of Coq, and it will also need to run a coqotop or coqidetop session depending on that version); so I guess that further aliases would be a much simpler solution.
Also IIUC, it would enhance backward compatibility to some extent (coqtop will be in the PATH so Coq Platform users could do tiny tests just by running rlwrap coqtop).
Unfortunately I'm swamped this week so I can't promise an ETA… maybe @hendriktews or @Matafou would have the time to open the PR you are mentioning?

[gares]

Asking for aliases can be done by anyone, not just me, but it is better to synchronize since the procedure requires the request to get 2 positive votes, so one cannot do it alone either. See https://forum.snapcraft.io/t/aliases-request-for-coq-prover/21925 for and example of the procedure to follow.

[Zimmi48]

Two PG maintainers saying the same thing is enough to me. I can take care of opening the request for more aliases based on this feedback.

[gares]

Beware that coqidetop has a .opt extension (if you ask, ask for both), I mean, vscoq (and coqide) load coqidetop.opt, not coqidetop:
https://github.com/coq-community/vscoq/blob/c2d0f95483404f050577d95a76947c33f0d25b90/package.json#L70

So the aliases should be

• coq-prover.coqidetop -> coqidetop.opt (makes me p...)
• coq-prover.coqtop -> coqtop

[gares]

(this was another reason I was not in love with these aliases)

[Matafou]

I guess I can propose a PR that also tries coq-prover.coqtop and coq-prover.coqc as possible executable names. But definitely not happy with such adhoc code.

Shouldn't we (IDE developpers) rather come up with some common shell variable name to look at when looking for coq{top,c,...}?

[gares]

Well, there is indeed PATH, but the "confinement" of snap packages gets in the way.

Between the lines I read that PG also calls coqc, is that right? (better to make just one request for all the aliases we want)

[Matafou]

Yes, during auto-compilation of "Requires". Actually we also need coqdep.
@hendriktews do you confirm? Is there another executable from coq needed for autocompilation?

[hendriktews]

Yes, auto compilation calls coqc and coqdep.

[hendriktews]

... and for 8.9.1 or before it may also call coqtop -schedule-vio2vo. No other executable.

[Zimmi48]

coqtop, coqidetop, coqc and coqdep is a long list of aliases to ask in addition to coqide and coq_makefile which have already been granted. I don't know how Snap gatekeepers will react to this request but it seems to go a little against their philosophy of limiting how a Snap package can affect the PATH. Would it also be an option to export only coqtop and that PG runs $(coqtop -where)/../../bin/coqc, $(coqtop -where)/../../bin/coqdep, etc.? This could also be useful BTW to users that override coq-prog-name to give an absolute path to this command.

[Matafou]

If this works on all systems it looks like a very good solution.

[hendriktews]

In the end, PG can follow all the proposals mentioned so far in this issue. The question is the relative effort and if there is somebody willing to implement and maintain it. I have not looked into how complicated it is to apply for aliases, but to me it seems to be the solution that requires the least effort. Would it be possible to apply for the aliases, and if that fails implement one of the proposals made so far?

[Zimmi48]

Would it be possible to apply for the aliases, and if that fails implement one of the proposals made so far?

Sure. I'll do that next week, unless someone else wants to take care of it.

[Zimmi48]

The additional aliases having been granted, this issue can now be closed.

[Matafou]

Thanks for the work @Zimmi48.

[hendriktews]

Thanks!