Julin S (Jul 05 2022 at 06:54): 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.)
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 ?
Julin S (Jul 05 2022 at 07:10):No I hadn't got multiple ocaml. Only the one that came with the OS (ubuntu).
Julin S (Jul 05 2022 at 07:11):But am now trying to make a new one with opam.
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?
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.
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.
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?
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
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?
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
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.)
Paolo Giarrusso (Jul 05 2022 at 09:36):This message still shows the warnings Enrico mentioned
Paolo Giarrusso (Jul 05 2022 at 09:40):can you show the output of which coqc from this shell (after eval $(opam env) )?
Julin S (Jul 05 2022 at 12:01):Got this:
$ eval $(opam env)
$ which coqc
/home/famubu/.opam/coq/bin/coqc
I think this error may have been due to a space in the path to files.
It worked fine when there was no space.
Notification Bot (Jul 06 2022 at 06:06):Julin S has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC