search

UCSD-PL / proverbot9001

GNU General Public License v3.0
39 stars 17 forks source link

Is the .gitmodules file incomplete -- e.g. it's misisng constructive-geometry coq project? #98

Open brando90 opened 1 year ago

brando90 commented 1 year ago

I was trying to build constructive-geometry but it was missing for some reason. When I tried to reinitialize it just wouldn't reinitialize it for some reason, idk why.

Then I noticed it wasn't even in the .gitmodules file. Does this mean that the .gitmodules file is missing some git projects or something?

I can see it here: https://github.com/UCSD-PL/proverbot9001/tree/develop/coq-projects but it's not in the submodules file: https://github.com/UCSD-PL/proverbot9001/blob/master/.gitmodules

brando90 commented 1 year ago

but the .gitignore file also has ignoring /coq-projects/. How are people suppose to have the coq-projects or update them?

brando90 commented 1 year ago

shouldn't there be 124 or 136 entries in the .gitignore file?

(metalearning_gpu) brando9~/proverbot9001 $ find $HOME/proverbot9001/coq-projects -maxdepth 1 -type d | wc -l
136
(metalearning_gpu) brando9~/proverbot9001 $ total_num_coq_projs=$(jq length coqgym_projs_splits.json)
(metalearning_gpu) brando9~/proverbot9001 $ echo total_num_coq_projs = $total_num_coq_projs
total_num_coq_projs = 124
HazardousPeach commented 1 year ago

Yeah originally, the coq projects were committed direclty into the Proverbot repo, instead of using submodules. Projects were converted over to submodules as-needed while I was fixing builds, and it looks like constructive-geometry never made the switch, it's still committed directly into the repo. So, if it's missing for you, you should be able to get it with git checkout coq-projects/constructive-geometry. If you'd like to move it to a submodule to match the others, pull requests are welcome!