Commit 2024-04-28 22:28 0e05cbe2

View on Github →

feat: 'lake exe pole' computes the longest pole (#8361) See zulip discussion.

Estimated changes

Created LongestPole/Main.lean

added def Float.toStringDecimals

added def SpeedCenterAPI.RunResponse.instructions

added def SpeedCenterAPI.getRunResponse

added def SpeedCenterAPI.instructions

added def SpeedCenterAPI.runJson

added def headSha

added def longestPoleCLI

added def main

added def mathlib4RepoId

added def pole

added def runCmd

added def runCurl

added def slowestParents

added def totalInstructions

Created LongestPole/SpeedCenterJson.lean

added structure SpeedCenterAPI.CommitSource

added structure SpeedCenterAPI.Dimension

added structure SpeedCenterAPI.ErrorMessage

added structure SpeedCenterAPI.Measurement

added structure SpeedCenterAPI.Result

added structure SpeedCenterAPI.Run

added structure SpeedCenterAPI.RunResponse

added structure SpeedCenterAPI.Source

Modified Mathlib/Data/String/Defs.lean

modified def String.leftpad

added def String.rightpad

Modified lakefile.lean