One of the lunch discussions during the recent ICFP 2023 week was about parallel parsing and I was then inspired to look up the Agda code of this paper:
"Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda"
Jean-Philippe Bernardy, Patrik Jansson
http://arxiv.org/abs/1601.07724

The basic idea is to compute a (sparse, upper triangular) matrix whose position (i,j) contains the parses from position i to j in the input string. The fact that it works is fascinating! The formalisation is an exercise in working with block matrices in several layers and keeping few requirements on the final matrix elements in the "leaves" but still synthesizing the necessary properties on the way up the "quad tree".

The Agda code was originally published on github in 2016 (using Agda version 2.4.2.3 and agda-stdlib-0.9) but as usual with code written in a living language (Agda) it did not type check anymore. It took almost two hours to figure out the changes needed to bring it up to date with current Agda 2.6.3 and stdlib 1.7.3:
  https://github.com/DSLsofMath/ValiantAgda

There were a number of (arguably minor) changes needed:

It would be interesting to investigate what it wold take to build tool support for this kind of code refactoring. The only tool support I had was the error messages from (current) Agda and the full repository history of stdlib on github.