Makefile doesn't work with EXTERNAL_DEPENDENCIES=1 about bedrock2 HOT 4 OPEN

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

from bedrock2.

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 ?

from bedrock2.

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?

from bedrock2.

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.

from bedrock2.