After days of fiddling around, I finally found a combination of versions for Coq, MenhirLib and compcert so that I can verify the Coq files successfully. Now I'm trying to extract the ML code and compile it and I get this error:
Linking ccomp clang: error: no such file or directory: '/Users/simon/.opam/coq-8.9/lib/menhirLib/menhirLib.o' File "caml_startup", line 1: Error: Error during linking make: *** [ccomp] Error 2 make: *** [ccomp] Error 2 make: *** [all] Error 2
have you installed menhirLib via regular OPAM? It's not part of Coq's repo.
I have the following versions:
MENHIR_VERSION=20200123 MENHIR_LIB_VERSION=20200123 COMPCERT_VERSION=3.6 COQ_VERSION=8.9.1
(i.e. using OPAM)
looks like you're using a bundled version of menhirLib which hasn't been compiled with clang and so on
How do I fix that?
you could try to compile menhirLib in isolation I guess, and see if it generates the required
.o file. Specifically, menhirLib is compiled via dune (which I believe then calls clang for the required compilation)
but I think the only person who truly knows the ins and outs of CompCert compilations is @Michael Soegtrop
Is it common to have packages that are so hard to configure and compile with Coq / OPAM?
yes, the whole Coq/OCaml ecosystem is very complex, and there are multiple interactions between C/C++ compilers, linkers, the OCaml compiler, the build system(s), etc. For example, some OCaml packages require the presence of system packages, that are different on Linux/macOS and on ARM/x86/...
It also looks like you have to hand pick the version of every package. It would be great to have like
stack or even
cabal where a set of versions are chosen for you
Progress: using coq 8.9.1, I managed to do
opam install coq-compcert and it seems to be working. Bad news: if I select a different switch with a different version of Coq, (e.g. 8.10) I'm not able to install or even call
compcert. Is there a way for
opam to install the executable globally?
you can usually find the executable in
.opam/<switch-name>/<path-to-exec>, and in some cases it executes without having the PATH set to the switch path...
@Simon Hudon I’ve never tried extraction, but I’ve never seen so much trouble as you described here. OTOH, CompCert and VST got started earlier and are big and complex, which doesn’t help.
I have feeling that when I try new software, I have a habit of stepping on every single rake lying around
Sounds like you’re a great tester! https://blog.regehr.org/archives/861 suggests that some users are more prone to this.
Also, that’s funny reading :-)
Thanks! :) That's a very kind way of rephrasing it
I will admit that typical CLI/Unix tools are often not friendly to “trial and error”, but nobody (should) expect theorem prover users to be command-line experts. Making things usable is just lots of work, and something that seldom happens in academic software.
(I also sent a quick PR for https://github.com/PrincetonUniversity/VST/pull/435, hopefully addressing your report; thank goodness for GitHub’s PRs from the web interface).
You're very right about how hard and time consuming it is to make software usable. I have long felt like it made it embarrassing in academia to identify as software engineering experts: we know all about making great software except we don't make great software. Well ... there's no money for it
We’re getting OT, but engineering proper tools _is_ an existing strategy, just a risky and an uncommon one. I suspect it might work better in theorem proving, since your users are likely to be academics who cite your work.
And CompCert and VST _are_ doing that to an extent — they’re actually dealing with a big subset of C!
Last updated: Oct 03 2023 at 20:01 UTC