Stream: Coq users

Topic: ✔ Build *.v Files Into a Subdirectory

view this post on Zulip Jiahong Lee (Jun 02 2022 at 02:13):

Hi, I'm very new to Coq.

After building a Coq project, I see files with extensions: .vo, .vok, .vos, .glob, and .<filename>.aux generated for each .v file. I have no idea what these build files are. And I find them very messy.

Questions:

  1. What are all the build files for?

  2. What does each build file do?
    I mean, one output file is enough, but why five?

  3. How can I move all the build files into a subdirectory and still make it loadable?
    E.g. at the project root, I would create a subdirectory .build/ and move all the build files into .build/. Can I still load all the build files seamlessly in ProofGeneral as if they are all residing at the project root?

Thanks!

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 02:16):

Re 3: AFAIK not today. Dune moves build output to _build, but Proof General is not integrated with that yet (https://github.com/ProofGeneral/PG/issues/477).

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 02:20):

Re "why 5 files": those 5 files have different life cycles, so if they were merged together, downstream tools would need to be more complex.

view this post on Zulip Jiahong Lee (Jun 02 2022 at 02:43):

Paolo Giarrusso said:

Re 3: AFAIK not today. Dune moves build output to _build, but Proof General is not integrated with that yet (https://github.com/ProofGeneral/PG/issues/477).

I see, thanks for pointing me to this issue!

view this post on Zulip Jiahong Lee (Jun 02 2022 at 02:44):

Paolo Giarrusso said:

Re "why 5 files": those 5 files have different life cycles, so if they were merged together, downstream tools would need to be more complex.

I see... Do you know any tool using any of the build files?

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 02:46):

IIRC, .aux records some timing information, that can be used to speed up some build operations (IIRC, async proofs). As such, they’re even kept by make clean (while make cleanall removes them as well).

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 02:47):

vos and vok will be empty in your case, but they’ll have useful content when doing quick builds with make vos and make vok

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 02:48):

even less sure about .glob files, but I recall they’re used by coqdoc?

view this post on Zulip Jiahong Lee (Jun 02 2022 at 02:50):

I see, thanks for your information!

view this post on Zulip Notification Bot (Jun 02 2022 at 02:50):

Jiahong Lee has marked this topic as resolved.

view this post on Zulip Ali Caglayan (Jun 02 2022 at 11:51):

Paolo Giarrusso said:

even less sure about .glob files, but I recall they’re used by coqdoc?

They record metadata about documentation such as locations, type etc. When coqdoc is run, it only uses the .glob files.

view this post on Zulip Ali Caglayan (Jun 02 2022 at 11:52):

Paolo Giarrusso said:

Re 3: AFAIK not today. Dune moves build output to _build, but Proof General is not integrated with that yet (https://github.com/ProofGeneral/PG/issues/477).

I'm unsure about this. I recall @Rodolphe Lepigre added support to dune. Perhaps he can say a bit more.

view this post on Zulip Rodolphe Lepigre (Jun 02 2022 at 20:58):

I did add support to dune, but some work is required on the editor side (e.g., in Proof General) to make things work out of the box. Currently, the only way to benefit from the dune coq top command is to hack your emacs configuration. Stuff like jump to definition can also be fixed with editor hacks, but ideally all of this would be done by the editor if it detects a dune environment.

Last updated: Oct 13 2024 at 01:02 UTC