Stream: Coq users

Topic: ✔ coq plugin


view this post on Zulip Julin S (Jul 05 2022 at 06:54):

I was trying the most basic plugin in the plugin_tutorials at https://github.com/coq/coq/tree/v8.12/doc/plugin_tutorial/tuto0
for coq version 8.12

But when I ran make, it gave this error:

CAMLOPT -c -for-pack Tuto0_plugin src/g_tuto0.ml
File "src/g_tuto0.ml", line 1:
Error: /usr/local/lib/coq//vernac/mltop.cmi
is not a compiled interface for this version of OCaml.
It seems to be for a newer version of OCaml.
Makefile.coq:663: recipe for target 'src/g_tuto0.cmx' failed
make[1]: *** [src/g_tuto0.cmx] Error 2
Makefile.coq:338: recipe for target 'all' failed
make: *** [all] Error 2

Does anyone know why this may be coming?

I'm using the v8.12 branch.

(I could've sworn that this was working a couple of months back, but I may be wrong.)

view this post on Zulip Kenji Maillard (Jul 05 2022 at 06:58):

You seem to be using a different version of ocaml (older from what the error message says) than the one used to compile Coq. Do you have mutiple versions of ocaml installed on your computer ? For instance one installed with your distribution's package manager and the other with opam ?

view this post on Zulip Julin S (Jul 05 2022 at 07:10):

No I hadn't got multiple ocaml. Only the one that came with the OS (ubuntu).

view this post on Zulip Julin S (Jul 05 2022 at 07:11):

But am now trying to make a new one with opam.

view this post on Zulip Julin S (Jul 05 2022 at 07:11):

Hadn't got another ocaml with opam before, but had installed coq via opam. Does that pull in a separate ocaml as well?

view this post on Zulip Julin S (Jul 05 2022 at 07:12):

And is there a way to know which ocaml version would be acceptable in this case? The error just mentions version mismatch but not the expected version itself.

view this post on Zulip Julin S (Jul 05 2022 at 07:14):

Julin S said:

Hadn't got another ocaml with opam before, but had installed coq via opam. Does that pull in a separate ocaml as well?

Ah, looks like it does.

After doing the eval $(opam env), I got ocaml version 4.10.

view this post on Zulip Julin S (Jul 05 2022 at 07:17):

Thanks, using the opam ocaml got rid of that error.

Now the compilation progessed, but got another error.

COQDEP VFILES
COQPP src/g_tuto0.mlg
CAMLDEP src/tuto0_main.mli
OCAMLLIBDEP src/tuto0_plugin.mlpack
CAMLDEP src/tuto0_main.ml
CAMLDEP src/g_tuto0.ml
W: This Makefile was generated by Coq 8.12.0
W: while the current Coq version is 8.12.2
CAMLC -c src/tuto0_main.mli
CAMLOPT -c -for-pack Tuto0_plugin src/tuto0_main.ml
CAMLOPT -c -for-pack Tuto0_plugin src/g_tuto0.ml
CAMLOPT -pack -o src/tuto0_plugin.cmx
CAMLOPT -a -o src/tuto0_plugin.cmxa
CAMLOPT -shared -o src/tuto0_plugin.cmxs
COQC theories/Loader.v
File "./theories/Loader.v", line 1, characters 0-33:
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/media/famubu/New Volume1/gits/coq/doc/plugin_tutorial/tuto0/src/tuto0_plugin.cmxs: undefined symbol: camlTacticals__Pmakeblock_5370\")")

Makefile.coq:715: recipe for target 'theories/Loader.vo' failed
make[1]: *** [theories/Loader.vo] Error 1
Makefile.coq:338: recipe for target 'all' failed
make: *** [all] Error 2

Any idea what this one could be about?

view this post on Zulip Enrico Tassi (Jul 05 2022 at 08:22):

Hum, something fishy, see the warnings. You may have 2 similar but not identical version of Coq in you paths.
try make VERBOSE=1

view this post on Zulip Enrico Tassi (Jul 05 2022 at 08:23):

Any reason for using that old version of Coq by the way? I mean, you are recompiling it yourself, so why not pick a more recent one?

view this post on Zulip Julin S (Jul 05 2022 at 09:02):

No I'm not compiling coq itself. Just trying to run a 'hello world' coq plugin.

And some other wierd thing happened.

At one point, it actually seemed to work. But after doing a make clean it longer worked.

$ make
COQC theories/Loader.v
COQC theories/Demo.v
Hello world!
Hello world!
File "./theories/Demo.v", line 14, characters 0-13:
Warning: Hello world! [name,category]
File "./theories/Demo.v", line 18, characters 0-14:
Warning: Hello world! [name,category]

$ make
make[1]: Nothing to be done for 'real-all'.

$ coqc theories/Demo.
Warning: File "./theories/Demo." has been implicitly expanded to
"./theories/Demo..v" [file-no-extension,filesystem]
Error: Can't find file ./theories/Demo..v

$ coqc theories/Demo.v
File "./theories/Demo.v", line 1, characters 26-32:
Error: Cannot find a physical path bound to logical path matching suffix
<> and prefix Tuto0.

$ make
make[1]: Nothing to be done for 'real-all'.

$ make clean
makeCLEAN

$ make
COQDEP VFILES
COQPP src/g_tuto0.mlg
CAMLDEP src/tuto0_main.mli
OCAMLLIBDEP src/tuto0_plugin.mlpack
CAMLDEP src/tuto0_main.ml
CAMLDEP src/g_tuto0.ml
CAMLDEP src/tuto0_main.mli
CAMLDEP src/tuto0_main.ml
CAMLDEP src/g_tuto0.ml
CAMLDEP src/tuto0_main.mli
CAMLDEP src/tuto0_main.ml
CAMLDEP src/g_tuto0.ml
CAMLDEP src/tuto0_main.mli
CAMLDEP src/tuto0_main.ml
CAMLDEP src/g_tuto0.ml
CAMLOPT -c -for-pack Tuto0_plugin src/tuto0_main.ml
Makefile.coq:663: recipe for target 'src/tuto0_main.cmx' failed
make[1]: *** [src/tuto0_main.cmx] Error 127
Makefile.coq:338: recipe for target 'all' failed
make: *** [all] Error 2

view this post on Zulip Julin S (Jul 05 2022 at 09:08):

Output of make VERBOSE=1:

COQDEP VFILES
COQPP src/g_tuto0.mlg
CAMLDEP src/tuto0_main.mli
OCAMLLIBDEP src/tuto0_plugin.mlpack
CAMLDEP src/tuto0_main.ml
CAMLDEP src/g_tuto0.ml
W: This Makefile was generated by Coq 8.12.0
W: while the current Coq version is 8.12.2
CAMLC -c src/tuto0_main.mli
CAMLOPT -c -for-pack Tuto0_plugin src/tuto0_main.ml
CAMLOPT -c -for-pack Tuto0_plugin src/g_tuto0.ml
CAMLOPT -pack -o src/tuto0_plugin.cmx
CAMLOPT -a -o src/tuto0_plugin.cmxa
CAMLOPT -shared -o src/tuto0_plugin.cmxs
COQC theories/Loader.v
File "./theories/Loader.v", line 1, characters 0-33:
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/media/famubu/New Volume1/gits/coq/doc/plugin_tutorial/tuto0/src/tuto0_plugin.cmxs: undefined symbol: camlTacticals__Pmakeblock_5370\")")

Makefile.coq:715: recipe for target 'theories/Loader.vo' failed
make[1]: *** [theories/Loader.vo] Error 1
Makefile.coq:338: recipe for target 'all' failed
make: *** [all] Error 2

(I had deleted a previous message because I hadn't done eval $(opam env) there.)

view this post on Zulip Paolo Giarrusso (Jul 05 2022 at 09:36):

This message still shows the warnings Enrico mentioned

view this post on Zulip Paolo Giarrusso (Jul 05 2022 at 09:40):

can you show the output of which coqc from this shell (after eval $(opam env) )?

view this post on Zulip Julin S (Jul 05 2022 at 12:01):

Got this:

$ eval $(opam env)
$ which coqc
/home/famubu/.opam/coq/bin/coqc

view this post on Zulip Julin S (Jul 06 2022 at 06:06):

I think this error may have been due to a space in the path to files.

It worked fine when there was no space.

view this post on Zulip Notification Bot (Jul 06 2022 at 06:06):

Julin S has marked this topic as resolved.


Last updated: Jun 14 2024 at 18:01 UTC