The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I’m in the process of constructing an ml plugin for Coq.  I have a source file “advanced_rewrite.ml4” which references a symbol “intern” which is defined in an ml file “intern.ml” (and “intern.mli”).  I get the following error when I compile:

File "./theories/advancedRewrite.v", line 1, characters 0-37:

Error: while loading src/advanced_rewrite.cmxs:

error loading shared library: dlopen(/Users/kendroe/FDS/engine/plugin/src/advanced_rewrite.cmxs, 138): Symbol not found: _camlIntern__intern_1306

  Referenced from: /Users/kendroe/FDS/engine/plugin/src/advanced_rewrite.cmxs

  Expected in: flat namespace

 in /Users/kendroe/FDS/engine/plugin/src/advanced_rewrite.cmxs

make[1]: *** [theories/advancedRewrite.vo] Error 1

make: *** [plugin] Error 2

It appears that the file intern.cmi and intern.cmo are not being properly loaded into the Coq environment.  How do I fix this bug?  This is what I have in my _CoqProject file (which is sent to coq_makefile) to create the makefile:

-Q theories AdvancedRewrite

-I src

src/builtin.ml

src/builtin.mli

src/cache.ml

src/cache.mli

src/context.ml

src/context.mli

src/crewrite.ml

src/crewrite.mli

src/derive.ml

src/derive.mli

src/disc.ml

src/disc.mli

src/env.ml

src/env.mli

src/exp.ml

src/exp.mli

src/intern.ml

src/intern.mli

src/expIntern.ml

src/expIntern.mli

src/getfile.ml

src/getfile.mli

src/inner.ml

src/inner.mli

src/kbrewrite.ml

src/kbrewrite.mli

src/lex.ml

src/lex.mli

src/match.ml

src/match.mli

src/mylist.ml

src/mylist.mli

src/parser.ml

src/parser.mli

src/prettyPrint.ml

src/prettyPrint.mli

src/rule_app.ml

src/rule_app.mli

src/subst.ml

src/subst.mli

src/trace.ml

src/trace.mli

src/trie.ml

src/trie.mli

src/type.ml

src/type.mli

src/advanced_rewrite.ml4

theories/advancedRewrite.v

My intern.mli file looks like this:

val intern: string -> int

val decode: int -> string

val intern_oriented_rule: int   (* 1 *)

val intern_unoriented_rule: int (* 2 *)

val intern_bool: int            (* 3 *)

val intern_true: int            (* 4 *)

val intern_false: int           (* 5 *)

…

           - Ken