Comments (9)
All Lean kata are compatible with Lean 3.18 now. So both Lean 3.7 and Lean 3.11 may be removed.
from codewars-runner-cli.
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.
from codewars-runner-cli.
Deployed and updated the list of kata to update.
from codewars-runner-cli.
If you can update your examples, that'll be awesome. I just need something for CI to test that proper output is produced.
from codewars-runner-cli.
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.
from codewars-runner-cli.
@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
from codewars-runner-cli.
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"}
from codewars-runner-cli.
@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.
from codewars-runner-cli.
Yeah, I'll do that. Thanks
from codewars-runner-cli.
Related Issues (20)
- Update default test setup for Coq HOT 1
- Nim tests incorrectly shown as passing when actually faliing HOT 3
- Add Dart 2.8 HOT 1
- Add Rust 1.44 HOT 1
- Add Haxe HOT 14
- Add Crystal 0.34 HOT 2
- Update Python math/scientific libraries HOT 1
- `mcheck` breaks every C kata in new language version HOT 2
- Add Lean v3.11.0 (with mathlib) HOT 6
- Add NodeJS 12 HOT 1
- Add possibility to use scala testing frameworks for java solutions HOT 1
- C++ : updated kata to Clang8C++17 passed by function without body HOT 12
- Rust test runner: Please support Codewars Output format too HOT 20
- Add bit_set to rust HOT 1
- Add Lean 3.16.3 HOT 6
- Haxe: Type not found : Int64 HOT 3
- Exit code is 0 when crashing with memory error with Node 12 HOT 7
- CFML: java.lang.VerifyError:Expecting a stackmap frame at branch target HOT 5
- Add rest api documentation. HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from codewars-runner-cli.