Stream: Coq devs & plugin devs

Topic: Executable using Ltac_plugin

view this post on Zulip Chantal Keller (Jul 30 2022 at 12:34):

I am trying to build a native OCaml executable that relies on Ltac_plugin, but I am facing an error when running the code.
Attached is a minimal example that I compile with

export COQLIB=... #path to COQLIB

ocamlopt -c -rectypes -I $COQLIB/kernel -I $COQLIB/lib -I $COQLIB/library -I $COQLIB/parsing -I $COQLIB/pretyping -I $COQLIB/interp -I $COQLIB/proofs -I $COQLIB/tactics -I $COQLIB/toplevel -I $COQLIB/plugins/btauto -I $COQLIB/plugins/cc -I $COQLIB/plugins/decl_mode -I $COQLIB/plugins/extraction -I $COQLIB/plugins/field -I $COQLIB/plugins/firstorder -I $COQLIB/plugins/fourier -I $COQLIB/plugins/funind -I $COQLIB/plugins/micromega -I $COQLIB/plugins/nsatz -I $COQLIB/plugins/omega -I $COQLIB/plugins/quote -I $COQLIB/plugins/ring -I $COQLIB/plugins/romega -I $COQLIB/plugins/rtauto -I $COQLIB/plugins/setoid_ring -I $COQLIB/plugins/syntax -I $COQLIB/plugins/xml -I $COQLIB/clib -I $COQLIB/gramlib/.pack -I $COQLIB/engine -I $COQLIB/config -I $COQLIB/printing -I $COQLIB/vernac -I $COQLIB/plugins/ltac -I $COQLIB/stm -I $COQLIB/kernel/byterun

ocamlfind ocamlopt -rectypes -I +threads -package zarith -I $COQLIB/kernel -I $COQLIB/lib -I $COQLIB/library -I $COQLIB/parsing -I $COQLIB/pretyping -I $COQLIB/interp -I $COQLIB/proofs -I $COQLIB/tactics -I $COQLIB/toplevel -I $COQLIB/plugins/btauto -I $COQLIB/plugins/cc -I $COQLIB/plugins/decl_mode -I $COQLIB/plugins/extraction -I $COQLIB/plugins/field -I $COQLIB/plugins/firstorder -I $COQLIB/plugins/fourier -I $COQLIB/plugins/funind -I $COQLIB/plugins/micromega -I $COQLIB/plugins/nsatz -I $COQLIB/plugins/omega -I $COQLIB/plugins/quote -I $COQLIB/plugins/ring -I $COQLIB/plugins/romega -I $COQLIB/plugins/rtauto -I $COQLIB/plugins/setoid_ring -I $COQLIB/plugins/syntax -I $COQLIB/plugins/xml -I $COQLIB/clib -I $COQLIB/gramlib/.pack -I $COQLIB/engine -I $COQLIB/config -I $COQLIB/printing -I $COQLIB/vernac -I $COQLIB/plugins/ltac -I $COQLIB/stm -I $COQLIB/kernel/byterun -o foo unix.cmxa threads.cmxa nums.cmxa str.cmxa zarith.cmxa dynlink.cmxa clib.cmxa config.cmxa lib.cmxa gramlib.cmxa kernel.cmxa library.cmxa engine.cmxa pretyping.cmxa interp.cmxa proofs.cmxa parsing.cmxa printing.cmxa tactics.cmxa toplevel.cmxa vernac.cmxa stm.cmxa ltac_plugin.cmx foo.cmx

Compilation goes through but I get an error when running it:

$ ./foo
No level labelled "0" in entry "term"
Fatal error: exception Failure("Grammar.extend")

The error disappears if I do not link ltac_plugin.cmx (and do not use it).

I am not using a build tool in this minimal example to try to understand what is going on. I am using Coq-8.13.2.


view this post on Zulip Gaƫtan Gilbert (Jul 30 2022 at 12:40):

try using -linkall for the second ocamlopt call

view this post on Zulip Chantal Keller (Jul 30 2022 at 12:44):

Indeed :-) Many thanks!

Last updated: Feb 06 2023 at 19:03 UTC