k32 (Apr 03 2021 at 23:00): k32 (Apr 03 2021 at 23:00):Hello,
Probably a very simple question: I use coq_makefile to build a project. It generates artifacts (.vo, .vok, .vos) in the theories directory. Is it possible to configure it to output artifacts into a separate build directory? Is it possible to do it for proof-general as well? Thanks!
Emilio Jesús Gallego Arias (Apr 04 2021 at 00:46):Hi @k32 , I think as of today there is no such support, which is a pity as it is pretty easy to implement I think [I did it recently for the Coq stdlib] I dunno if there is a bug report already open, but otherwise feel free to open it.
Another option is to try the dune build system, which does indeed keep the build tree clean.
k32 (Apr 04 2021 at 07:11):Thanks, @Emilio Jesús Gallego Arias !
Last updated: Apr 19 2024 at 08:01 UTC