Makefile doesn't work with EXTERNAL_DEPENDENCIES=1

[Alizter]

I am trying to add the submodule dependencies of bedrock2 to coq's ci, however I am finding it really difficult to get bedrock2 to depend on already built versions of kami etc.

Looking at the makefile, it seems that setting EXTERNAL_DEPENDENCIES=1 is a bit too aggresive. It also stops the logical paths being supplied. It would be great if you could fix the makefile so it doesn't have to depend on submodules.

[samuelgruetter]

I think this is the intended behavior, because EXTERNAL_DEPENDENCIES=1 is meant to be used with $COQPATH, ie for scenarios where you ran make install in each of the dependencies, which installed them into $COQPATH/nameOfDependency, which means that indeed, -Q or -R options for these dependencies don't need to be passed any more.

Maybe the feature you are looking for is not EXTERNAL_DEPENDENCIES=1, but DEPS_DIR=/path/to/your/custom/dependencyDirectory ?

[JasonGross]

EXTERNAL_DEPENDENCIES=1 is the correct setting for Coq's CI, where the dependencies are installed. Possibly the issue that you're running into is that kami (?) tracks something other than the master branch (I've forgotten which branch it tracks though)? What's the error that you see?

[Alizter]

Well its just that the makefile of bedrock2 isn't binding any logical names at all. I had to do this manually, and I could only supply it for the top makefile.

[JasonGross]

Ah, I see the issue. The issue is that EXTERNAL_DEPENDENCIES=1 impacts both submodules and non-submodules. So either Coq's CI should build & install each subcomponent before the next one, or there should be done variant of EXTERNAL_DEPENDENCIES=1 which treats submodules like coqutil as external without treating, e.g., bedrock2 as external in end2end