Coq's .git is 152MB
HoTT is >600MB
what is going on?
@Gaëtan Gilbert they put all their static documentation for every commit in the
gh-pages branch. Coqdoc for a medium-sized project runs at maybe 5-10MB uncompressed. The delta-compression in Git can only do so much.
this is why we only recommend to keep static documentation in
gh-pages for each release in projects in coq-community.
for anyone doing documentation for a medium to large project, I would just put that in a different dedicated repo for each commit, like Coq does with its Stdlib HTML
Are you saying we should have a seperate repo for the gh-pages commits?
yes that too, but your existing repo is now so large that I think you should rewrite its history to not include all the static docs
basically, everyone who now clones the repo will have to wait at the minimum a few minutes and typically maybe 10 minutes due to bandwidth limits imposed by GitHub
How can we rewrite git history?
if you move the gh-pages branch to a separate repo just deleting it from hott/hott should work I think
Thanks @Gaëtan Gilbert for bringing this up, I had noticed the large file size too, but I didn't think much of it at the time.
I've opened an issue in the HoTT repo #1388
I confirm this recommendation. We had the same problem in the repository for Scala 3. There's also git clone --single-branch (or such) as a stopgap, but not a complete fix.
if anyone is still following this, I just want to say that recommending people to clone with
--single-branch (as done in the HoTT repo issue) is a non-solution to this issue. Typically, we will have many tools cloning Coq repos automatically, and making sure all of them use such a specific command is completely unrealistic in my view.
Last updated: Sep 28 2023 at 11:01 UTC