GitLab

These are my first experiments with using submodules to document the Iris commit that this builds against. Beyond mere documentation, this is also useful if you have some other, incompatible version of Iris installed but still want to compile this repo (say, for compiling an outdated version).

Things seem to work fine. If you just clone && make, it builds against the system version of Iris. You can do make iris-local to tell it to use the local version of Iris; this will initialize, clone and/or update the submodule and build Iris in there. If you want to switch back to the system-installed Iris, do make iris-system. Of course, before we merge this I should write a README explaining this (a README would be a good idea for this project anyway).

There's one problem: After initializing the submodule, coqdep in the outer repo will notice the .v files in the submodule and add them as dependencies. So even if you just initialize the submodule e.g. in order to update it to the latest commit (but you are otherwise using the system version), you need to remember to deinitialzie it again or your builds will start to fail because it can't find the .vo files it is looking for inside the submodule. Because of this effect on the dependencies (i.e., the .v.d files), both iris-local and iris-system also do a make clean in the outer repo -- which I guess makes sense anyway because you just switched Iris versions.

Our users don't have any problems with that, but I expect us to typically use a system-installed Iris -- so updating the submodule would mean doing the following: Initialize submodule, cd into it, update it, cd out of it, git add && git commit this change, deinitalize the submodule. It would be ncier if we could keep the submodule permanently initialized without using it, but I can't think of a way to do this. I guess I could write a little shellscript that does all these tasks (and some sanity checks like making sure we only go forward), so we'd do ./update-iris <SHA1 here> and be done.

Cc @robbertkrebbers @jjourdan @zhangz @janno What do you think? Zhen, if this works here I'd also implement the same for iris-atomic. Janno, do you think it would make sense for GPS-Iris to also adapt this?