Stream: Coq devs & plugin devs

Topic: ✔ Using PG from the Coq repo

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.

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.

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

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

Rodolphe Lepigre (Jul 12 2023 at 12:12):

Ah! Thanks! Let me try that.

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

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.

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

Rodolphe Lepigre (Jul 12 2023 at 12:20):

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

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

Rodolphe Lepigre (Jul 12 2023 at 12:21):

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

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:

Notification Bot (Jul 12 2023 at 12:43):

Rodolphe Lepigre has marked this topic as resolved.

Last updated: Nov 29 2023 at 21:01 UTC