search

leanprover / reservoir

Package registry for Lean/Lake.
https://reservoir.lean-lang.org
Apache License 2.0
16 stars 1 forks source link

feat: build archive metrics #40

Closed tydeu closed 2 months ago

tydeu commented 2 months ago

Runs lake pack as part of the testbed and stores the archive size as part of the index. At the end of the testbed, logs the number of packed archives and average archive size for the testbed.