Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
chipsf opened this issue Sep 2, 2023 · 2 comments
Open

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

chipsf opened this issue Sep 2, 2023 · 2 comments

Comments

@chipsf
Copy link

chipsf commented Sep 2, 2023

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
Copy link
Contributor

gares commented Sep 2, 2023

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
Copy link
Author

chipsf commented Sep 2, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants