Re: Trouble packaging coq-elpi

[Stéphane Glondu <glondu@debian.org>]

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