Weird Makefile logic?

[ejgallego]

Hi folks, I see your makefile has:

# absolute paths so that emacs compile mode knows where to find error
# use cygpath -m because Coq on Windows cannot handle cygwin paths
SRCDIR := $(shell cygpath -m "$$(pwd)" 2>/dev/null || pwd)/src

then you do

	@$(COQ_MAKEFILE) $(ALL_VS) -o Makefile.coq.all

with the above files, being absolute paths.

Using absolute paths is really not supported by coq_makefile (paths should be relative to the flags given in _CoqProject) , it works because coqdep implements some (fragile magic) but we'd like to get rid of it.

What is this stuff about emacs needing absolute paths? cc @samuelgruetter

[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]

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]

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.