Stream: Coq users

Topic: compiling compcert

Simon Hudon (Jul 02 2020 at 16:03):

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[2]: *** [ccomp] Error 2
make[1]: *** [ccomp] Error 2
make: *** [all] Error 2

Karl Palmskog (Jul 02 2020 at 16:05):

have you installed menhirLib via regular OPAM? It's not part of Coq's repo.

Simon Hudon (Jul 02 2020 at 16:05):

I have the following versions:

MENHIR_VERSION=20200123
MENHIR_LIB_VERSION=20200123
COMPCERT_VERSION=3.6
COQ_VERSION=8.9.1

Simon Hudon (Jul 02 2020 at 16:06):

Yes, exactly

Simon Hudon (Jul 02 2020 at 16:07):

(i.e. using OPAM)

Karl Palmskog (Jul 02 2020 at 16:07):

looks like you're using a bundled version of menhirLib which hasn't been compiled with clang and so on

Simon Hudon (Jul 02 2020 at 16:08):

How do I fix that?

Karl Palmskog (Jul 02 2020 at 16:09):

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)

Karl Palmskog (Jul 02 2020 at 16:10):

https://github.com/ocaml/opam-repository/blob/master/packages/menhirLib/menhirLib.20200123/opam

Karl Palmskog (Jul 02 2020 at 16:13):

but I think the only person who truly knows the ins and outs of CompCert compilations is @Michael Soegtrop

Simon Hudon (Jul 02 2020 at 16:31):

Thanks

Simon Hudon (Jul 02 2020 at 16:32):

Is it common to have packages that are so hard to configure and compile with Coq / OPAM?

Karl Palmskog (Jul 02 2020 at 16:47):

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

Simon Hudon (Jul 02 2020 at 16:50):

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

Simon Hudon (Jul 02 2020 at 16:52):

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?

Karl Palmskog (Jul 02 2020 at 16:57):

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

Paolo Giarrusso (Jul 02 2020 at 17:04):

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

Simon Hudon (Jul 02 2020 at 17:08):

I have feeling that when I try new software, I have a habit of stepping on every single rake lying around

Paolo Giarrusso (Jul 02 2020 at 17:12):

Sounds like you’re a great tester! https://blog.regehr.org/archives/861 suggests that some users are more prone to this.

Paolo Giarrusso (Jul 02 2020 at 17:12):

Also, that’s funny reading :-)

Simon Hudon (Jul 02 2020 at 17:12):

Thanks! :) That's a very kind way of rephrasing it

Paolo Giarrusso (Jul 02 2020 at 17:15):

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.

Paolo Giarrusso (Jul 02 2020 at 17:17):

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

Simon Hudon (Jul 02 2020 at 17:18):

Thanks!

Simon Hudon (Jul 02 2020 at 17:19):

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

Paolo Giarrusso (Jul 02 2020 at 17:31):

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.

Paolo Giarrusso (Jul 02 2020 at 17:33):

And CompCert and VST _are_ doing that to an extent — they’re actually dealing with a big subset of C!

Last updated: Oct 13 2024 at 01:02 UTC