[isabelle-dev] Slaying the hydra

Lars Hupel hupel at in.tum.de
Fri Oct 12 11:38:54 CEST 2018


Yesterday, Tobias observed an interesting problem:

$ hg pull
pulling from http://isabelle.in.tum.de/repos/testboard/
searching for changes
abort: HTTP Error 414: Request-URI Too Long

The cause is a combination of that repository being many-headed and
Mercurial trying to be too smart about pulling via HTTP(S).

I checked the situation and there were >400 heads in that repository. I
cleaned those and wanted to post the relevant command for posterity here:

hg strip -r "all() and not ancestors(revision_to_keep)"

Note that this is apparently not an atomic operation! During my
experiments at home interrupting a strip operation was more likely than
not to leave the repository in a corrupted state.

Cheers
Lars


More information about the isabelle-dev mailing list