Stream: Coq users

Topic: Extracting to a directory


view this post on Zulip Ana de Almeida Borges (Sep 21 2022 at 18:43):

I have some Coq files living in a theories directory, one of which has an extraction command:

Extraction "ml/extracted" f.

The ml directory needs to exist in order for this to work. I have both theories and ml in the same directory, as well as a standard makefile that I copied from somewhere. make is perfectly happy to accept this and extracts everything to ml, as requested. However, when I interactively run through the above file with Proof General, it complains that ml doesn't exist. It turns out tweaking the path makes it work:

Extraction "../ml/extracted" f.

But then make no longer works.

Should I do something special in the makefile or anywhere else?

view this post on Zulip Karl Palmskog (Sep 21 2022 at 18:51):

maybe not the best answer, but if you can, I highly recommend using Dune extraction. In my view, it finally makes it feasible to do complex OCaml builds depending on extracted code. My standard example here, a plugin that uses extracted code: https://github.com/coq-community/stalmarck/blob/master/tactic/dune

view this post on Zulip Ana de Almeida Borges (Sep 21 2022 at 19:21):

Thanks for the link! I'll make sure to look into it when I start using Dune, but for now I was looking for some faster solution.

view this post on Zulip Ana de Almeida Borges (Sep 21 2022 at 19:21):

There has been some discussion about extraction directories in the bug tracker. There is even a PR introducing an Extraction Output Directory command, but it's still a draft.

view this post on Zulip Ali Caglayan (Sep 22 2022 at 08:53):

I can push that PR forward if there is interest.

view this post on Zulip Ana de Almeida Borges (Sep 22 2022 at 14:02):

Yeah, I'm interested.

view this post on Zulip Matthieu Sozeau (Sep 23 2022 at 06:41):

FWIW, it’s a symptom of running coqc and coqidetop from different working directories.

view this post on Zulip Paolo Giarrusso (Sep 23 2022 at 08:45):

@Ana de Almeida Borges where does your _CoqProject live? If you put it in theories, maybe that's why, and you could move it outside (and adjust the paths!). At least that'd be enough for VsCoq

view this post on Zulip Paolo Giarrusso (Sep 23 2022 at 08:47):

OTOH... this feels like an issue with Extraction; when coq-elpi had the same problem, we moved to a mechanism where paths where computed relative to loadpaths, tho there things fit better

view this post on Zulip Ana de Almeida Borges (Sep 23 2022 at 10:03):

My _CoqProject lives in the root directory, not inside theories. I guess that means this is possibly a problem with Proof General itself

view this post on Zulip Paolo Giarrusso (Sep 23 2022 at 17:12):

Amazing... Does it mean proof general adjustes the paths to run coq in a different folder? It's not impossible, but it does seem pointless...

view this post on Zulip Paolo Giarrusso (Sep 23 2022 at 17:12):

Ah no it's not: it must adjust that, since it searches the file around... @Ana de Almeida Borges where do you launch proof general? Maybe that's the current directory used?

view this post on Zulip Gaëtan Gilbert (Sep 23 2022 at 18:05):

PG runs coq in the directory of the source

view this post on Zulip Gaëtan Gilbert (Sep 23 2022 at 18:05):

coq_makefile runs coq in the directory of the makefile

view this post on Zulip Gaëtan Gilbert (Sep 23 2022 at 18:05):

if they are not the same then you lose

view this post on Zulip Ana de Almeida Borges (Sep 24 2022 at 09:38):

Yeah, that's exactly it. It doesn't matter where I am when I open PG, it always thinks I'm in the source's directory.

view this post on Zulip Karl Palmskog (Sep 24 2022 at 09:45):

from what I remember, PG uses the location of the _CoqProject it finds

view this post on Zulip Ana de Almeida Borges (Sep 24 2022 at 09:49):

I can't confirm that, it seems to me it's using the Coq source's directory even though _CoqProject is not in the same place.

view this post on Zulip Ali Caglayan (Sep 27 2022 at 11:38):

So I made some more progress with https://github.com/coq/coq/pull/16126 however I am unsure how to progress. There are questions like:

I haven't been able to give them much thought however. I also need to write some more tests and furthermore make sure that we are somewhat backwards compatible.

view this post on Zulip Ali Caglayan (Sep 27 2022 at 11:39):

If anybody wants to help out or has some ideas how to progress they are welcome to let me know :)


Last updated: Jan 29 2023 at 03:28 UTC