Robin Green (Sep 08 2020 at 20:01): Robin Green (Sep 08 2020 at 20:01):I am using dune to compile my project. I found that once I split it into multiple files, I had to put this in _CoqProject:
-R _build/default/src cdage
i.e. use dune's build directory to read the compiled modules from. But this seems wrong. Is it OK or is there a better way?
Paolo Giarrusso (Sep 08 2020 at 20:41):Adding _build/default is indeed the current hack
Paolo Giarrusso (Sep 08 2020 at 20:42):we're waiting for something better
Paolo Giarrusso (Sep 08 2020 at 20:42):but I'd recommend -Q not -R for new code
Paolo Giarrusso (Sep 08 2020 at 20:43):(Maybe we should start deprecating -R altogether)
Emilio Jesús Gallego Arias (Sep 09 2020 at 13:31):We have an issue here https://github.com/ProofGeneral/PG/issues/477 , but indeed it is open what to do
Emilio Jesús Gallego Arias (Sep 09 2020 at 13:31):Generating _CoqProject is a tad fragile as they cannot capture all the cases
Last updated: Jun 04 2023 at 23:30 UTC