Commit 2026-01-30 13:30 a1c5c929

View on Github ā†’

chore: remove LongestPole (#34354) This PR removes the lake exe pole and lake exe unused tools, along with the LongestPole library and scripts/unused_in_pole.sh. These were early experiments in analyzing Mathlib's import structure and build times. Equivalent data is now available as part of the lakeprof report produced by radar.

  • depends on: #34555 šŸ¤– Prepared with Claude Code

Estimated changes

deleted def RadarAPI.getRunInfo
deleted def countLOC
deleted def headSha
deleted def longestPoleCLI
deleted def main
deleted def pole
deleted def runCmd
deleted def runCurl
deleted def slowestParents
deleted def totalInstructions
deleted structure RadarAPI.JsonGet
deleted def Rectangle.area
deleted def Rectangle.height
deleted def Rectangle.toString
deleted def Rectangle.width
deleted structure Rectangle
deleted def countDecls
deleted def main
deleted def unused
deleted def unusedImportsCLI