Add Lean v3.18.4

[DonaldKellett]

Please complete the following information:

• Name: Lean
• Version: 3.18.2

---

👍 reaction might help.

[kazk]

I need some up to date example code for testing. Passing example with allowed axioms doesn't work any more because of

unknown identifier 'add_comm'
state:
n m : ℕ
⊢ n + m = m + n

For something that uses mathlib, I've been using this solution, but it doesn't work any more because of

/workspace/_target/deps/mathlib/src/meta/expr.lean:446:9
invalid definition, a declaration named 'expr.pi_arity' has already been declared

I'm using the following leanpkg.toml:

[package]
name = "lean-challenge"
version = "1.0"
lean_version = "leanprover-community/lean:3.18.2"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "e14ba7b059d149c69489d59003cae175ac45b24c"}

[kazk]

If you can update your examples, that'll be awesome. I just need something for CI to test that proper output is produced.

[DonaldKellett]

I've just been notified on the Zulip chat that 3.18.x is currently a bit buggy since mathlib is not yet fully working with it. I'll update the examples once that's fixed and ping you when it's done.

[DonaldKellett]

@kazk My examples have been updated to use Lean v3.18.4 (see leanpkg.toml at the bottom of the README for the corresponding mathlib commit), let's upgrade to Lean v3.18.4 on Codewars and see what breaks

[kazk]

v3.18.4 seems significantly faster than v3.11 and faster than v3.7.

For your allowed axioms example, v3.7 takes around 5s, v3.11 takes around 8s, and v3.18 is around 4s.
For mathlib example, v3.7 takes around 7s, v3.11 takes around 12s, and v3.18.4 takes about 4s.

These are on my laptop so it'll take longer on the server, but it's much faster.

31 kata on Codewars is not compatible with v3.18.4 and I'll update the wiki like before. I'll try deploying the new version some time this week.

[kazk]

Deployed and updated the list of kata to update.

[DonaldKellett]

@kazk Perhaps we can remove support for Lean 3.7 now that all Lean kata are compatible with 3.11 or above. As for migrating to 3.18, there are currently only 7 kata remaining to be upgraded.

[kazk]

Yeah, I'll do that. Thanks

[monadius]

All Lean kata are compatible with Lean 3.18 now. So both Lean 3.7 and Lean 3.11 may be removed.