I have some Coq files living in a
theories directory, one of which has an extraction command:
Extraction "ml/extracted" f.
ml directory needs to exist in order for this to work. I have both
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.
make no longer works.
Should I do something special in the makefile or anywhere else?
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
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.
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.
I can push that PR forward if there is interest.
Yeah, I'm interested.
FWIW, it’s a symptom of running coqc and coqidetop from different working directories.
@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
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
_CoqProject lives in the root directory, not inside
theories. I guess that means this is possibly a problem with Proof General itself
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...
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?
PG runs coq in the directory of the source
coq_makefile runs coq in the directory of the makefile
if they are not the same then you lose
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.
from what I remember, PG uses the location of the
_CoqProject it finds
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.
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.
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