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
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.
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..)
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
Ah! Thanks! Let me try that.
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
OK, loading that file does not seem to work for me. I'm hopeless with
emacs, so I might be doing something wrong.
note that the file only has an effect when opening files in the coq repo itself
Yeah, that is what I am doing. My file is at the root though.
if you want we can do a visio where you share screen, might be easier to debug
Thanks, that might be useful. Let me just try a bit harder first.
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:
Rodolphe Lepigre has marked this topic as resolved.
Last updated: Nov 29 2023 at 21:01 UTC