Stream: VsCoq devs & users

Topic: Compilation with dune


view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Sep 08 2020 at 20:41):

Adding _build/default is indeed the current hack

view this post on Zulip Paolo Giarrusso (Sep 08 2020 at 20:42):

we're waiting for something better

view this post on Zulip Paolo Giarrusso (Sep 08 2020 at 20:42):

but I'd recommend -Q not -R for new code

view this post on Zulip Paolo Giarrusso (Sep 08 2020 at 20:43):

(Maybe we should start deprecating -R altogether)

view this post on Zulip 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

view this post on Zulip 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: Jan 30 2023 at 18:04 UTC