Is it possible to use ocamlfind install
to install a .v file, so that Coq can load it?
@Philip can you provide a bit more context? Both coq_makefile and dune will install .v files by default
If you mean a .vo file, then maybe you need to configure your _CoqProject
settings
I was planning to manually write a Makefile with an install
rule, but now that you have reminded me of coq_makefile
, I guess I can generate one of those and then defer the installation using a recursive $(MAKE)
installation.
Yes @Philip , I recommend you start from coq_makefile or dune , then build from there. ocamlfind install
may not work the best for Coq due to differences between OCaml and Coq libs.
It seems that the Makefile that coq_makefile
generates places the files under $HOME/.opam/default/lib/coq/user-contrib
, but this won't allow me to Require Import
the code from just any file (e.g. I created a ~/test.v
, and in complains Error: Cannot find a physical path bound to logical path [name])
what -Q or -R did you give to coq_makefile?
@Philip Coq by default will add user-contrib
directory to its load path, so it should work, note that to develop your own lib you don't need to install the .vo files, Coq UIs and build systems will tell Coq where to look for binary objects
Gaëtan Gilbert said:
what -Q or -R did you give to coq_makefile?
Would it be easier if I just gave you a link to the repository I am working on? It is not that easy to describe it in generic terms ^^
Yes @Philip
Emilio Jesús Gallego Arias said:
Philip Coq by default will add
user-contrib
directory to its load path, so it should work, note that to develop your own lib you don't need to install the .vo files, Coq UIs and build systems will tell Coq where to look for binary objects
That is surprising, because I would have expected that running coqc test.v
should work in that case.
Yup, it should have worked, so we need to see more to understand what went wrong
Emilio Jesús Gallego Arias said:
Yes Philip
This is the code, pointing to the most recent revision with the changes I am working on right now: https://git8.cs.fau.de/software/abellatocoq/-/tree/a459d9148b379c6a76c7993ec627a25d82aacf1a/src
Philip said:
It seems that the Makefile that
coq_makefile
generates places the files under$HOME/.opam/default/lib/coq/user-contrib
, but this won't allow me toRequire Import
the code from just any file (e.g. I created a~/test.v
, and in complains Error: Cannot find a physical path bound to logical path [name])
What does your test.v
file contain? In particular, are you using a clause From Abella2Coq
or anything semantically equivalent?
Also, the -Q elpi
part of your _CoqProject
file might be confusing coq_makefile
.
Guillaume Melquiond said:
Philip said:
It seems that the Makefile that
coq_makefile
generates places the files under$HOME/.opam/default/lib/coq/user-contrib
, but this won't allow me toRequire Import
the code from just any file (e.g. I created a~/test.v
, and in complains Error: Cannot find a physical path bound to logical path [name])What does your
test.v
file contain? In particular, are you using a clauseFrom Abella2Coq
or anything semantically equivalent?Just a `Require Import`: ```coq Require Import Abella2Coq.
Also, the
-Q elpi
part of your_CoqProject
file might be confusingcoq_makefile
.How come? FWIW I am confused about -Q as well. I was just trying to follow @**Enrico Tassi**'s example from https://github.com/LPCIC/coq-elpi/tree/master/apps/derive.
@Philip things in user-contrib are scope by your package name, so you need to do From Abella2Coq Require Import abella2coq
.
Or Require Import Abella2Coq.abella2coq
, the test.v file was missing in your repos btw
Emilio Jesús Gallego Arias said:
Or
Require Import Abella2Coq.abella2coq
, the test.v file was missing in your repos btw
The latter work, thanks!
And I didn't add that file, because the point was to test something outside of the repository.
Last updated: Oct 13 2024 at 01:02 UTC