Le 01/12/2021 à 11:58, Julien Puydt a écrit : > In fact, I would say it re-exports everything it gets, since I could > only get rid of the error with: > > override_dh_ocaml: > dh_ocaml --nodefined-map=libcoq-elpi-ocaml- > dev:Extfun,Gramext,Versdep,Fstream,Pretty,Token,Grammar,Ploc,Plexing,Pl > exer,Eprinter,Diff,Stdpp,Pprintf,Extfold,Elpi__Ptmap,Elpi__Util,Elpi__B > uiltin,Elpi__Data,Elpi__Ast,Elpi__Builtin_map,Elpi__Builtin,Elpi__Built > in_checker,Elpi__Builtin_stdlib,Elpi__API,Elpi__Runtime,Trace_ppx_runti > me__Runtime,Elpi__Runtime_trace_on,Elpi__parser,Trace_ppx_runtime,Elpi_ > _exported,Elpi,Elpi__Runtime_trace_off,Elpi__Builtin_set,Elpi__exported > ,Elpi__Parser,Elpi__Compiler,Elpi__,Ppx_deriving_runtime,Re__,Re__Fmt,R > e__Category,Re__Group,Re__str,Re__Pcre,Re,Re__Str,Re__str,Re__Posix,Re_ > _Automata,Re__Emacs,Re__Core,Re__Cset,Re__Color,Re__Perl,Re__Color_map, > Re__Glob,Re_str,Re__Pmark,Result > > So there's definitely something wrong in the way it is built! I'll > definitely won't upload as-is...
I suspect the cmxs of coq-elpi is linked with its external dependencies (which seem to be Camlp5, Elpi and Re in your case), to "ease" its loading by Coq. This might work if coq-elpi is loaded into Coq alone, but will break when one wants to load another Coq plugin, e.g. one using Re. The proper way is to link coq-elpi's cmxs without its external dependencies, and instruct Coq to load the external dependencies (in the right order, and only once each) before it loads coq-elpi. Is your packaging of coq-elpi publicly available somewhere? Cheers, -- Stéphane
