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
(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?
“-as” sounds very weird there, and _CoqProject should usually have all the needed information
Indeed, that’s what https://github.com/PrincetonUniversity/VST/blob/master/BUILD_ORGANIZATION.md#with-proof-general says
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.
(But I don’t use VST in particular, I opened the topic because of the generic title!)
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.
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
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!)
(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)
No no worries, it’s just that I might need more info :-)
For those docs, I’d remove all the changes to the emacs config that you posted (and restart emacs to be sure)
Now, I don’t get why they have different CoqProject files, and which one to use
(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)
What is the effect of using multiple
_CoqProject file with Proof General? Does it help at all?
No clue! Here’s what a more common setup looks like https://github.com/Blaisorblade/dot-iris/blob/master/_CoqProject#L1
So, options, and maybe a list of files
ignore the -arg -w part, that sets warning options
Now, what’s in the generated files? Can you post them, dunno, on a gist?
I agree that the instructions you just linked seem VERY outdated and deserve a bug report or PR
And you might have to undo what you did following those instructions, in general (can’t divine the details)
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
-Q options in the emacs config is legacy behavior, basically what was state of the art 10 years ago
Here is the _CoqProject being generated: https://gist.github.com/cipher1024/de4158b78832a036c9c3e28736eff793
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
@Karl Palmskog Do you know what the suggested setup is for Proof General?
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?
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
-as is old stuff https://github.com/coq/coq/commit/6599e31f04b6e8980de72e9d3913b70c04b6698c
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
sorry for the delays in answering your question @Paolo G. Giarrusso, I'm fighting with
opam to set the right switch
@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
projects relying on CompCert seem to have a high difficulty curve in general w.r.t. building for external users (also as CompCert evolves)
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
yeah, it seems you shouldn’t need other setups
it can be built both with CompCert vendored or with system-installed CompCert
but the configuration differences are very subtle
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.
*remove any customization to proof general done following old vst instructions
depending on the trial and error on VST, you might need a clean install, I don’t know, sorry :-(
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 :-(
hope this helps, sorry if it doesn’t
The travis scripts is also usually my plan B
It does, thanks!
Iris and the iris tutorial as well as software foundations worked before. My installation of Iris in opam now seems broken
(both in Proof General and when trying to build the iris tutorial on the command line)
Iris is a much more regular package
But if you tweaked opam settings that might be a problem?
I think the issue was with
opam switch link
Maybe, no crystal ball :-)
What is the standard way to get the right version of Coq when switching projects?
(it seems to be building fine now)
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...
Well, to use a project, installing it from opam is the simplest thing if possible
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
If two projects require incompatible dependencies and I cannot “sync” them, I create different switches
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?
And then I don’t change globally the default, but either change per shell with
eval $(opam env --with-switch wanted_switch --set-switch)
opam switch link
that’s loaded by
eval $(opam env), not automatically, unless you _also_ setup the opam shell hooks correctly
opam has an option for doing that automatically, which I use, but I remember some concerns
IIRC, the concern was that opam advises loading .bash_profile or .profile from .bashrc, which is backward (and would sometimes cause an infinite loop)
still, what opam itself does works for many people — if it doesn’t for you, that needs another discussion
also, opam _advises_ that part, doesn’t do it automatically
so setting up the shell hook is at least safe, it just might not always work
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
(for details on this, see https://github.com/ocaml/opam/issues/4201)
you need to get those settings right _outside_ Emacs
open a shell,
eval $(opam env), then start emacs
for multiple projects at once, start multiple emacses
That's annoying. Mac OS X is not exactly friendly to having multiple instances of the same application open at once
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)...
that’s fine in macos
you’ll get separate emacs icons in the dock
but uh wait, I mean start emacs _from the shell_
not from clicking some Emacs icon — that never loads the PATH set in the shell config
(unless you have emacs packages that work around that, but even those can’t work decently with multiple opam switches!)
VS code is pretty popular in Lean too. How does it interact with the switches?
you can configure the path to the coq binary in each workspace
(you can also configure a default per-user)
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
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
(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)
never tried it, but sounds plausible, and you can tell Proof General the path to Coq IIRC
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!)
I remember I had to mess around a bit with
.bashrc to get the right environment in emacs. I don't remember what ended up doing the trick though
.dir-locals.el, I set
coq-dependency-analyzer and that works.
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
Back to our point,
msl/base.v works in proof general now
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
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
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?
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 "...")
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)
Thanks for the explanation!
@Simon Hudon for the errors on tutorial, it sounds like Coqlib etc. are neither installed globally, nor listed in CoqProject
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.
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
tutorial1.v still fails
New idea: copy the
compcert into that of
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.
Actually, ignore the last condition: it was a thinko, I don’t think you could set it up otherwise.
So far it seems to be working: adjusting the physical path but not the logical path
What would break if the logical path inside a package was not the same as the one outside?
the logical path is stored in the vo file, so coq will refuse to load a vo file with a mismatching logical path
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.
Iirc the error will mention both logical paths, and it’s a classic symptom of problems with -Q setup.
That's a nice solution
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: Jan 29 2023 at 06:02 UTC