Ana de Almeida Borges (Sep 21 2022 at 18:43): 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?
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
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.
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.
Ali Caglayan (Sep 22 2022 at 08:53):I can push that PR forward if there is interest.
Ana de Almeida Borges (Sep 22 2022 at 14:02):Yeah, I'm interested.
Matthieu Sozeau (Sep 23 2022 at 06:41):FWIW, it’s a symptom of running coqc and coqidetop from different working directories.
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
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
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
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...
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?
Gaëtan Gilbert (Sep 23 2022 at 18:05):PG runs coq in the directory of the source
Gaëtan Gilbert (Sep 23 2022 at 18:05):coq_makefile runs coq in the directory of the makefile
Gaëtan Gilbert (Sep 23 2022 at 18:05):if they are not the same then you lose
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.
Karl Palmskog (Sep 24 2022 at 09:45):from what I remember, PG uses the location of the _CoqProject it finds
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.
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.
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: Sep 15 2024 at 13:02 UTC