Compilation output files


Is there way to configure coqc or the makefile so that it doesn’t create compiled files in the same place with the input files? More specifically having a structure in the project folder similar to /src containing .v files and /build containing compilation results.

No, but you may be interested in using Dune as your build system instead of a coq_makefile-generated Makefile. It puts every build output into a _build folder. For now, the Coq support is still preliminary, but already good enough for some use cases. Don’t hesitate to ask questions!

Cf. doc at

1 Like

Thank you for the suggestion. I ported to dune and it compiles successfully. However when I try to import a file, it can’t find it during interactive proving. How can I solve this issue?
I am using coq 8.11 and emacs 26.1 with proof general for development.

That’s an unfortunate problem that we should solve in Proof General; I’m going to open a bug report.

You can workaround that by creating a CoqProject file, then add the corresponding -R Foo _build/default/dir flag there.


Thank you. This worked.

1 Like