Stream: Coq users

Topic: hott repo is surprisingly large

Gaëtan Gilbert (Aug 27 2020 at 12:08):

Coq's .git is 152MB
HoTT is >600MB
what is going on?

Karl Palmskog (Aug 27 2020 at 12:12):

@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.

Karl Palmskog (Aug 27 2020 at 12:13):

this is why we only recommend to keep static documentation in gh-pages for each release in projects in coq-community.

Karl Palmskog (Aug 27 2020 at 12:15):

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

Ali Caglayan (Aug 27 2020 at 12:29):

Are you saying we should have a seperate repo for the gh-pages commits?

Karl Palmskog (Aug 27 2020 at 12:31):

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

Karl Palmskog (Aug 27 2020 at 12:33):

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

Ali Caglayan (Aug 27 2020 at 12:35):

How can we rewrite git history?

Gaëtan Gilbert (Aug 27 2020 at 12:36):

if you move the gh-pages branch to a separate repo just deleting it from hott/hott should work I think

Ali Caglayan (Aug 27 2020 at 12:45):

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.

Ali Caglayan (Aug 27 2020 at 12:47):

I've opened an issue in the HoTT repo #1388

Paolo Giarrusso (Aug 27 2020 at 20:06):

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.

Karl Palmskog (Sep 16 2020 at 13:01):

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.

Ali Caglayan (Sep 16 2020 at 14:01):

I agree

Last updated: Sep 15 2024 at 13:02 UTC