5

One of the projects I am using has in it/s .gitmodules file:

(iit_synthesis) brando9~/proverbot9001 $ cat .gitmodules  | grep 'metalib'
[submodule "deps/metalib"]
    path = deps/metalib
    url = git@github.com:plclub/metalib.git

but I am pretty sure it should be:

[submodule "coq-projects/metalib"]
    path = coq-projects/metalib
    url = git@github.com:plclub/metalib.git

when I do it by the command line it doesn't let me due to the gitignore file:

(iit_synthesis) brandomiranda~/proverbot9001 ❯ git submodule add --name coq-projects/metalib https://git@github.com:plclub/metalib.git coq-projects/metalib

The following paths are ignored by one of your .gitignore files:
coq-projects
coq-projects/metalib
hint: Use -f if you really want to add them.
hint: Turn this message off by running
hint: "git config advice.addIgnoredFile false"

I am going to modify it manually but it feels dirty, weird. Then I will force it to update:

git submodule update && git submodule init # todo modify to only target metalib

What is the proper way using the git command to re-add from stratch and update a specific git module.

Is the proper solution to do:

git submodule add -f --name coq-projects/metalib https://github.com/plclub/metalib.git coq-projects/metalib

feels hacky? Will it always work?

Bounty: ideal solution, # -- Pull metalib explicitly 1st before doing the standard git submodule "pulls/inits" (for now hope to fix later so git "pull" does it all)

#-- Pull metalib explicitly 1st before doing the standard git submodule "pulls/inits" (for now hope to fix later so git "pull" does it all)
# - I think this pulls the coq projects properly in proverbot
# todo: Q: metalib missing, how do I pull it with original git submodule commands?
# todo: https://stackoverflow.com/questions/74757297/how-do-i-make-sure-to-re-add-a-submodule-correctly-with-a-git-command-without-ma
# todo: https://github.com/UCSD-PL/proverbot9001/issues/59
# todo: https://github.com/UCSD-PL/proverbot9001/issues/60
# ### rm -rf coq-projects/metalib  # why?
git submodule add -f --name coq-projects/metalib https://github.com/plclub/metalib.git coq-projects/metalib

e.g. with:

git submodule update && git submodule init

Bounty2: Need details in answers to be able to verify suggestions actually work

I'd like that the answers given have more details by providing checks I can do to check that the updated gitmodules is as expected either in the .gitmodules files, downloaded repo or any check. Code and natural language explanations are best for verification.

Which is first init or update?

Related note, when I should run git submodule update vs git submodule init vs is really confusing me. I usually do git submodule init then git submodule update --init --remote. Is that correct or a different order is better? related: which should be ran first git submodule update or git submodule init?

related:

Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
  • 2
    The fact that they're marked as *ignored* (a poor choice of verb on Git's part, but that's another story entirely) is deeply suspicious. If they should be tracked as submodules with that path, they should not be ignored. Fix the ignore issue and the `git submodule` command will stop complaining. But in this case there's no really "proper" anything here; Git's submodules are currently still a lot of mechanism with very little fancy UI, so there's no reason (as of yet) not to just reach down into the gears and wires and yank and shove things about. – torek Dec 11 '22 at 06:10
  • @torek hi torek! I'm puzzld, why is it saying "ignored"? I don't think I told git to ignore anything. Where might that option be set? Thanks for your time in advance. Not in `.gitignore`. – Charlie Parker Feb 04 '23 at 00:46
  • The '/coq-projects/' is in the `.gitignore` file. Does that explain why the `.gitmodules` is incorrect and why I need to run `git submodule add -f --name coq-projects/metalib https://github.com/plclub/metalib.git coq-projects/metalib` and why `git submodule init && git submodule update --init --recursive --remote` doesn't seem to initialize all coq-projects correctly? I'm confused. What I want is to pull all coq-projects and the right version once using ideally the standard command `git submodule init && git submodule update --init --recursive --remote`. How do you recommend I do that? @torek – Charlie Parker Feb 05 '23 at 02:16
  • btw, when I should run `git submodule update` vs `git submodule init` vs is really confusing me. I usually do `git submodule init` then `git submodule update --init --remote`. Is that correct or a different order is better? related: https://stackoverflow.com/questions/75342383/which-should-be-ran-first-git-submodule-update-or-git-submodule-init – Charlie Parker Feb 10 '23 at 23:40
  • related: https://stackoverflow.com/questions/74757297/how-do-i-make-sure-to-re-add-a-submodule-correctly-with-a-git-command-without-ma – Charlie Parker Feb 15 '23 at 04:34
  • see: https://github.com/UCSD-PL/proverbot9001/issues/86 for soln – Charlie Parker Feb 15 '23 at 04:56
  • look at https://stackoverflow.com/questions/75342383/which-should-be-ran-first-git-submodule-update-or-git-submodule-init (a stack overflow post on what to run first) – joe-bro Feb 17 '23 at 20:55

3 Answers3

1

The proper way to re-add a Git submodule is to use the following command:

git submodule add -f --name <new_submodule_name> <submodule_repository_URL> <submodule_path>

In your case, the command would look like this:

git submodule add -f --name coq-projects/metalib https://github.com/plclub/metalib.git coq-projects/metalib

The -f flag is used to force the addition of the submodule even if it is ignored by a .gitignore file.

To update the submodule after adding it, you can run the following command:

git submodule update --init coq-projects/metalib
Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
Mike Lennon
  • 1,026
  • 3
  • how do I checked your above suggestion actually worked? – Charlie Parker Feb 10 '23 at 23:14
  • ok so a few question -- especially to be able to tell if what your suggesting is working for me. What does "adding a submodule mean operationally & thus how do I how it worked"? What I mean is, if I run the command you suggested `git submodule add -f --name coq-projects/Metalib https://github.com/plclub/Metalib.git coq-projects/Metalib `, are the changes I should see 1. an update to the .gitmodules folder with the addition of the above 2. should I see the repo being added & code being pulled or is that why you suggested later `git submodule update --init coq-projects/Metalib`? – Charlie Parker Feb 10 '23 at 23:29
  • btw I think it's metalib not Metalib. Made the changes. – Charlie Parker Feb 10 '23 at 23:37
  • btw, when I should run `git submodule update` vs `git submodule init` vs is really confusing me. I usually do `git submodule init` then `git submodule update --init --remote`. Is that correct or a different order is better? related: https://stackoverflow.com/questions/75342383/which-should-be-ran-first-git-submodule-update-or-git-submodule-init I assume this must be relevant to our discussion. – Charlie Parker Feb 10 '23 at 23:41
0

You need to use git check-ignore --verbose coq-projects command inside you project directory to get information about which file contains the pattern that make git ignore that path. There are a bunch of places that could contain ignore directives, not only .gitignore. After you find out the source and delete that pattern just retry what you did in your question.

Upd: Actually I see that the folder coq-projects is ignored in the repository that you've provided.

Max Dmitrichenko
  • 330
  • 2
  • 8
  • empty response form `(iit_synthesis) brando9~/proverbot9001 $ git check-ignore --verbose coq-projects` :( – Charlie Parker Feb 05 '23 at 02:13
  • I see the '/coq-projects/' in the `.gitignore` file. Does that explain why the `.gitmodules` is incorrect and why I need to run `git submodule add -f --name coq-projects/metalib https://github.com/plclub/metalib.git coq-projects/metalib` and why `git submodule init && git submodule update --init --recursive --remote` doesn't seem to initialize all coq-projects correctly? I'm confused. What I want is to pull all coq-projects and the right version once using ideally the standard command `git submodule init && git submodule update --init --recursive --remote`. How do you recommend I do that? – Charlie Parker Feb 05 '23 at 02:16
0

See this: https://stackoverflow.com/a/75455526/1601580

To make daniel's answer concrete this works:

# -- Get metalib foor coq-8.10 via commit when getting it through git submodules
## git init the right metalib if it wasn't git submodule init properly. ref: https://stackoverflow.com/questions/74757297/how-do-i-make-sure-to-re-add-a-submodule-correctly-with-a-git-command-without-ma, ref2: https://github.com/UCSD-PL/proverbot9001/issues/59, ref3: https://github.com/UCSD-PL/proverbot9001/issues/60
#rm -rf coq-projects/metalib
#git submodule add -f --name coq-projects/metalib https://github.com/plclub/metalib.git coq-projects/metalib
git submodule add -f --name coq-projects/metalib git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897 coq-projects/metalib
git submodule update --init coq-projects/metalib
# cd to coq-projects/metalib and make sure it's using the hash 104fd9efbfd048b7df25dbac7b971f41e8e67897
(cd coq-projects/metalib && git checkout 104fd9efbfd048b7df25dbac7b971f41e8e67897)
(git status && cd ..)

approx output:

(iit_synthesis) brando9~/proverbot9001 $ rm -rf coq-projects/metalib
(iit_synthesis) brando9~/proverbot9001 $
(iit_synthesis) brando9~/proverbot9001 $ git submodule add -f --name coq-projects/metalib git+https://github.com/plclub/metalib.git#104fd9efbfd048b7df25dbac7b971f41e8e67897 coq-projects/metalib
Reactivating local git directory for submodule 'coq-projects/metalib'.

(iit_synthesis) brando9~/proverbot9001 $
(iit_synthesis) brando9~/proverbot9001 $ cd metalib
-bash: cd: metalib: No such file or directory
(iit_synthesis) brando9~/proverbot9001 $ cd coq-projects/
(iit_synthesis) brando9~/proverbot9001/coq-projects $ cd metalib
(iit_synthesis) brando9~/proverbot9001/coq-projects/metalib $ git rev-parse HEAD
4ea92d82286cf66e54b4119b2bb2b039827204ab
(iit_synthesis) brando9~/proverbot9001/coq-projects/metalib $ cd coq-projects/metalib
-bash: cd: coq-projects/metalib: No such file or directory
(iit_synthesis) brando9~/proverbot9001/coq-projects/metalib $ git checkout 104fd9efbfd048b7df25dbac7b971f41e8e67897
Note: switching to '104fd9efbfd048b7df25dbac7b971f41e8e67897'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at 104fd9e Sync Makefile coq version with README/Docker
(iit_synthesis) brando9~/proverbot9001/coq-projects/metalib $ git status
HEAD detached at 104fd9e
nothing to commit, working tree clean
Charlie Parker
  • 5,884
  • 57
  • 198
  • 323