Weird Makefile logic?

[ejgallego]

Weird Makefile logic?

[ejgallego]

Yes, that'd be fine. Tho relative paths and fixing your emacs setup seems like a much better solution to me.

[samuelgruetter]

According to the documentation of the compilation-directory-matcher variable, its default value should work... except that it doesn't, and I can't figure out why. Absolute paths look like a much more stable solution to me, so I changed _CoqProject to be autogenerated with absolute paths.

[ejgallego]

I am not expert, but I think the right fix is to teach your compilation buffer about submake and update current-directory accordingly. That's more robust, but indeed, nested makefiles are a pain.

[ejgallego]

Note how today, the .d dependency file doesn't contain absolute paths due to this hack, so it is not relocatable in the way you'd expect.

[ejgallego]

Note that I understand how this is a pain, and I'd suggest setting compilation-search-path in the right way for your project.

Another choice that could work is that you use absolute paths in _CoqProject for the directory in -R.

I'm willing to be convinced otherwise, but I'm afraid there is a lot of fragile path magic that could would have to do to support a different path scheme in _CoqProject and in the input for coq_makefile.

What do you think?

[ejgallego]

Another choice is to set your compilation-directory-matcher properly.

[samuelgruetter]

In our other makefiles, eg here:

https://github.com/mit-plv/bedrock2/blob/99b86e974bdaf0ed2ffd893b42cf60d980669000/bedrock2/Makefile#L37-L38

we autogenerate _CoqProject so that it contains absolute paths. Would that solve the issue?

[ejgallego]

That's weird ... Maybe you can open an issue in the Coq repos for coq_makefile?

Thanks for the fix, I will document the coq_makefile constraints.

Dune-based Coq modes actually understand composition better, so coqc is called from the base directory and emacs compilation buffer does work without the change directory hackery.