sieve of Eratosthenes benchmark

Stream: lean4

[Wrenna Robson]

I must be missing something - but I cannot see what the benchmark in lean4#12345 has to do with the sieve of Eratosthenes. divisorsList, as defined there, seems to output exactly those numbers less than n which divide n. But this is not what the sieve does - indeed it is the exact opposite of what the sieve does. It is notoriously easy to mis-implement the sieve, especially in a functional context, but this doesn't even seem to do that. What am I missing?

[Jovan Gerbscheid]

Let's tag the relevant person: @Bhavik Mehta

[Wojciech Różowski]

Actually that was me who added the benchmark for the upcoming cbv tactic and did mistakenly attribute the name "sieve of Eratosthenes" to the benchmark proposed by @Bhavik Mehta . I am happy to rename this to avoid further confusion.

[Bhavik Mehta]

I don't think this is meant to be a sieve of Eratosthenes benchmark, it's just a prime filter benchmark. That is, I think the PR description misnames it, but the benchmark is still valuable

[Bhavik Mehta]

(I think it's possible that this example was minimised from a true sieve benchmark, but I'm not certain, and you're correct that now it definitely doesn't do that)

[Wrenna Robson]

It looks like a pretty sensible benchmark aye, I just think the description is confusing. I think just tests/bench/speedcenter.exec.velcom.yaml needs changing (that's the only bit that mentions the sieve I think).