lean4
lean4 copied to clipboard
leanprover
fix: collect level parameters in evalExpr
elabEvalUnsafe already does something similar: it also instantiates universe metavariables, but it is not clear to me whether that is sensible here.
To be conservative, I leave it out of this PR.
See https://github.com/leanprover/lean4/pull/3090#discussion_r1432007590 for a comparison between #eval and Meta.evalExpr. This PR is not trying to fully align them, but just to fix one particular misalignment that I am impacted by.
Closes #3091
- ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-18 15:50:28)
- ✅ Mathlib branch lean-pr-testing-3090 has successfully built against this PR. (2023-12-20 12:34:38) View Log
- ✅ Mathlib branch lean-pr-testing-3090 has successfully built against this PR. (2023-12-20 13:12:04) View Log
It would be good to have a Mathlib build for this one. Could you rebase onto nightly-with-mathlib?
I'm afraid I probably have no time today to do so, but might later this week.
My figuring is that this is very unlikely to break anything, since the change only affects code that was previously producing kernel errors; but indeed it's good practice to test it anyway.
It would be good to have a Mathlib build for this one. Could you rebase onto
nightly-with-mathlib?
I did this rebase @semorrison, but I guess CI won't run until tomorrow?
It would be good to have a Mathlib build for this one. Could you rebase onto
nightly-with-mathlib?I did this rebase @semorrison, but I guess CI won't run until tomorrow?
The workflow is a bit racy; by the time it ran, a new nightly tag appeared (2023-12-19), but nightly-with-mathlib did not advance. I hope that #3097 will fix that. Once that hits master, I can re-trigger the workflow and then it hopefully works. Sorry for the delays.
Seems to work (https://github.com/leanprover/lean4/actions/runs/7274620683/job/19820906002), mathlib CI should be running
@semorrison, do you think this is ok as is? While there's some discussion above about instantiating metavariables, it's mainly about code that isn't part of this patch anyway; and the actual change is only two lines!
Just to note this now also impacts eval% in mathlib:
import Mathlib.Tactic.Eval
def foo.{u} (x : PUnit.{u}) : Nat := 37
-- fails without this PR
def bar.{u} (x : PUnit.{u}) : Nat := eval% foo.{u} PUnit.unit