Stream: Coq users

Topic: `coqc` can find the libraries but Proof General cannot

Simon Hudon (Jun 30 2020 at 15:16):

I'm building the VST project right now and there was a lot of trial and error. Now, I got the whole thing to build using their Makefile and their _CoqProject file but Proof General still can't step through a file. The VST documentation recommends I put this in my init.el file:

(custom-set-variables '(coq-prog-args '(
"-R" "/Users/simon/lean/VST/compcert" "-as" "compcert"
"-R" "/Users/simon/lean/VST/msl" "-as" "msl"
"-R" "/Users/simon/lean/VST/veric" "-as" "veric"
"-R" "/Users/simon/lean/VST/floyd" "-as" "floyd"
"-R" "/Users/simon/lean/VST/progs" "-as" "progs"
"-R" "/Users/simon/lean/VST/sepcomp" "-as" "sepcomp"
"-emacs"
)))

(setq coq-load-path '(("/Users/simon/lean/VST/compcert" "compcert")
                  ("/Users/simon/lean/VST/msl" "msl")
                  ("/Users/simon/lean/VST/veric" "veric")
                  ("/Users/simon/lean/VST/floyd" "floyd")
                  ("/Users/simon/lean/VST/progs" "progs")
                  ("/Users/simon/lean/VST/sepcomp" "sepcomp") ))

Still, the compcert files (included in VST) can't be run by Proof General. What should I try next?

Paolo Giarrusso (Jun 30 2020 at 19:32):

“-as” sounds very weird there, and _CoqProject should usually have all the needed information

Paolo Giarrusso (Jun 30 2020 at 19:35):

Indeed, that’s what https://github.com/PrincetonUniversity/VST/blob/master/BUILD_ORGANIZATION.md#with-proof-general says

Paolo Giarrusso (Jun 30 2020 at 19:36):

I suppose you’re using a different version of VST, but then you’ll need to show which documentation you’re using. What I link also suggests -Q over -R.

Paolo Giarrusso (Jun 30 2020 at 19:40):

(But I don’t use VST in particular, I opened the topic because of the generic title!)

Paolo Giarrusso (Jun 30 2020 at 19:41):

Unless VST developers show up here (and I haven’t seen many), I expect you might have to describe which versions you’re using, what you’ve done and what you’re seeing in more detail.

Simon Hudon (Jun 30 2020 at 19:44):

I might have gotten turned around with the various versions of the documentation. I'm now using the v2.5 tag which also specifies -Q rather than -R

Paolo Giarrusso (Jun 30 2020 at 19:45):

Also, fwiw, https://coq.inria.fr/refman/practical-tools/coq-commands.html#command-line-options documents what those options mean for the latest coq release (but make sure to pick the right versions!)

Simon Hudon (Jun 30 2020 at 19:45):

(sorry for luring you with overly general topic, I was hoping there might be a Coq / proof general skill that I'm lacking that could help)

Paolo Giarrusso (Jun 30 2020 at 19:47):

No no worries, it’s just that I might need more info :-)

Paolo Giarrusso (Jun 30 2020 at 19:47):

For those docs, I’d remove all the changes to the emacs config that you posted (and restart emacs to be sure)

Paolo Giarrusso (Jun 30 2020 at 19:48):

Now, I don’t get why they have different CoqProject files, and which one to use

Simon Hudon (Jun 30 2020 at 19:48):

(additional note: I took those settings from https://github.com/PrincetonUniversity/VST/blob/v2.5/doc/INSTALL.md#instructions-for-os-x which specifies "-R" but I now think this file is outdated and should have been deleted a while ago)

Simon Hudon (Jun 30 2020 at 19:50):

What is the effect of using multiple _CoqProject file with Proof General? Does it help at all?

Paolo Giarrusso (Jun 30 2020 at 19:50):

No clue! Here’s what a more common setup looks like https://github.com/Blaisorblade/dot-iris/blob/master/_CoqProject#L1

Paolo Giarrusso (Jun 30 2020 at 19:51):

So, options, and maybe a list of files

Paolo Giarrusso (Jun 30 2020 at 19:51):

ignore the -arg -w part, that sets warning options

Paolo Giarrusso (Jun 30 2020 at 19:52):

Now, what’s in the generated files? Can you post them, dunno, on a gist?

Paolo Giarrusso (Jun 30 2020 at 19:53):

I agree that the instructions you just linked seem VERY outdated and deserve a bug report or PR

Paolo Giarrusso (Jun 30 2020 at 19:53):

And you might have to undo what you did following those instructions, in general (can’t divine the details)

Karl Palmskog (Jun 30 2020 at 19:56):

VST is known to be difficult to build and install, there is a discussion here on doing it automatically via OPAM: https://github.com/PrincetonUniversity/VST/pull/406

Karl Palmskog (Jun 30 2020 at 19:57):

specifying -R or -Q options in the emacs config is legacy behavior, basically what was state of the art 10 years ago

Simon Hudon (Jun 30 2020 at 19:58):

Here is the _CoqProject being generated: https://gist.github.com/cipher1024/de4158b78832a036c9c3e28736eff793

Paolo Giarrusso (Jun 30 2020 at 19:58):

It also seems they should delete https://github.com/PrincetonUniversity/VST/blob/master/pg , dunno? The “new” docs I linked suggest using a “coqide” script that’s not committed, dunno if that’s up-to-date

Simon Hudon (Jun 30 2020 at 20:00):

@Karl Palmskog Do you know what the suggested setup is for Proof General?

Paolo Giarrusso (Jun 30 2020 at 20:00):

Hm, that file looks like it could be correct... can you step through, dunno, some basic file like msl/base.v? What error do you get if not?

Karl Palmskog (Jun 30 2020 at 20:02):

Simon Hudon said:

Karl Palmskog Do you know what the suggested setup is for Proof General?

for VST? no idea. If I did anything with VST, I would try to get it installed into user-contribs so I didn't have to worry about setting -Q/-R

Gaëtan Gilbert (Jun 30 2020 at 20:03):

-as is old stuff https://github.com/coq/coq/commit/6599e31f04b6e8980de72e9d3913b70c04b6698c

Paolo Giarrusso (Jun 30 2020 at 20:04):

Right, luckily both -R and -as aren’t part of the “new” docs https://github.com/PrincetonUniversity/VST/blob/master/BUILD_ORGANIZATION.md#with-proof-general

Simon Hudon (Jun 30 2020 at 20:05):

sorry for the delays in answering your question @Paolo G. Giarrusso, I'm fighting with opam to set the right switch

Paolo Giarrusso (Jun 30 2020 at 20:07):

@Simon Hudon no worries; since you mention you can’t step through compcert, I must say that the old and new instructions seem pretty different about installing CompCert, so there’s no way to know here if after your “trial and error” things are setup correctly or not

Karl Palmskog (Jun 30 2020 at 20:09):

projects relying on CompCert seem to have a high difficulty curve in general w.r.t. building for external users (also as CompCert evolves)

Simon Hudon (Jun 30 2020 at 20:10):

My understanding is that, the new way of working with CompCert for VST is that it has compcert directory and the Coq sources are there and I don't need other setups

Paolo Giarrusso (Jun 30 2020 at 20:10):

yeah, it seems you shouldn’t need other setups

Karl Palmskog (Jun 30 2020 at 20:10):

it can be built both with CompCert vendored or with system-installed CompCert

Karl Palmskog (Jun 30 2020 at 20:10):

but the configuration differences are very subtle

Paolo Giarrusso (Jun 30 2020 at 20:11):

if you haven’t setup some project before, _maybe_ you should try setting up some simpler library first — say, checkout https://gitlab.mpi-sws.org/iris/stdpp (biased choice, but I know it works and takes 1-2 minutes to build), run make -j2, open a file in Proof General (without any special configuration, and remove ), and confirm you can step through it.

Paolo Giarrusso (Jun 30 2020 at 20:12):

*remove any customization to proof general done following old vst instructions

Paolo Giarrusso (Jun 30 2020 at 20:13):

depending on the trial and error on VST, you might need a clean install, I don’t know, sorry :-(

Paolo Giarrusso (Jun 30 2020 at 20:15):

often, if I’m not sure docs are up-to-date, I check the scripts run by the CI, but for some reason they seem much more complex than what they suggest users to do, so I’m not sure there either :-(

Paolo Giarrusso (Jun 30 2020 at 20:15):

hope this helps, sorry if it doesn’t

Simon Hudon (Jun 30 2020 at 20:15):

The travis scripts is also usually my plan B

Simon Hudon (Jun 30 2020 at 20:15):

It does, thanks!

Simon Hudon (Jun 30 2020 at 20:26):

Iris and the iris tutorial as well as software foundations worked before. My installation of Iris in opam now seems broken

Simon Hudon (Jun 30 2020 at 20:28):

(both in Proof General and when trying to build the iris tutorial on the command line)

Paolo Giarrusso (Jun 30 2020 at 20:56):

Iris is a much more regular package

Paolo Giarrusso (Jun 30 2020 at 20:57):

But if you tweaked opam settings that might be a problem?

Simon Hudon (Jun 30 2020 at 20:57):

I think the issue was with opam switch link

Paolo Giarrusso (Jun 30 2020 at 20:58):

Maybe, no crystal ball :-)

Simon Hudon (Jun 30 2020 at 20:58):

What is the standard way to get the right version of Coq when switching projects?

Simon Hudon (Jun 30 2020 at 20:58):

(it seems to be building fine now)

Paolo Giarrusso (Jun 30 2020 at 20:58):

Say, if building the iris tutorial fails, either you need a make clean, or your checkout requires a version different from the one in your switch...

Paolo Giarrusso (Jun 30 2020 at 20:59):

Well, to use a project, installing it from opam is the simplest thing if possible

Simon Hudon (Jun 30 2020 at 21:00):

Yeah both Proof General and the Makefile work with Iris. But they're in a separate switch. They use Coq 8.11 whereas my VST setup uses Coq 8.10

Paolo Giarrusso (Jun 30 2020 at 21:00):

If two projects require incompatible dependencies and I cannot “sync” them, I create different switches

Simon Hudon (Jun 30 2020 at 21:01):

I'm with you so far, I have different switches for different versions of Coq but I have to remember which project uses which. Can I have a default switch given a certain directory?

Paolo Giarrusso (Jun 30 2020 at 21:01):

And then I don’t change globally the default, but either change per shell with eval $(opam env --with-switch wanted_switch --set-switch)

Paolo Giarrusso (Jun 30 2020 at 21:01):

_or_ use opam switch link

Paolo Giarrusso (Jun 30 2020 at 21:01):

_but_

Paolo Giarrusso (Jun 30 2020 at 21:02):

that’s loaded by eval $(opam env), not automatically, unless you _also_ setup the opam shell hooks correctly

Paolo Giarrusso (Jun 30 2020 at 21:02):

opam has an option for doing that automatically, which I use, but I remember some concerns

Paolo Giarrusso (Jun 30 2020 at 21:06):

IIRC, the concern was that opam advises loading .bash_profile or .profile from .bashrc, which is backward (and would sometimes cause an infinite loop)

Simon Hudon (Jun 30 2020 at 21:07):

oh

Paolo Giarrusso (Jun 30 2020 at 21:07):

still, what opam itself does works for many people — if it doesn’t for you, that needs another discussion

Paolo Giarrusso (Jun 30 2020 at 21:07):

also, opam _advises_ that part, doesn’t do it automatically

Paolo Giarrusso (Jun 30 2020 at 21:08):

so setting up the shell hook is at least safe, it just might not always work

Simon Hudon (Jun 30 2020 at 21:08):

Let's say I'm in emacs and I open a file. How do I set the right switch for that file? calling opam switch ... and eval $(opam ...) from a shell within emacs doesn't seem to cut iit

Paolo Giarrusso (Jun 30 2020 at 21:08):

(for details on this, see https://github.com/ocaml/opam/issues/4201)

Paolo Giarrusso (Jun 30 2020 at 21:08):

ah

Paolo Giarrusso (Jun 30 2020 at 21:09):

you need to get those settings right _outside_ Emacs

Paolo Giarrusso (Jun 30 2020 at 21:09):

open a shell, eval $(opam env), then start emacs

Paolo Giarrusso (Jun 30 2020 at 21:09):

for multiple projects at once, start multiple emacses

Simon Hudon (Jun 30 2020 at 21:10):

That's annoying. Mac OS X is not exactly friendly to having multiple instances of the same application open at once

Paolo Giarrusso (Jun 30 2020 at 21:10):

I honestly use vscoq for that, and vscoq supports _CoqProject and has other advantages (including async proofs!), but it’s still less mature (tho getting better rapidly)...

Paolo Giarrusso (Jun 30 2020 at 21:10):

that’s fine in macos

Paolo Giarrusso (Jun 30 2020 at 21:11):

you’ll get separate emacs icons in the dock

Paolo Giarrusso (Jun 30 2020 at 21:11):

but uh wait, I mean start emacs _from the shell_

Paolo Giarrusso (Jun 30 2020 at 21:11):

not from clicking some Emacs icon — that never loads the PATH set in the shell config

Paolo Giarrusso (Jun 30 2020 at 21:12):

(unless you have emacs packages that work around that, but even those can’t work decently with multiple opam switches!)

Simon Hudon (Jun 30 2020 at 21:13):

VS code is pretty popular in Lean too. How does it interact with the switches?

Paolo Giarrusso (Jun 30 2020 at 21:13):

you can configure the path to the coq binary in each workspace

Paolo Giarrusso (Jun 30 2020 at 21:14):

(you can also configure a default per-user)

Paolo Giarrusso (Jun 30 2020 at 21:15):

if you change the switch path (or rather, replace a switch by another) you have to change it manually in each affected workspace, but it’s fine for me

Simon Hudon (Jun 30 2020 at 21:15):

Interesting. Emacs has directory local variables. Maybe I can use that to set the path to the Coq directory. I would prefer that to setting up Coq before calling emacs

Paolo Giarrusso (Jun 30 2020 at 21:15):

(my switches are named after Coq version, so I never upgrade Coq in a switch, just create a separate switch and transition gradually; if I had 20 projects, I might pick a different workshop)

Paolo Giarrusso (Jun 30 2020 at 21:16):

never tried it, but sounds plausible, and you can tell Proof General the path to Coq IIRC

Paolo Giarrusso (Jun 30 2020 at 21:18):

Btw, since you’re on Mac, I know that on Mac the .profile doesn’t load .bashrc as it should (and as is standard on Linux). I copied code from Debian for it. But not advised if you don’t know enough bash (the needed code is subtle!)

Simon Hudon (Jun 30 2020 at 21:20):

I remember I had to mess around a bit with .profile / .bashrc to get the right environment in emacs. I don't remember what ended up doing the trick though

Simon Hudon (Jun 30 2020 at 21:35):

Update: in .dir-locals.el, I set coq-prog-name, coq-compiler and coq-dependency-analyzer and that works.

Simon Hudon (Jun 30 2020 at 21:36):

I wonder if I could create a hook on coq-mode that would set them in accordance with the switch I set with opam switch link

Simon Hudon (Jun 30 2020 at 21:44):

Back to our point, msl/base.v works in proof general now

Simon Hudon (Jun 30 2020 at 21:44):

If I try progs/tutorial1.v I get the following error:

*** Warning: in file /Users/simon/lean/VST/compcert/common/AST.v, library Coqlib is required and has not been found in the loadpath!
*** Warning: in file /Users/simon/lean/VST/compcert/common/AST.v, library Maps is required and has not been found in the loadpath!
*** Warning: in file /Users/simon/lean/VST/compcert/common/AST.v, library Errors is required and has not been found in the loadpath!
*** Warning: in file /Users/simon/lean/VST/compcert/common/AST.v, library Archi is required and has not been found in the loadpath!
/Users/simon/lean/VST/compcert/common/AST.vo /Users/simon/lean/VST/compcert/common/AST.glob /Users/simon/lean/VST/compcert/common/AST.v.beautified /Users/simon/lean/VST/compcert/common/AST.required_vo: /Users/simon/lean/VST/compcert/common/AST.v
/Users/simon/lean/VST/compcert/common/AST.vio: /Users/simon/lean/VST/compcert/common/AST.v

Erik Martin-Dorel (Jun 30 2020 at 22:07):

Hi @Simon Hudon, sorry I just skimmed this zulip stream, but I just wanted to say that indeed, switching between several opam switches directly from PG/Emacs (without restarting emacs!) is an increasingly common use case, and albeit the PG team focused on other features in the past few months, we plan to focus at this this feature soon (there is already an open issue for that in the PG tracker: https://github.com/ProofGeneral/PG/issues/481)

In the meantime, a workaround without restarting emacs consists in changing the coq-prog-name variable by typing: M-: (setq coq-prog-name ".../coqtop") RET, then typing C-u C-c C-x then C-c C-n in a .v buffer

Simon Hudon (Jun 30 2020 at 22:12):

Hi @Erik Martin-Dorel That's wonderful thank you! What does C-u C-c C-x do? And I've never seen the ... notation in ".../coqtop". What does it mean?

Erik Martin-Dorel (Jun 30 2020 at 22:14):

sorry I didn't elaborate on the path string, actually by ... I just meant the complete path of the coqtop binary.
I.e., you could do in a terminal:

$ opam switch your-switch-name
$ eval $(opam env)
$ which coqtop

and paste the full path of coqtop into the elisp command (setq coq-prog-name "...")

Erik Martin-Dorel (Jun 30 2020 at 22:17):

Regarding C-u C-c C-x, the C-u (ctrl+u) command is standard in Emacs to prefix an existing binding (C-c C-x here) and modify it, a bit like an "argument".
To have more details on C-c C-x, you can just do:
C-h k C-c C-x and you get:

C-c C-x runs the command proof-shell-exit (found in coq-mode-map),
which is an interactive Lisp function in ‘proof-shell.el’.

It is bound to C-c C-x, <menu-bar> <Coq> <Exit Coq>.

(proof-shell-exit &optional DONT-ASK)

Query the user and exit the proof process.

This simply kills the ‘proof-shell-buffer’ relying on the hook function

‘proof-shell-kill-function’ to do the hard work.  If optional
argument DONT-ASK is non-nil, the proof process is terminated
without confirmation.

The kill function uses ‘<PA>-quit-timeout’ as a timeout to wait
after sending ‘proof-shell-quit-cmd’ before rudely killing the process.

This function should not be called if
‘proof-shell-exit-in-progress’ is t, because a recursive call of
‘proof-shell-kill-function’ will give strange errors.

so one can guess here that thanks to the prefix C-u, the interactive keybinding amounts to pass a non-nil argument to DONT-ASK, namely C-u C-c C-x is a variant of C-c C-x that does not prompt with the question Exit Coq process? (yes or no)

Simon Hudon (Jun 30 2020 at 22:24):

Thanks for the explanation!

Paolo Giarrusso (Jun 30 2020 at 23:26):

@Simon Hudon for the errors on tutorial, it sounds like Coqlib etc. are neither installed globally, nor listed in CoqProject

Paolo Giarrusso (Jun 30 2020 at 23:30):

Well, actually, the problem might be for compcert itself: it sounds like ProofGeneral is not finding AST.vo so it is trying to compile AST.v by itself, which it can do in simple cases, but won’t work for such a complex setting. that’s enabled by compile-before-require.

Simon Hudon (Jul 01 2020 at 00:22):

Ok, I think I found something that works. There is a _CoqProject file in compcert. When stepping through a file, Coq would crash. I thought of removing the file but then important files weren't found (e.g. Coqlib earlier). I went back to the _CoqProject file and looked at the crash report:

Fatal error: exception Sys_error("/Users/simon/lean/VST/compcert/MenhirLib: No such file or directory")

I deleted that entry from the _CoqProject. I got a few more crashes but by adjusting the _CoqProject file, in the end, I was able to step through AST.v

Simon Hudon (Jul 01 2020 at 00:27):

tutorial1.v still fails

Simon Hudon (Jul 01 2020 at 00:27):

New idea: copy the _CoqProject of compcert into that of VST

Paolo Giarrusso (Jul 01 2020 at 00:41):

Makes sense, but you need to adjust the physical paths (the first argument to -Q) but not the logical paths (since those appear in source files). Also, that assumes that the logical paths to compcert are the same in compcert and in vst, which is the obvious thing nowadays.

Paolo Giarrusso (Jul 01 2020 at 00:43):

Actually, ignore the last condition: it was a thinko, I don’t think you could set it up otherwise.

Simon Hudon (Jul 01 2020 at 00:43):

So far it seems to be working: adjusting the physical path but not the logical path

Simon Hudon (Jul 01 2020 at 00:44):

What would break if the logical path inside a package was not the same as the one outside?

Paolo Giarrusso (Jul 01 2020 at 00:45):

the logical path is stored in the vo file, so coq will refuse to load a vo file with a mismatching logical path

Simon Hudon (Jul 01 2020 at 00:46):

Nice!

Paolo Giarrusso (Jul 01 2020 at 00:46):

So if you compile foo.v without any -Q, so its logical name is foo, but try to load it with name bar.foo, you might be able to make coq find it, but not load it.

Paolo Giarrusso (Jul 01 2020 at 00:47):

Iirc the error will mention both logical paths, and it’s a classic symptom of problems with -Q setup.

Simon Hudon (Jul 01 2020 at 00:51):

That's a nice solution

Simon Hudon (Jul 01 2020 at 00:55):

Lean 3 has a single space of logical names and it has to match the physical structure exactly. So far we haven't had trouble but it seems like trouble isn't too far off. In Lean 4, all the logical names are prefixed by the library name and then it matches exactly the directory structure. I think that should be simple to manage

Last updated: Oct 03 2023 at 21:01 UTC