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!
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.
Thanks, @Emilio Jesús Gallego Arias !
Last updated: Jan 28 2023 at 06:30 UTC