Hello,
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 https://dune.readthedocs.io/en/stable/dune-files.html#coq-theory
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.