Timing lean code

Stream: general

[Bolton Bailey]

To my great happiness, I have reached a point in my formalization of SNARKs project where there is a full proof of the soundness of (one version of) the well-known Groth '16 SNARK. Thanks to everyone on this forum for answering questions along the way, @Mario Carneiro in particular for all of his help with tactic programming.

I'm currently doing what I can to try to speed up the proof a little. My approach for benchmarking the proof has mainly been to just remove the olean file, then run time lean --make src/snarks/groth16typeIII/knowledge_soundness.lean. This has been roughly consistent - time reports that it takes about 33 minutes of cpu time on average, with a standard deviation of maybe 3 minutes or so.

Are there any good ways of making more fine-grained measurements of the amount of time taken by individual parts of the proof?

[Scott Morrison]

You might try set_option profiler true.

[Yakov Pechersky]

You might also want to include a CI script that auto-updates mathlib, and makes an issue when mathlib master is incompatible with your repo. This makes maintaining mathlib parity much more straightforward.

[Bryan Gin-ge Chen]

(There's an example script on the community website here.)