Stream: Coq devs & plugin devs

Topic: ✔ Using PG from the Coq repo


view this post on Zulip Rodolphe Lepigre (Jul 12 2023 at 12:08):

Is there documentation somewhere on how to step through files using PG from the Coq repository? I tried to do:

PATH=$PWD/_build/default/dev/shim:$PATH COQPATH=$PWD/_build/default/theories:$PWD/_build/default/user-contrib emacs test.v

but it seems that emacs overrides the PATH with the opam configuration, so this does not pick up the right coqtop.

view this post on Zulip Rodolphe Lepigre (Jul 12 2023 at 12:09):

I know I can probably set some variable in the PG config, and give it an absolute path to the coqtop shim, but I'd rather avoid having to do that manually each time.

view this post on Zulip Janno (Jul 12 2023 at 12:10):

I haven't actually found a way to make it work even with manual intervention because every time the coqtop process is restarted by PG it seems to recalculate all the variables from the opam configuration (or from something else, I don't understand how it works..)

view this post on Zulip Gaëtan Gilbert (Jul 12 2023 at 12:11):

If you load https://github.com/coq/coq/blob/master/dev/tools/coqdev.el it should auto set the path to the shim when in files in the coq repo
for files outside the coq repo I have (setq proof-prog-name-ask t) in my config and the absolute shim path in shell-command-history

view this post on Zulip Rodolphe Lepigre (Jul 12 2023 at 12:12):

Ah! Thanks! Let me try that.

view this post on Zulip Gaëtan Gilbert (Jul 12 2023 at 12:14):

but it seems that emacs overrides the PATH with the opam configuration, so this does not pick up the right coqtop.

that's probably something in your config, my emacs doesn't override PATH AFAICT

view this post on Zulip Rodolphe Lepigre (Jul 12 2023 at 12:18):

OK, loading that file does not seem to work for me. I'm hopeless with emacs, so I might be doing something wrong.

view this post on Zulip Gaëtan Gilbert (Jul 12 2023 at 12:20):

note that the file only has an effect when opening files in the coq repo itself

view this post on Zulip Rodolphe Lepigre (Jul 12 2023 at 12:20):

Yeah, that is what I am doing. My file is at the root though.

view this post on Zulip Gaëtan Gilbert (Jul 12 2023 at 12:21):

if you want we can do a visio where you share screen, might be easier to debug

view this post on Zulip Rodolphe Lepigre (Jul 12 2023 at 12:21):

Thanks, that might be useful. Let me just try a bit harder first.

view this post on Zulip Rodolphe Lepigre (Jul 12 2023 at 12:23):

OK, I managed to make it work. I did not get that you need to load the coqdev.el before you even visit the file. :sweat_smile:

view this post on Zulip Notification Bot (Jul 12 2023 at 12:43):

Rodolphe Lepigre has marked this topic as resolved.


Last updated: May 20 2024 at 20:01 UTC