Mario Carneiro
Mario Carneiro
It's not a false alarm this time, this came up during testing of `lean4lean`. Currently `Level.geq` differs from `level::is_geq` in the case of `max u v >= imax u v`:...
As [reported on zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unknown.20identifier.20in.20.60let.20var.20.3A.3D.20if.20let.60/near/396272940). The second commit fixes #2663, which looks similar but is a separate issue. I also fixed some typos and formatting issues in the debugging code in...
As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unreachable.20code.20reached.20in.20Lean.204.2E8.2E0/near/449286780). --- [](https://gitpod.io/from-referrer/)
Here is an example failing build of Mathport due to a moved upstream file: ``` $ lake build ✖ [63/1717] Running Mathlib.Init.ZeroOne error: no such file or directory (error code:...
MWE: ```lean import Lean elab (ident)? ("Foo") : command => sorry syntax "Fix " colGt ident : tactic example (x : Lean.TSyntax `ident) : Lean.MacroM Lean.Syntax := `(tactic| Fix $x:iden)...
It was still present in the namespaces `Std.Tactic.Lint` and `Std.CodeAction`.
These were previously moved to core (verbatim) in leanprover/lean4#3290.
This test is timing-sensitive, and has [spuriously failed](https://github.com/leanprover-community/batteries/actions/runs/10036728715/job/27735044947?pr=887) before. Increase the timings slightly to make it less easy to race.
* [ ] Depends on #1308 * [ ] Depends on https://github.com/digama0/polyml/compare/exportSmall Adds a new kernel type, `--trknl`. This is mostly the same as the standard kernel, but it uses...
This PR moves uses of `genericError` to custom errors when possible. * In two cases (root module not compiled, number of parameters doesn't match) the conditions appear to be impossible...