08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
68 lines
2.3 KiB
Text
68 lines
2.3 KiB
Text
import Lean
|
|
|
|
/-! Basic tests, including edge cases. -/
|
|
example : Nat.gcd 0 0 = 0 := rfl
|
|
example : Nat.gcd 0 1 = 1 := rfl
|
|
example : Nat.gcd 0 17 = 17 := rfl
|
|
example : Nat.gcd 1 0 = 1 := rfl
|
|
example : Nat.gcd 17 0 = 17 := rfl
|
|
example : Nat.gcd 1 1 = 1 := rfl
|
|
example : Nat.gcd 1 17 = 1 := rfl
|
|
example : Nat.gcd 17 1 = 1 := rfl
|
|
example : Nat.gcd 2 2 = 2 := rfl
|
|
example : Nat.gcd 2 3 = 1 := rfl
|
|
example : Nat.gcd 2 4 = 2 := rfl
|
|
example : Nat.gcd 9 6 = 3 := rfl
|
|
|
|
/-!
|
|
We check that `Nat.gcd` is evaluated using bignum functions in the kernel.
|
|
|
|
Because of variations in run time on different operating systems during CI,
|
|
for the larger calculations we don't attempt to do any timing.
|
|
|
|
All of the "large" calculations below used to fail with
|
|
```
|
|
maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)
|
|
```
|
|
prior to lean4#2533.
|
|
-/
|
|
|
|
open Lean Elab Command in
|
|
elab "#fast" c:command : command => do
|
|
let start ← IO.monoMsNow
|
|
elabCommand c
|
|
let elapsed := (← IO.monoMsNow) - start
|
|
if elapsed > 1000 then throwError m!"Too slow! {elapsed}ms"
|
|
|
|
-- Used to take ~1500ms, now takes ~3ms.
|
|
#fast example : Nat.gcd 45 (Nat.gcd 15 85) = 5 := rfl
|
|
|
|
example : Nat.gcd (115249 * 180811) (115249*181081) = 115249 := rfl
|
|
|
|
/-- Mersenne primes. -/
|
|
def m (p : Nat) := 2^p - 1
|
|
|
|
/-- Largish primes, targeting <100ms GCD calculations. -/
|
|
def p_29 := 110503
|
|
def p_30 := 132049
|
|
def p_31 := 216091
|
|
def p_32 := 756839
|
|
def p_33 := 859433
|
|
|
|
set_option exponentiation.threshold 10000000
|
|
/- GCD with large prime factors on one side, and small primes on the other. -/
|
|
example : Nat.gcd (p_29 * p_30 * p_31 * p_32 * p_33) 2^(2^20) = 1 := rfl
|
|
/- GCD with two prime factors on both sides, including one in common. -/
|
|
example : Nat.gcd (m p_31 * m p_33) (m p_32 * m p_33) - m p_33 = 0 := rfl
|
|
/- GCD with many small prime factors. -/
|
|
example :
|
|
Nat.gcd (2^1 * 3^1 * 5^2 * 7^3 * 11^5 * 13^8) (2^8 * 3^5 * 5^3 * 7^2 * 11^1 * 13^1) =
|
|
2 * 3 * 5^2 * 7^2 * 11 * 13 := rfl
|
|
|
|
-- #eval Lean.maxSmallNat -- 9223372036854775807
|
|
def maxSmallNat := 9223372036854775807
|
|
|
|
example : maxSmallNat = 7^2 * 73 * 127 * 337 * 92737 * 649657 := rfl
|
|
-- Calculate GCDs of numbers on either side of `maxSmallNat`.
|
|
example : Nat.gcd (maxSmallNat - 92737) (maxSmallNat + 92737) = 185474 := rfl
|
|
example : Nat.gcd (maxSmallNat / 649657) (maxSmallNat * 649657) = 14197294936951 := rfl
|