decide +revert not reverting

[hargoniX]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Consider:

theorem Bool.and_left (lhs rhs : Bool) (h : (lhs && rhs) = true) : lhs = true := by
  decide +revert

In this situation I would have expected the new +revert feature to just solve the goal,
given that:

theorem Bool.and_left (lhs rhs : Bool) (h : (lhs && rhs) = true) : lhs = true := by
  revert lhs rhs h
  decide

does work. However it throws:

expected type must not contain free or meta variables
  lhs = true

Expected behavior: decide +revert should close the goal

Actual behavior: decide +revert seemingly does not revert

Versions

nightly-2024-11-11

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[kmill]

I can't reproduce this on Lean 4.15.0, commit 281c07c
Target: arm64-apple-darwin24.1.0 macOS

What's your #version saying?

[kmill]

The full error message includes the line "Use the '+revert' option to automatically cleanup and revert free variables." Given that you're not including it, I'm guessing that you're accidentally on an old version and there's a red squiggle on the +.

[nomeata]

Something is strange. On live.lean-lang.org today with

Lean 4.15.0-nightly-2024-11-11
Target: x86_64-unknown-linux-gnu

I get red squiggly lines under decide +, but it seems to work and #proof shows the full proofs. Didn’t check locally yet.

Oh, and now as I switch back to that tab it's gone. Reloading makes it appear again. Maybe unrelated to the present issue.

[hargoniX]

I just built master on 5e01e62 and tried

theorem Bool.and_left (lhs rhs : Bool) (h : (lhs && rhs) = true) : lhs = true := by
  decide +revert

again and it is still erroring with the same error message for me. No error on the +revert only the error I reported. Though interestingly it only happens when I work in Std not when I work on files in e.g. tests/lean/run. Is there a bootstrapping problem or a missed update-stage0 cycle here?

[kmill]

That's correct, there has not been a stage0 update since this feature was added, so it can't be used from within Lean yet. I generally don't do stage0 updates myself unless they are necessary -- I've just triggered the update-stage0 workflow for you.

I'm wondering if the issue template should mention that you should verify that you aren't using the stage0 compiler. You basically were using the 2024-11-3 nightly when reporting this issue.

[nomeata]

Is the nightly release as available through live.lean-lang.org freshly bootstrapped? Should it? Henrik did tick the box next to “I tested it on live.lean-lang.org”, and ideally that is a reliable way to test mwe's.

[kmill]

Before doing the stage0 update, I also tried it on live.lean-lang.org @nomeata, at least with the 4.15.0-nightly-2024-11-12 edition, and I couldn't see the error.

I don't understand how live.lean-lang.org would have any staging problems. This is all being run serverside, right? so there shouldn't be any caching issues? How could the red squiggles be showing how it would look in the older version but act as if it were the newer version. Did you copy/paste the example @nomeata? or did you type the tactic in manually? I could see the the squiggles happening if you had decide + in the buffer and then finished it by adding revert in a second step.

[nomeata]

Right, I also couldn’t see Henrik’s error just (possibly unrelated) other strange behavior. @hargoniX, did you actually “Test your test case against the latest nightly release” as checked, or is this just evidence for my theory that these issue template checkboxes are just mostly ignored by people :-)

I wonder if the phantom red squiggly lines are a consequence of leanprover-community/lean4web#41, where the are actually both versions running on the server. Actually, this is rather likely.

(I can trigger that behavior by going directly to https://live.lean-lang.org/#project=lean-nightly&codez=C4Cwpg9gTmC2AEAhCEA2A6AhgOwCYH1UwAzYeAClRAGd4ob4AuJFVASgpCYqtoDI+dGhwC88YFACuYDs17wxE6UzEAjAJ4AoePFxgAxgEs98ANQwAbmCjAgA, or by reloading, but not by interactively writing and then switching versions.)

[hargoniX]

I did indeed merely run it within my current Lean build at the time which was at the nightly commit of that day so I had naively assumed it should behave the same but forgotten about stage0.

[nomeata]

Fixed on nightly, right?