search

runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
34 stars 19 forks source link

[adopted] .gitmodules: Change pybind11 URL from relative to absolute #1101

Open Baltoli opened 4 days ago

Baltoli commented 4 days ago

All the other URLs are absolute, so logically this one should match. Additionally, the relative URL will break if someone's main remote is not on GitHub.

Adopted PR from #1100 - thanks @0cjs!

0cjs commented 3 days ago

So it turns out that this is the source of my issues with being unable to init submodules in the k repo. Here's the problem:

  1. .../llvm-backend is a submodule of k, and deps/pybind is a submodule of .../llvm-backend.
  2. When in a fresh checkout of k I do git submodule update --init --recursive, .../llvm-backend is brought in, and HEAD is set to the commit specified by the current commit of k. Thus, HEAD points to a commit, not a ref (or "branch name", as it's often called). Being a commit and not a ref, it can have no tracking ref (a ref updated from the remote, e.g. refs/remotes/origin/main).
  3. When git submodule attempts to init deps/pybind11 in .../llvm-backend it reads url = ../../pybind/pybind11, determines that it's a relative URL (because it starts with ../) and goes to look for an absolute URL for it to be relative to.
  4. This absolute URL is, according to the git-submodule manual page, "relative to the superproject’s repository." It normal attempts to retrieve the superproject's repo URL by looking at the tracking ref associated with HEAD in the superproject.
  5. It can't find the absolute URL using the technique in point 4, because of point 2.
  6. Rather than looking for any remote in .git/config, it instead just guesses origin as the remote name. This does not exist in my repo, because I have clone.defaultRemoteName = r set in my ~/.gitconfig. (I hate typing more than I have to.) I'd argue that this guess of origin rather than guessing one of the remote names the repo is actually using is a bug in Git.
  7. Since it cant find the URL of a remote namedorigin`, it falls back to a remote set to the relative path relative to the filesystem path in which llvm-backend is checked out.
  8. That's not a repo, but git submodule doesn't recognise this, and considers the failure to fetch from it a temporary error. It tries again almost immediately, but that fails too, of course.
  9. It then leaves the subrepo init'd to this bad remote, meaning that you'll see nothing but errors for this until you de-init and manually re-init to a good remote.