Hi,

I'm trying to package coq-elpi (after I packaged elpi [in NEW], and
before I can package hierarchy-builder), but dh_ocaml gives me an error
and I don't get it:

E: Error: unit Extfun exported in libcoq-elpi-ocaml-dev/libcoq-elpi-
ocaml v1.11.2-1 but already exported by camlp5 v7.14-1

But there's no mention of Extfun in the sources... so I don't know
where that comes from!

How does one handle that?

Cheers,

J.Puydt

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

Le 22/11/2021 à 10:45, Julien Puydt a écrit :

I'm trying to package coq-elpi (after I packaged elpi [in NEW], and
before I can package hierarchy-builder), but dh_ocaml gives me an error
and I don't get it:

E: Error: unit Extfun exported in libcoq-elpi-ocaml-dev/libcoq-elpi-
ocaml v1.11.2-1 but already exported by camlp5 v7.14-1

But there's no mention of Extfun in the sources... so I don't know
where that comes from!

How does one handle that?

This is probably coq-elpi trying to embed and reexport some camlp5 lib. Probably a bug in coq-elpi. But if not (a more thorough analysis is
needed), Extfun must be added to --nodefined-map option in
override_dh_ocaml.


Cheers,

--
Stéphane

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

I could finally find some time for some digging.

Le mardi 23 novembre 2021 à 10:13 +0100, Stéphane Glondu a écrit :

Le 22/11/2021 à 10:45, Julien Puydt a écrit :

I'm trying to package coq-elpi (after I packaged elpi [in NEW], and
before I can package hierarchy-builder), but dh_ocaml gives me an
error
and I don't get it:

E: Error: unit Extfun exported in libcoq-elpi-ocaml-dev/libcoq-elpi-
ocaml v1.11.2-1 but already exported by camlp5 v7.14-1

But there's no mention of Extfun in the sources... so I don't know
where that comes from!

How does one handle that?

This is probably coq-elpi trying to embed and reexport some camlp5 lib. Probably a bug in coq-elpi. But if not (a more thorough analysis is
needed), Extfun must be added to --nodefined-map option in
override_dh_ocaml.

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...

Cheers,

J.Puydt

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)