Stream: Coq devs & plugin devs

Topic: Plugin Tutorial

view this post on Zulip Seth Poulsen (Aug 23 2021 at 16:48):

Has anyone used the Plugin Tutorial lately? I'm trying to follow the instructions here: https://github.com/coq/coq/blob/master/doc/plugin_tutorial/README.md

But keep getting this error: 

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
File "src/g_tuto0.ml", line 2, characters 8-30:
2 | let _ = Mltop.add_known_module __coq_plugin_name
            ^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module Mltop
make[1]: *** [Makefile.coq:626: src/g_tuto0.cmx] Error 2
make: *** [Makefile.coq:327: all] Error 2

Thanks!

view this post on Zulip Seth Poulsen (Aug 23 2021 at 16:56):

I've tried checking out the last few major version branches (8.10-8.14), and I still get the same error.

view this post on Zulip Théo Zimmermann (Aug 23 2021 at 18:52):

Did you make sure that you have Coq installed and that you checked out the corresponding branch of the plugin tutorial?

view this post on Zulip Théo Zimmermann (Aug 23 2021 at 18:52):

It should still work since it is continuously tested, but it is possible that there are issues in the documented instructions.

view this post on Zulip Seth Poulsen (Aug 23 2021 at 19:00):

Yes, even if I am checked out on the branch of the exact version I have installed on my system (8.11 as of right now), I get this same error.

view this post on Zulip Hugo Herbelin (Aug 24 2021 at 16:02):

Seth Poulsen said:

Yes, even if I am checked out on the branch of the exact version I have installed on my system (8.11 as of right now), I get this same error.

Could you compile with make VERBOSE=1 and show a log?

view this post on Zulip Seth Poulsen (Aug 24 2021 at 18:21):

like this? 

$ make VERBOSE=1
make --no-print-directory -f "Makefile.coq" pre-all
if [ "8.11.0" != "8.11.0" ]; then\
  echo "W: This Makefile was generated by Coq 8.11.0";\
  echo "W: while the current Coq version is 8.11.0";\
fi
make --no-print-directory -f "Makefile.coq" real-all
"/usr/bin/ocamlfind" opt      -c  -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58   -safe-string -strict-sequence -I src  -I "/usr/lib/coq//config"  -I "/usr/lib/coq//lib"  -I "/usr/lib/coq//clib"  -I "/usr/lib/coq//kernel"  -I "/usr/lib/coq//library"  -I "/usr/lib/coq//engine"  -I "/usr/lib/coq//pretyping"  -I "/usr/lib/coq//interp"  -I "/usr/lib/coq//gramlib"  -I "/usr/lib/coq//gramlib/.pack"  -I "/usr/lib/coq//parsing"  -I "/usr/lib/coq//proofs"  -I "/usr/lib/coq//tactics"  -I "/usr/lib/coq//toplevel"  -I "/usr/lib/coq//printing"  -I "/usr/lib/coq//ide"  -I "/usr/lib/coq//stm"  -I "/usr/lib/coq//vernac"  -I "/usr/lib/coq//plugins/btauto"  -I "/usr/lib/coq//plugins/cc"  -I "/usr/lib/coq//plugins/derive"  -I "/usr/lib/coq//plugins/extraction"  -I "/usr/lib/coq//plugins/firstorder"  -I "/usr/lib/coq//plugins/fourier"  -I "/usr/lib/coq//plugins/funind"  -I "/usr/lib/coq//plugins/ltac"  -I "/usr/lib/coq//plugins/micromega"  -I "/usr/lib/coq//plugins/nsatz"  -I "/usr/lib/coq//plugins/omega"  -I "/usr/lib/coq//plugins/rtauto"  -I "/usr/lib/coq//plugins/setoid_ring"  -I "/usr/lib/coq//plugins/ssr"  -I "/usr/lib/coq//plugins/ssrmatching"  -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3  -for-pack Tuto0_plugin src/g_tuto0.ml
File "src/g_tuto0.ml", line 2, characters 8-30:
2 | let _ = Mltop.add_known_module __coq_plugin_name
            ^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module Mltop
make[1]: *** [Makefile.coq:626: src/g_tuto0.cmx] Error 2
make: *** [Makefile.coq:327: all] Error 2

view this post on Zulip Hugo Herbelin (Aug 25 2021 at 13:24):

Thanks!
What is the contents of /usr/lib/coq/vernac? Isn't there a file mltop.cmi there?
Also, what returns coqtop -config? Alternatively, where is coqtop or coqide located in your path?

view this post on Zulip Seth Poulsen (Aug 25 2021 at 21:24):

seth:~$ cat /usr/lib/coq/vernac
cat: /usr/lib/coq/vernac: No such file or directory
seth:~$ ls /usr/lib/coq
plugins  theories  tools  user-contrib
seth:~$ coqtop -config
LOCAL=0
COQLIB=/usr/lib/coq/
DOCDIR=/usr/share/doc/coq/
OCAMLFIND=/usr/bin/ocamlfind
CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-58   -safe-string -strict-sequence
WARN=-warn-error +a-3
HASNATDYNLINK=true
COQ_SRC_SUBDIRS=config lib clib kernel library engine pretyping interp gramlib gramlib/.pack parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax
seth:~$ which coqtop
/usr/bin/coqtop

looks like I don't have anything at /usr/lib/coq/vernac. I installed coq through the package manager (ubuntu 20.04). Do I need to install from source to get those files or something?

Thanks for all the help.

view this post on Zulip Seth Poulsen (Aug 25 2021 at 23:34):

aha! That file is provided by the libcoq-ocaml-dev package in Ubuntu. After installing that through apt, everything seems to be working fine. Will update here if I have further issues. Thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Aug 26 2021 at 00:11):

(deleted)

view this post on Zulip Emilio Jesús Gallego Arias (Aug 26 2021 at 00:14):

(deleted)

view this post on Zulip Théo Zimmermann (Aug 26 2021 at 09:43):

@Seth Poulsen Would you mind opening a PR to update the README of the plugin tutorial to mention this edge case (maybe a Troubleshoot section?)

view this post on Zulip Seth Poulsen (Aug 26 2021 at 15:57):

Sure, will do. I'm also happy to include how to get it working with VScoq if that would be helpful--it seems a lot of people are using it these days.

Last updated: Apr 18 2024 at 15:01 UTC