Chantal Keller (Jul 30 2022 at 12:34): Chantal Keller (Jul 30 2022 at 12:34):Hi
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 foo.ml
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.
Thanks!
Gaëtan Gilbert (Jul 30 2022 at 12:40):try using -linkall for the second ocamlopt call
Chantal Keller (Jul 30 2022 at 12:44):Indeed :-) Many thanks!
Notification Bot (Jul 30 2022 at 15:03):Chantal Keller has marked this topic as resolved.
Last updated: Oct 08 2024 at 16:02 UTC