Stream: Coq users

Topic: compiling compcert


view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jul 02 2020 at 16:05):

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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jul 02 2020 at 16:06):

Yes, exactly

view this post on Zulip Simon Hudon (Jul 02 2020 at 16:07):

(i.e. using OPAM)

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jul 02 2020 at 16:08):

How do I fix that?

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Jul 02 2020 at 16:10):

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

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jul 02 2020 at 16:31):

Thanks

view this post on Zulip 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?

view this post on Zulip 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/...

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 02 2020 at 17:12):

Also, that’s funny reading :-)

view this post on Zulip Simon Hudon (Jul 02 2020 at 17:12):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Simon Hudon (Jul 02 2020 at 17:18):

Thanks!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: Jan 27 2023 at 01:03 UTC