search

LPCIC / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
139 stars 51 forks source link

Exports a unit already exported by camlp5 #311

Closed SnarkBoojum closed 2 years ago

SnarkBoojum commented 2 years ago

At the end of the compilation of my package for coq-elpi, dh_ocaml tries to sanity-check the result and complains:

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

I was told on the Debian OCaml Maintainers mailing-list that it could be an upstream issue (needs a more thorough analysis, but I'm unable to do so yet).

Does coq-elpi re-export this unit?

SnarkBoojum commented 2 years ago

What's the status on this? That blocks me on getting coq-elpi in Debian and packaging hierarchy-builder.

SnarkBoojum commented 2 years ago

In fact, it's not re-exporting things from camlp5, but from all of its deps, since to get rid of the error I needed:

override_dh_ocaml:
        dh_ocaml --nodefined-map=libcoq-elpi-ocaml-dev:Extfun,Gramext,Versdep,Fstream,Pretty,Token,Grammar,Ploc,Plexing,Plexer,Eprinter,Diff,Stdpp,Pprintf,Extfold,Elpi__Ptmap,Elpi__Util,Elpi__Builtin,Elpi__Data,Elpi__Ast,Elpi__Builtin_map,Elpi__Builtin,Elpi__Builtin_checker,Elpi__Builtin_stdlib,Elpi__API,Elpi__Runtime,Trace_ppx_runtime__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,Re__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
gares commented 2 years ago

The root problem is the same of #312 with the same solution in Coq.

Coq, without https://github.com/coq/coq/pull/15220 uses Dynlink directly, so plugins need to be statically linked against all their dependencies. With that PR plugins will be loaded via findlib, so dependencies will be loaded automatically and not linked in anymore.

IMO your only way out is the very boring override you wrote up there, and you will be able to remove it as soon as https://github.com/coq/coq/pull/15220 gets in (and we release, hopefully Coq 8.16)

SnarkBoojum commented 2 years ago

Well, the boring override makes the package build, but if I understand well, at runtime that means there will be trouble: when coq will try to load several plugins, it will just break.

gares commented 2 years ago

Yes. As of today, the only two conflicting plugins are coq-elpi and coq-serapi

Blaisorblade commented 2 years ago

The root problem is the same of https://github.com/LPCIC/coq-elpi/issues/312 with the same solution in Coq.

If you close #312, this might warrant closing as well the same way?

gares commented 2 years ago

This is already fixed if you use elpi 1.15.2, since it does not use camlp5 anymore

SnarkBoojum commented 2 years ago

Well, I'm still compiling the list of re-exported symbols from elpi, but I can already say the problem is still there.

SnarkBoojum commented 2 years ago

It looks like coq-elpi re-exports just everything:

dh_ocaml --nodefined-map=libcoq-elpi-ocaml-dev:Elpi_parser,Elpi_util,Elpi_parser__Ast,Elpi__Runtime,Elpi__,Elpi_util__Util,Elpi__Builtin_checker,Elpi__Builtin,Elpi__Ptmap,Elpi_parser__Grammar,Elpi__Data,Elpi_lexer_config,Elpi__API,Elpi_parser__Parse,Elpi__Builtin_set,Trace_ppx_runtime,Elpi_parser__Parser_config,Elpi_parser__Error_messages,Elpi_parser__Lexer,Elpi,Elpi_exer_config__Tokens,Elpi_Builtin_stdlib,Elpi__Legacy_parser_proxy,Elpi__Builtin_map,Elpi_lexer_config__Tokens,Elpi__Compiler,Trace_ppx_runtime__Runtime,Elpi_lexer_config__Lexer_config,Elpi__Builtin_stdlib,Elpi__Runtime_trace_off,MenhirLib,Ppx_deriving_runtime,Re__Perl,Re__Core,Re__Pcre,Re_str,Re__Automata,Re__Emacs,Re,Re__Fmt,Re__Group,Re__,Re__Glob,Re__Pmark,Re__Category,Re__Str,Re__Posix,Re__Color_map,Re__Cset,Result
Blaisorblade commented 2 years ago

elpi now can still use camlp5, but I guess this survives when that option is disabled, right?

gares commented 2 years ago

Hum, I was pulling an hack for camlp5, I thought that was the offender. I've no idea why, say, Re is there.

SnarkBoojum commented 2 years ago

Well, everything seems to be there ; I see menhir, ppxlib, ppx-deriving and elpi... I guess re just comes through one of them.

Basically, coq-elpi seems to re-export everything... Here is my build file in case you want to check my compilation lines...

The problem is detected by dh_ocaml, so I have to override its call with the above monstruous line to get around the matter.