Consider cleaning the gh-pages branch up constantly

[ice1000]

Currently, the gh-pages branch has tons of commits, which might have drastically increased the size of this repo:

I wish someone can, like, clean up all the non-newest commits of this branch from time to time so our .git file contains less unnecessary junky files.

[MatthewDaggitt]

@ice1000 What would this involve? Squashing the commits down?

@gallais do you know of any automated tools/pages that might link to previous commits?

[gallais]

I do not understand what "cleaning" means in this context.

Note that the fact the history wasn't squashed was really helpful a couple of
times when a broken .travis.yml got rid of the doc for older versions of the
library.

[ice1000]

I do not understand what "cleaning" means in this context.

Like, as there are already 1,792 commits, we can squash the first 1,700 commits, as they are useless in general. We do want the doc to be still available when the CI is broken, but AFACT the most recent working commit is the only one needed for saving the broken CI, and I was talking about the non-newest commits.

[JacquesCarette]

Squashing in the main branch (and experimental) would be disastrous; but I think here the suggestion is just got gh-pages, which indeed seems quite reasonable.

[ice1000]

I'll test how a squashing makes the .git smaller.
This is how it looks like now:

~/SDK/agda-stdlib|experimental λ> git gc
~/SDK/agda-stdlib|experimental λ> du -sh .git
126M    .git

[ice1000]

It does not change after I cleaning something:

~/SDK/agda-stdlib|gh-pages λ> du -sh .git
126M    .git

I guess it's because the commits are also stored in the tags. :(