search

codewars / codewars-runner-cli

Old CodeRunner project. See https://github.com/codewars/runner instead.
GNU Affero General Public License v3.0
402 stars 141 forks source link

Add Lean v3.18.4 #828

Closed DonaldKellett closed 4 years ago

DonaldKellett commented 4 years ago

Please complete the following information:

:+1: reaction might help.

kazk commented 4 years ago

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 commented 4 years ago

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

DonaldKellett commented 4 years ago

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 commented 4 years ago

@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 commented 4 years ago

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 commented 4 years ago

Deployed and updated the list of kata to update.

DonaldKellett commented 4 years ago

@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 commented 4 years ago

Yeah, I'll do that. Thanks

monadius commented 4 years ago

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