add iris as submodule

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?

I just thought of a way to solve the problem mentioned above. My idea was to call the submodule something like iris-sub, and then let make iris-local and make iris-system install/delete a symlink from iris to iris-sub. So we could initialize the submodule without having the iris folder filled. However, coqdep will still pick uo the files in iris-sub, since they are below . and we have -Q . lrust. To fix this, we'd have to change that . to something that excludes the iris submodule; for example, we could move all files into a folder src and then use -Q src lrust. (That would also get rid of -Q . lrust and -Q iris iris overlapping.)

So, the new folder structure would be something like:

• iris: submodule, can be permanently initialized
• use-iris: Symlink to iris, managed by make iris-local and make iris-system (not checked into git)
• src: lrust files

_CoqProject would start with

-Q src lrust
-Q use-iris iris
src/adequacy.v
...

In case Coq doesn't like non-existing folders in -Q, instead of deleting the symlink we could replace it by an empty directory. But it doesn't seem like Coq minds such folders to be missing.

EDIT: Looks like the usual name for that src folder in Coq developments is theories. I don't care strongly.

Unmarked this merge request as a Work In Progress

Marked this merge request as a Work In Progress

First it looks like a perfect solution would involve multiple parties including git, make, coq_makefile, and everyone's system specifics ..... so I am afraid that it might be hard to make everyone happy while keeping the scrips minimal.

In fact, I have thought about the general problem a bit: I think basically we want to have a simple build + version-control system (similar to package managers likecargo in Rust), but it should be lightweight, highly-configurable (similar to CI), and works closely with git rather than some central repository (so shortly it is a package manager for your private and many-repo-style projects).

So if:

1. You guys agree with my points on the complexity of this problem
2. We can confirm that there is no existing system for such purpose
3. It is a headache in a lot of cases

then I think it is an independent engineering problem worth solving.

I would say that in order to make sure Lambdarust still compiles with the current version of the submodule, a developer of Lambdarust should never use the system Iris, because it has probably a different version anyway. So most of your problems disappear, don't they?

@jjourdan Maybe because in our case, we might develop both downstream and upstream at the same time? (So the scenario might be, you modify the system-global Iris, and want to check if it is compatible with lrust ....)

It is true that Coq lacks a proper package manager, but I don't plan to invent one here. ;) (Also, maybe opam can fill that role, I don't know.)

As a developer, I don't want to compile Iris once for every reverse dependency. I'd rather use CI to check that the submodule link stays up-to-date.

My problems would also disappear if we stop using . as the mapping folder for whatever is the local module -- which is considered bad practice in some programming language communities (e.g. many Java programs will have their Java sources rooted in a java folder, Rust puts everything into a src folder, and so on). So IMHO that step makes sense anyway, precisely because it lets us version-control things "outside" of the Coq module tree. (Think of the benchmark folder in the main Iris repo as an example of sth. that shouldn't really be inside he Coq module tree. On the other hand, main Iris doesn't need a submodule, so moving things around there is less pressing.)

As a developer, I don't want to compile Iris once for every reverse dependency. I'd rather use CI to check that the submodule link stays up-to-date.

The point is that you should not do a submodule update at every single commit of Iris. And, anyway, builds within the submodule are also incremental. I am not so happy about relying on the CI: this can make intermediate commits broken, you rely on everyone being quite responsive to CI alerts...

The point is that you should not do a submodule update at every single commit of Iris. And, anyway, builds within the submodule are also incremental. I am not so happy about relying on the CI: this can make intermediate commits broken, you rely on everyone being quite responsive to CI alerts...

Agreed.

If I fail to keep the build working, I'll change strategies. I'd still prefer to support initializing the submodule without using it for building. So are you fine with what I propose in https://gitlab.mpi-sws.org/FP/LambdaRust-coq/merge_requests/1#note_16526 ?

Not sure I understand everything, but yes, that seems right (except that I will have large conflicts to solve with my local branch, but whatever).

"local branch"? Couldn't you just merge to master soon-ish?

Well, it does not build.

Hm. That's a point ;)

Any estimates when it will be mergeable?

Not any time soon. I'm rebasing the new lifetime logic.

But feel free to merge: there will indeed probably be conflicts, but they will easily be fixed. But for the submodule, please do use a commit using the old notation for separating conjunction!

Added 1 commit:

• 9a515ecb - add iris as submodule

Compare with previous version

Unmarked this merge request as a Work In Progress

Mentioned in commit 556a69f5

Status changed to merged

All right, I did the move and merged. Next I will experiment with CI builds.