Stream: Coq users

Topic: coq_makefile build directory


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

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

view this post on Zulip k32 (Apr 04 2021 at 07:11):

Thanks, @Emilio Jesús Gallego Arias !


Last updated: Jan 28 2023 at 06:30 UTC