feat: fixes for v4.14.0-rc1

[andrewmw94]

Bump toolchain to 4.12 nightly-2024-10-21 v4.14.0-rc1

[andrewmw94]

When working on this, I ran into an issue where the tactics seem to be duplicated. For example:

.lake/build/bin/repl < test/all_tactics.in
Output:

{"tactics":
 [{"tactic": "have t := 37",
   "proofState": 0,
   "pos": {"line": 1, "column": 18},
   "goals": "⊢ Nat",
   "endPos": {"line": 1, "column": 30}},
  {"tactic": "exact t",
   "proofState": 1,
   "pos": {"line": 1, "column": 32},
   "goals": "t : Nat ⊢ Nat",
   "endPos": {"line": 1, "column": 39}},
  {"tactic": "have t := 37",
   "proofState": 2,
   "pos": {"line": 1, "column": 18},
   "goals": "⊢ Nat",
   "endPos": {"line": 1, "column": 30}},
  {"tactic": "exact t",
   "proofState": 3,
   "pos": {"line": 1, "column": 32},
   "goals": "t : Nat ⊢ Nat",
   "endPos": {"line": 1, "column": 39}}],
 "env": 0}

I suspect this is related to leanprover/lean4#3106 , but I don't understand the code well enough to be sure. If you have pointers, I'm happy to try to fix it.

[andrewmw94]

Dug into this a bit more. Adding let tactics := tactics.take (tactics.length / 2) to REPL/Main.lean gives close to the expected output. Unfortunately, the proof states for the repeated tactics still exist, so in an input file like test/by_cases.in the numbering isn't correct after sending the first command.
(These are ok)

{"cmd": "theorem foo (x : Int) : x = x := by sorry"}

{"proofState" : 0, "tactic": "by_cases h : x < 0"}

(These are not, proof state 1 is repeated from proof state 0)

{"proofState" : 1, "tactic": "case pos => rfl"}

{"proofState" : 1, "tactic": "all_goals sorry"}

If we change this to:

{"proofState" : 2, "tactic": "case pos => rfl"}

{"proofState" : 2, "tactic": "all_goals sorry"}

the test passes (with the same adjustments in the expected output).

[andrewmw94]

I played around a bit and it seems applying this patch to Lean would be sufficient to restore the previous behavior:

In /src/Lean/Elab/Frontend.lean

-  let st ← IO.processCommandsIncrementally inputCtx parserState commandState none
-  return st.toState
+  let (_, s) ← (Frontend.processCommands.run { inputCtx := inputCtx }).run { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
+  pure s

I'm not familiar enough with Lean's internals to know if the redundant proof states from IO.processCommandsIncrementally are expected. If so, should I update the tests to match the numbering of these states (that feels weird as I wouldn't expect the numbering to be stable between versions)? Another option is to add a IO.processCommandsNonIncremental function and make the REPL call that. Do you have other suggestions?

[Kha]

The following patch should fix the underlying issue, could you test it?

--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -102,7 +102,7 @@ partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext)
 where
   go initialSnap t commands :=
     let snap := t.get
-    let commands := commands.push snap.data.stx
+    let commands := commands.push snap.data
     if let some next := snap.nextCmdSnap? then
       go initialSnap next.task commands
     else
@@ -111,13 +111,13 @@ where
       let messages := toSnapshotTree initialSnap
         |>.getAll.map (·.diagnostics.msgLog)
         |>.foldl (· ++ ·) {}
-      let trees := toSnapshotTree initialSnap
-        |>.getAll.map (·.infoTree?) |>.filterMap id |>.toPArray'
+      let trees := commands.map (·.infoTree?) |>.filterMap id |>.toPArray'
       return {
         commandState := { snap.data.finishedSnap.get.cmdState with messages, infoState.trees := trees }
         parserState := snap.data.parserState
         cmdPos := snap.data.parserState.pos
-        inputCtx, initialSnap, commands
+        commands := commands.map (·.stx)
+        inputCtx, initialSnap
       }

[andrewmw94]

In all the examples I've looked at trees will be empty with the above code. I tried keeping trees := ... unchanged and adding a deduplication step based on the start and end stx of the Info associated with each element of trees. That gets rid of some but not all repetitions. Printing out .stx.formatStx (showInfo:= true) of the infos after removing duplicates, I see something like:

trees_with_dupes.size: 7
deduped.size: 4
string repr: (18:Tactic.refine:30
 18:"refine":30
 (18:Term.noImplicitLambda:30
  18:"no_implicit_lambda%":30
  (18:Term.have:30
   18:"have":30
   (Term.haveDecl (Term.haveIdDecl (Term.haveId "":23:`t:24:" ") [] [] "":25:":=":27:" " (num "":28:"37":30:"")))
   18:";":30
   (18:Term.syntheticHole:30 18:"?":30 18:"_":30))))(Tactic.exact "":32:"exact":37:" " "":38:`t:39:"")(Command.declaration
 (Command.declModifiers [] [] [] [] [] [])
 (Command.definition
  "":0:"def":3:" "
  (Command.declId "":4:`f:5:" " [])
  (Command.optDeclSig [] [(Term.typeSpec "":6:":":7:" " "":8:`Nat:11:" ")])
  (Command.declValSimple
   "":12:":=":14:" "
   (Term.byTactic
    "":15:"by":17:" "
    (Tactic.tacticSeq
     (Tactic.tacticSeq1Indented
      [(Tactic.tacticHave_
        "":18:"have":22:" "
        (Term.haveDecl (Term.haveIdDecl (Term.haveId "":23:`t:24:" ") [] [] "":25:":=":27:" " (num "":28:"37":30:""))))
       "":30:";":31:" "
       (Tactic.exact "":32:"exact":37:" " "":38:`t:39:"")])))
   (Termination.suffix [] [])
   [])
  []))(Command.eoi "":39:"":39:"")

[andrewmw94]

I made some more changes to the REPL and have andrewmw94@52b0c28 which seems to mostly work except when two commands have the same start and end locations (as in the final command of the below):

{"cmd": "theorem foo (x : Int) : x = x := by sorry"}

{"proofState" : 0, "tactic": "by_cases h : x < 0"}

{"proofState" : 1, "tactic": "case pos => rfl"}

{"proofState" : 1, "tactic": "all_goals sorry"}

Where we incorrectly deduplicate the second state for the all_goals command.

[Kha]

My bad, could you try the above fix with this line instead?

      let trees := commands.map (·.finishedSnap.get.infoTree?) |>.filterMap id |>.toPArray'

[andrewmw94]

Looks like that works (with a small change to the REPL). Thanks!

[Kha]

Thanks for testing, addressed in leanprover/lean4#5763

[andrewmw94]

I'll update this PR once leanprover/lean4#5763 is in nightly. I ran the tests locally with 4.12 + the patch above, and the only weird thing is
Expected output file test/H20231214.expected.out does not exist. Skipping test/H20231214.in. but it looks like that must be the case for the prior version as well.

[kim-em]

I'm hoping to merge this on Monday once v4.14.0-rc1 is available.