search

LPCIC / coq-elpi

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

coq-elpi.elpi not found when loading it with coqc #499

Open chipsf opened 1 year ago

chipsf commented 1 year ago

Now after a year of hiatus, I'm back working on packaging this for Guix.

I got coq-elpi to build and tried testing it by running coqc on a file containing just the line 

From elpi Require Import elpi.

I get the following error when doing that.

File "./testCoqElpi.v", line 1, characters 0-30:
Error:
Findlib error: coq-elpi.elpi not found in:
(a big list of directories)

After building, I'm only able to find a coq-lib.elpi file in the folder of the successful installation, but there is no coq-elpi.elpi file present.

Probably I'm just not able to see that there exists a simple way to fix this in the build process. It doesn't look like a problem with environment variables to me, but I can post the build script if it would help in debugging.

gares commented 1 year ago

That is the name of the findlib package, defined in a META file. The list of parts you elide should contain it, as in coq-elpi/META.

chipsf commented 1 year ago

The list didn't include the file src/META.coq-elpi, so adding a procedure to install that file fixed that error. What remains now is to get Coq to find stdlib-shims.

The second problem is a Guix issue, so I bet if I fixed something on that side, Coq would be able to find stdlib-shims.