Dave's Garage Benchmark

Stream: lean4

[ohhaimark]

The YouTube channel Dave's Garage initiated a benchmark of a bunch of languages. I have created a PR to add a Lean4 implementation (https://github.com/PlummersSoftwareLLC/Primes/pull/675). Feel free to check it out and try and improve things.

[Andrés Goens]

cool! Would be a nice kicker to add a proof that the sieve works, wouldn't it :grinning: ?

[Mario Carneiro]

Looking at the implementation, it is unfortunately not possible, because it makes use of Float.sqrt. There is probably another way to write it that avoids this

[ohhaimark]

Yeah, I just wanted to just get things working enough to PR before I try to write a proof friendly version.

[Mario Carneiro]

also Loop.forIn uses unbounded recursion

[Marc Huisinga]

leanprover/lean4:4.0.0-m2 is very old, but I guess it isn't fair to use a nightly version for a benchmark like that?

[ohhaimark]

@Marc Huisinga I wasn't aware of that. I just wanted to pin a specific version, so I avoided nightly.

[Marc Huisinga]

You can pin specific nightlies, e.g. leanprover/lean4:nightly-2021-08-24

[Marc Huisinga]

https://github.com/leanprover/lean4-nightly/releases

[ohhaimark]

Here is a tabulation of benchmarks including Lean4: https://plummerssoftwarellc.github.io/PrimeView/report?id=davepl-1630571740.json&hi=False&hf=False&hp=False&fi=&fp=&fa=&ff=&fb=&tp=True&sc=pp&sd=True