Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

metalib is missing even after git submodule update && git submodule init command #59

Closed
brando90 opened this issue Dec 10, 2022 · 20 comments

Comments

@brando90
Copy link

brando90 commented Dec 10, 2022

Idk why but coq/metalib is missing even after doing:

git submodule update && git submodule init
(iit_synthesis) brando9~/proverbot9001 $ git submodule update && git submodule init
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/CompCert'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/GeoCoq'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/QuickChick'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/UnifySL'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/VST'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/additions'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/algebra'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/area-method'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/bdds'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/buchberger'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/coq'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/coq-library-undecidability'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/coq-procrastination'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/coqrel'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/coquelicot'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/dictionaries'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/disel'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/distributed-reference-counting'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/euler-formula'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/fcsl-pcm'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/fermat4'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/finmap'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/float'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/goedel'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/hardware'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/hoare-tut'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/ieee754'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/int-map'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/lemma-overloading'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/lin-alg'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/math-comp'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/maths'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/mod-red'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/pocklington'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/pts'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/qarith'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/quicksort-complexity'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/smc'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/topology'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/tree-automata'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/twoSquare'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/verdi'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/verdi-raft'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/zchinese'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/zorns-lemma'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq-projects/zsearch-trees'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/coq_serapy'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/dataloader/gestalt-ratio'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/stubs/mypy-data'...
Cloning into '/lfs/ampere4/0/brando9/proverbot9001/stubs/pytorch-types'...
Submodule path 'CompCert': checked out '76a4ff8f5b37429a614a2a97f628d9d862c93f46'
Submodule path 'coq-projects/GeoCoq': checked out '09a02dc56715b3308689843dd872209262beb5af'
Submodule path 'coq-projects/QuickChick': checked out '2ebf945332f4f398ef14a4bf547bb595d945f6f2'
Submodule path 'coq-projects/UnifySL': checked out 'cf4eec5d0d9f76b864d92a9e6df5bc3e8bb43d9d'
Submodule path 'coq-projects/VST': checked out '84ede1cf708dd13b38dd4c3089ddf6f470c15093'
Submodule path 'coq-projects/additions': checked out 'e97f80de67e6c806e448504296a48bfe40cbcd3a'
Submodule path 'coq-projects/algebra': checked out 'a66ff5b0a908e706244f627bbd28b61f5e9b86e5'
Submodule path 'coq-projects/area-method': checked out '84cab885dd166ba80049973590a1080524fd9306'
Submodule path 'coq-projects/bdds': checked out '2a66529afca7c780fa18d21ecd4f6c8d55182a6d'
Submodule path 'coq-projects/buchberger': checked out 'fbf821ffe58eea281c6d98ebf0f8628cbe1d3ad1'
Submodule path 'coq-projects/coq': checked out 'dca7b1d4d2c83655eed74c5de264a5d3298ef788'
Submodule path 'coq-projects/coq-library-undecidability': checked out '1b1c59615d7b84a16d1d3a7b5dd510ac68699121'
Submodule path 'coq-projects/coq-procrastination': checked out '199dab4435148e4bdfdf934836c644c2c4e44073'
Submodule path 'coq-projects/coqrel': checked out '5f0dc26f999be80abe30cf51c42343f3a5cc0aa1'
Submodule path 'coq-projects/coquelicot': checked out 'aa05d3ec815002033893af422151558ea9330dbd'
Submodule path 'coq-projects/dictionaries': checked out '71d4c69ba2f1e0d5e08cd51fbaf801dcc006981d'
Submodule path 'coq-projects/disel': checked out '0418990a36f914c3eb69a2c63af6cfa6a05ec422'
Submodule path 'coq-projects/distributed-reference-counting': checked out '6f0d8fe701ec404702a8c7ae5aea97ad6be6b2b4'
Submodule path 'coq-projects/euler-formula': checked out '988520d51305a9bfe4158eefab2945eebaa87e29'
Submodule path 'coq-projects/fcsl-pcm': checked out 'fab4dfe3ca58ecf8aefeb8fa4ac4a2659b231f24'
Submodule path 'coq-projects/fermat4': checked out 'f91289c096a9a9e74bbf018444f23010465246d3'
Submodule path 'coq-projects/finmap': checked out '17da86bf63acbf21924c9159a4b5c1d4a4e9b38c'
Submodule path 'coq-projects/float': checked out 'a4b445bad8b8d0afb725d64472b194d234676ce0'
Submodule path 'coq-projects/goedel': checked out '89e0487eefa3f0c6c2ed9f552f2135b43ce937ab'
Submodule path 'coq-projects/hardware': checked out '525232186f45617626aaf4b18bdc40b5f0b71d9c'
Submodule path 'coq-projects/hoare-tut': checked out 'a4c2e609e065a90ceaaee6d1df931027ee983658'
Submodule path 'coq-projects/ieee754': checked out 'e50696e15dfabe5f9bcddf70947bd876f6d073df'
Submodule path 'coq-projects/int-map': checked out 'd96bb09fa7c8f261128acddf9d156e70e90e5c67'
Submodule path 'coq-projects/lemma-overloading': checked out 'e1c8bb876c7a26b90181d165f606cd35912ffa74'
Submodule path 'coq-projects/lin-alg': checked out 'aa5a7cc4105fd20debf4c13a7d40392e34631610'
Submodule path 'coq-projects/math-comp': checked out 'd09daeec7572ff9cb488e021245f7f5cd4680410'
Submodule path 'coq-projects/maths': checked out 'c50d4745619f6a8877ffd8d749cafea74d48ad62'
Submodule path 'coq-projects/mod-red': checked out '72bd9d8fd6752648792ec790c16217a4d1498859'
Submodule path 'coq-projects/pocklington': checked out '6571af6fe8305d8fce68bc188dffab9c842fb49c'
Submodule path 'coq-projects/pts': checked out 'f368d34f919bb7ff714c0eb0d97929207502892b'
Submodule path 'coq-projects/qarith': checked out '32aae3f90fd93e33ae10730e5566e1dccb4c6d1e'
Submodule path 'coq-projects/quicksort-complexity': checked out 'd94adf421241ebb6084c0c4f798e33569d0420c8'
Submodule path 'coq-projects/smc': checked out '60e63dc612eeffe7ed5ad4a658fdacf30709b19a'
Submodule path 'coq-projects/topology': checked out 'fdda7fef1a1981330e7662a101e4001b200270b7'
Submodule path 'coq-projects/tree-automata': checked out '1d756a966aaee796ed46362d45ec9b0ddc6951ca'
Submodule path 'coq-projects/twoSquare': checked out 'a58998cf3719811f00419e366db7f9c5bb889aae'
Submodule path 'coq-projects/verdi': checked out '064cc4fb2347453bf695776ed820ffb5fbc1d804'
Submodule path 'coq-projects/verdi-raft': checked out 'ea99a7453c30a0c11b904b36a3b4862fad28abe1'
Submodule path 'coq-projects/zchinese': checked out '906bb36960c230df143356ca4565771fe3008ef7'
Submodule path 'coq-projects/zorns-lemma': checked out 'aaf46b0c5f7857ce9211cbaaf36f184ca810e0e8'
Submodule path 'coq-projects/zsearch-trees': checked out '91b00b3912f78bc97dd2d450e9ff5d90d602600f'
Submodule path 'coq_serapy': checked out '61dfc7a14a5ad0a67c838bd75bad36c0ceeefe48'
Submodule path 'dataloader/gestalt-ratio': checked out '6544dc338b78bfbec6f376fb9c0136633439edbc'
Submodule path 'stubs/mypy-data': checked out '952404655a8f028cdd47d9fa39d55ff6c0b377ba'
Submodule path 'stubs/pytorch-types': checked out 'f0792dfdba67649427ebe70f69ee51f2ff1fae06'

and see:

(iit_synthesis) brando9~/proverbot9001 $ (cd coq-projects/metalib && opam install .)
-bash: cd: coq-projects/metalib: No such file or directory
@brando90
Copy link
Author

weird it is there:

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

idk why it's missing

@brando90
Copy link
Author

shouldn't it be:

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

U aksi see it is in the project splits json file so I think that's correct. Idk yet how to do it with one command.

@brando90
Copy link
Author

the git ignore ignores it? why?

(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"

@brando90
Copy link
Author

wait, nvm it makes sense to ignore the submodules /coq-projects/ but why it git not letting me submodule it then? :/

@brando90
Copy link
Author

I will manually change the file in my fork and the re update and init all submodules, though it feels weird...https://stackoverflow.com/questions/74757297/how-do-i-make-sure-to-re-add-a-submodule-correctly-with-a-git-command-without-ma

@brando90
Copy link
Author

to update all

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

@brando90
Copy link
Author

I manually changed it but I think this is enough:

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

@HazardousPeach
Copy link
Contributor

This one I'm not sure about, I'll keep it open until I can try a fresh install to see if I can reproduce.

@brando90
Copy link
Author

brando90 commented Feb 3, 2023

@HazardousPeach were you able to solve this?

@brando90
Copy link
Author

brando90 commented Feb 4, 2023

I'm confused, why does it say ignored?

(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"

@brando90
Copy link
Author

brando90 commented Feb 4, 2023

@HazardousPeach you have two meta-libs in the .gitmodules. Why? I think this is a mistake, let me know if I'm wrong :). Url:

https://github.com/UCSD-PL/proverbot9001/blob/develop/.gitmodules

@HazardousPeach
Copy link
Contributor

The git ignore is because we don't want to commit changes we make inside the projects generally. You can change that to see if it fixes anything for you, if it does pull requests welcome. Otherwise, for adding submodules just add the -f flag. The two meta-libs are installed in different places, referenced for different usages. If you can point everything to one of them I'll happily accept the pull request, but I don't think having multiple breaks anything.

@brando90
Copy link
Author

@HazardousPeach your install_coqgym_deps.sh only has:

# Metalib doesn't install properly through opam unless we use a
# specific commit.
(cd coq-projects/metalib && opam install .)

Why is the other present?

@brando90
Copy link
Author

also the above line is confusing me in the fact that this is also missing in the original install_coqgym_deps.sh:

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

Is that run anywhere? Is there a reason you don't have a list of git submodule adds recorded in your dependency install?

@brando90
Copy link
Author

I think this is most crucial @HazardousPeach -- how do I check the (two?) metalib's were installed correct? How should the repo and .gitmodules files look like for example?

Thanks in advance for ALL the help. :)

@brando90
Copy link
Author

brando90 commented Feb 11, 2023

I tried:

# Metalib doesn't install properly through opam unless we use a specific commit.
git submodule add -f --name coq-projects/metalib https://github.com/plclub/metalib.git coq-projects/metalib
git submodule update --init coq-projects/metalib
(cd coq-projects/metalib && opam install .)

I think I will simply install that coq version 8.15. I can't reproduce what you had in your set up such that it works without issues :( idk, the .gitmodules don't store the commit so I have no idea how git is aactually making sure we are using the right commits.

https://stackoverflow.com/questions/75417355/how-does-one-git-submodule-add-a-specific-commit-and-have-it-be-recorded-in-the

@brando90
Copy link
Author

likely needed: https://stackoverflow.com/questions/75452407/how-does-one-pin-freeze-a-version-of-the-dependencies-of-an-opam-project-package

and a command like this is likely needed:

opam pin add coq-metalib https://github.com/plclub/metalib/commits/104fd9efbfd048b7df25dbac7b971f41e8e67897

@brando90
Copy link
Author

@HazardousPeach I think this will fail:

# todo: We need to install it as a depedency such that build_coq_projects.sh would work. I assume it has to be the coq-projects/ or deps/ way to install it
# -- Get metalib, needs opam switch coq-8.15 for some reason either update to metalib or it's deps, ref: https://github.com/UCSD-PL/proverbot9001/issues/82
# - Create the coq 8.15 switch
#opam switch create coq-8.15 4.07.1
#eval $(opam env --switch=coq-8.15 --set-switch)
#opam pin add -y coq 8.15.2
## pull 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
git submodule add -f --name coq-projects/metalib https://github.com/plclub/metalib.git coq-projects/metalib
git submodule update --init coq-projects/metalib
## Metalib doesn't install properly through opam unless we use a specific commit.
#(cd coq-projects/metalib && opam install .)
## install it again since I think his code has pointers to a version under deps, could unify with above but it's less work to just accept as is and install it, ref: https://github.com/UCSD-PL/proverbot9001/issues/77
git submodule add -f --name deps/metalib https://github.com/plclub/metalib.git deps/metalib
git submodule update --init deps/metalib
#(cd deps/metalib && opam install .)
# 104fd9efbfd048b7df25dbac7b971f41e8e67897
#eval $(opam env --switch=coq-8.10 --set-switch)
#opam pin add coq-metalib https://github.com/plclub/metalib/commits/104fd9efbfd048b7df25dbac7b971f41e8e67897

because we need the specific repo that is compatible with coq 8.10, right?

@brando90 brando90 reopened this Feb 15, 2023
@brando90
Copy link
Author

closes this issue imho: #86

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants