search

LPCIC / coq-elpi

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

`coq-elpi` cannot be built while it is installed #428

Open LasseBlaauwbroek opened 1 year ago

LasseBlaauwbroek commented 1 year ago

When I first run opam install coq-elpi and then make build OCAMLWARN= I get

File "./theories/derive.v", line 55, characters 0-73:
Error: File derive_hook.elpi found twice in elpi.apps.derive:
<prefix>/coq8.16/coq-elpi/apps/derive/elpi/derive_hook.elpi,
<prefix>/coq8.16/_opam/lib/coq/user-contrib/elpi/apps/derive/derive_hook.elpi.

This is rather inconvenient. Is there a way to just prefer the locally built elpi files?

gares commented 1 year ago

I thought I fixed it, bit apparently not. Thanks for reporting

Blaisorblade commented 1 year ago

With 1.16.0 I'm stuck on either that or the error below (non-reproducible after cleaning, and was triggered using a parallel build).

$ make build OCAMLWARN=
Using coq found in /Users/pgiarrusso1/.opam/coq-8.16.01-ocaml-4.14.0+flambda/bin, from COQBIN or PATH
########################## building plugin ##########################
make[1]: Nothing to be done for 'bytefiles'.
COQC theories/elpi.v
File "./theories/elpi.v", line 9, characters 0-30:
Error:
Anomaly
"Uncaught exception Failure("File elpi2html.elpi not found in: /Users/pgiarrusso1/git-bedrock/coq-elpi/., /Users/pgiarrusso1/.opam/coq-8.16.01-ocaml-4.14.0+flambda/bin/coqc, /Users/pgiarrusso1/git-bedrock/coq-elpi/., /Users/pgiarrusso1/git-bedrock/coq-elpi/.., /Users/pgiarrusso1/.opam/coq-8.16.01-ocaml-4.14.0+flambda/lib/coq/user-contrib/elpi/")."
Please report at http://coq.inria.fr/bugs/.

Command exited with non-zero status 129
theories/elpi.vo (real: 0.46, user: 0.41, sys: 0.04, mem: 140224 ko)
make[3]: *** [Makefile.coq:793: theories/elpi.vo] Error 129
make[2]: *** [Makefile.coq:409: all] Error 2
make[1]: *** [Makefile.coq:892: opt] Error 2
make: *** [Makefile:51: build-core] Error 2
Blaisorblade commented 1 year ago

Still the case on master.

A build with coq-dune 0.8 should probably fix this since user-contrib isn't loaded by default, but I'm not claiming that's trivial (or volunteering).

gares commented 1 year ago

Ony setup I get warnings that some stuff if found twice, but compilation goes on and succeed. So I guess I need to know more about your setup to reproduce