Stream: Coq devs & plugin devs

Topic: Manually installing .v files


view this post on Zulip Philip (Oct 06 2023 at 12:00):

Is it possible to use ocamlfind install to install a .v file, so that Coq can load it?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 12:03):

@Philip can you provide a bit more context? Both coq_makefile and dune will install .v files by default

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 12:03):

If you mean a .vo file, then maybe you need to configure your _CoqProject settings

view this post on Zulip Philip (Oct 06 2023 at 12:25):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 12:26):

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.

view this post on Zulip Philip (Oct 06 2023 at 13:23):

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])

view this post on Zulip Gaëtan Gilbert (Oct 06 2023 at 13:25):

what -Q or -R did you give to coq_makefile?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 13:26):

@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

view this post on Zulip Philip (Oct 06 2023 at 13:27):

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 ^^

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 13:28):

Yes @Philip

view this post on Zulip Philip (Oct 06 2023 at 13:28):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 13:29):

Yup, it should have worked, so we need to see more to understand what went wrong

view this post on Zulip Philip (Oct 06 2023 at 13:29):

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

view this post on Zulip Guillaume Melquiond (Oct 06 2023 at 13:37):

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 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 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.

view this post on Zulip Philip (Oct 06 2023 at 13:47):

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 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 does your test.v file contain? In particular, are you using a clause From Abella2Coq or anything semantically equivalent?

Just a `Require Import`:

```coq
Require Import Abella2Coq.

Also, the -Q elpi part of your _CoqProject file might be confusing coq_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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 13:56):

@Philip things in user-contrib are scope by your package name, so you need to do From Abella2Coq Require Import abella2coq.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 06 2023 at 13:57):

Or Require Import Abella2Coq.abella2coq , the test.v file was missing in your repos btw

view this post on Zulip Philip (Oct 06 2023 at 13:58):

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