chore: Update Lean to v4.19.0 #205

Merged

aniva merged 2 commits from chore/toolchain into dev

2025-06-16 13:54:09 -07:00

aniva commented

2025-05-07 06:54:21 -07:00

Owner

No description provided.

aniva added this to the v0.3.2 milestone

2025-05-07 06:54:21 -07:00

aniva added the

category

chore

label

2025-05-07 06:54:21 -07:00

aniva self-assigned this

2025-05-07 06:54:21 -07:00

aniva added 1 commit

2025-05-07 06:54:22 -07:00

chore: Update Lean to v4.19.0 d41ec67a63

paperNeko was assigned by aniva

2025-05-09 10:02:06 -07:00

aniva commented

2025-05-12 13:49:43 -07:00

Author

Owner

There are tons of unit test failures for some reason.

aniva commented

2025-05-26 12:53:59 -07:00

Author

Owner

Tactic execution pipeline in a nutshell:

import Lean
open Lean

def fileName := "<example>"

structure Context where
  env: Environment
  coreContext : Core.Context := {
    currNamespace := Name.anonymous,
    openDecls := [],
    fileName,
    fileMap := { source := "", positions := #[0] }
  }
  elabContext : Elab.Term.Context := {
    declName? := .none,
    errToSorry := false
  }

abbrev M (m: Type → Type) := ReaderT Context m

def parse_expr (s: String): Elab.TermElabM Expr := do
  let syn? := Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := `term)
    (input := s)
    (fileName := fileName)
  let .ok syn := syn? | throwError "Parser not defined"
  let expr ← Elab.Term.elabType syn
  Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let expr ← instantiateMVars expr
  return expr

def start_tactic_state (expr: Expr): Elab.TermElabM Elab.Tactic.SavedState := do
  let mvar ← Meta.mkFreshExprMVar (some expr) (kind := .synthetic)
  let termState : Elab.Term.SavedState ← Elab.Term.saveState
  let tacticState : Elab.Tactic.SavedState := { term := termState, tactic := { goals := [mvar.mvarId!] }}
  IO.println "Tactic state started"
  return tacticState

def execute_tactic (state: Elab.Tactic.SavedState) (goalId: Nat) (tactic: String):
  Elab.TermElabM Elab.Tactic.SavedState := do
  let stx := Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := `tactic)
    (input := tactic)
    (fileName := fileName) |>.toOption |>.get!
  state.term.restore
  let tac : Elab.Tactic.TacticM Unit := set state.tactic *> Elab.Tactic.evalTactic stx
  let mvarId := state.tactic.goals[goalId]!
  Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let unsolvedGoals ← Elab.Tactic.run mvarId tac
  if (← getThe Core.State).messages.hasErrors then
    let messages := (← getThe Core.State).messages |>.toList.toArray
    let errors ← messages.mapM (·.toString)
    IO.println s!"{errors}"
    return state
  else
    unsolvedGoals.forM instantiateMVarDeclMVars
    let nextState : Elab.Tactic.SavedState := {
      term := (← Elab.Term.saveState),
      tactic := { goals := unsolvedGoals }
    }
    let goals ← unsolvedGoals.mapM fun g => do pure $ toString (← Meta.ppGoal g)
    IO.println s!"Tactic '{tactic}' succeeded."
    IO.println s!"{goals}"
    return nextState
def try_assign (state: Elab.Tactic.SavedState) (goalId: Nat) (expr: String):
  Elab.TermElabM Elab.Tactic.SavedState := do
  state.term.restore
  let mvarId := state.tactic.goals[goalId]!

  let expr := Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := `term)
    (input := expr)
    (fileName := fileName) |>.toOption |>.get!
  let goalType ← mvarId.getType

  let expr ← mvarId.withContext (Elab.Term.elabTerm (stx := expr) (expectedType? := .some goalType))

  mvarId.checkNotAssigned `try_assign
  mvarId.assign expr

  if (← getThe Core.State).messages.hasErrors then
    let messages := (← getThe Core.State).messages |>.toList.toArray
    let errors ← messages.mapM (·.toString)
    IO.println s!"{errors}"
    return state

  let prevMCtx := state.term.meta.meta.mctx
  let nextMCtx ← getMCtx
  -- Generate a list of mvarIds that exist in the parent state; Also test the
  -- assertion that the types have not changed on any mvars.
  let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
    if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
      assert! prevMVarDecl.type == mvarDecl.type
      return acc
    else
      return mvarId :: acc
    ) []
  let nextGoals ← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned))
  let nextState : Elab.Tactic.SavedState := {
    term := (← Elab.Term.saveState),
    tactic := { goals := nextGoals }
  }
  return nextState

def execute_term_elab (termElabM: Elab.TermElabM α): M IO (α × Core.State) := do
  let context ← read
  let metaM : MetaM α := termElabM.run' (ctx := context.elabContext)
  let coreM : CoreM α := metaM.run'
  let coreState : Core.State := { env := context.env }
  coreM.toIO context.coreContext coreState

def proof: M IO Unit := do
  let context ← read
  let (_, _) ← execute_term_elab <| do
    let expr ← parse_expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
    let state ← start_tactic_state expr
    let state ← execute_tactic state 0 "intro p q h"
    let branch ← try_assign state 0 "Or.inl (Or.inl h)"
  IO.println "Completed"


def main := do
  let env: Environment ← importModules
    (imports := #[`Init])
    (opts := {})
    (trustLevel := 1)
  proof |>.run { env := env }

Seems like the parser is not defined.

Tactic execution pipeline in a nutshell: ```lean import Lean open Lean def fileName := "<example>" structure Context where env: Environment coreContext : Core.Context := { currNamespace := Name.anonymous, openDecls := [], fileName, fileMap := { source := "", positions := #[0] } } elabContext : Elab.Term.Context := { declName? := .none, errToSorry := false } abbrev M (m: Type → Type) := ReaderT Context m def parse_expr (s: String): Elab.TermElabM Expr := do let syn? := Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := s) (fileName := fileName) let .ok syn := syn? | throwError "Parser not defined" let expr ← Elab.Term.elabType syn Elab.Term.synthesizeSyntheticMVarsNoPostponing let expr ← instantiateMVars expr return expr def start_tactic_state (expr: Expr): Elab.TermElabM Elab.Tactic.SavedState := do let mvar ← Meta.mkFreshExprMVar (some expr) (kind := .synthetic) let termState : Elab.Term.SavedState ← Elab.Term.saveState let tacticState : Elab.Tactic.SavedState := { term := termState, tactic := { goals := [mvar.mvarId!] }} IO.println "Tactic state started" return tacticState def execute_tactic (state: Elab.Tactic.SavedState) (goalId: Nat) (tactic: String): Elab.TermElabM Elab.Tactic.SavedState := do let stx := Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `tactic) (input := tactic) (fileName := fileName) |>.toOption |>.get! state.term.restore let tac : Elab.Tactic.TacticM Unit := set state.tactic *> Elab.Tactic.evalTactic stx let mvarId := state.tactic.goals[goalId]! Elab.Term.synthesizeSyntheticMVarsNoPostponing let unsolvedGoals ← Elab.Tactic.run mvarId tac if (← getThe Core.State).messages.hasErrors then let messages := (← getThe Core.State).messages |>.toList.toArray let errors ← messages.mapM (·.toString) IO.println s!"{errors}" return state else unsolvedGoals.forM instantiateMVarDeclMVars let nextState : Elab.Tactic.SavedState := { term := (← Elab.Term.saveState), tactic := { goals := unsolvedGoals } } let goals ← unsolvedGoals.mapM fun g => do pure $ toString (← Meta.ppGoal g) IO.println s!"Tactic '{tactic}' succeeded." IO.println s!"{goals}" return nextState def try_assign (state: Elab.Tactic.SavedState) (goalId: Nat) (expr: String): Elab.TermElabM Elab.Tactic.SavedState := do state.term.restore let mvarId := state.tactic.goals[goalId]! let expr := Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := expr) (fileName := fileName) |>.toOption |>.get! let goalType ← mvarId.getType let expr ← mvarId.withContext (Elab.Term.elabTerm (stx := expr) (expectedType? := .some goalType)) mvarId.checkNotAssigned `try_assign mvarId.assign expr if (← getThe Core.State).messages.hasErrors then let messages := (← getThe Core.State).messages |>.toList.toArray let errors ← messages.mapM (·.toString) IO.println s!"{errors}" return state let prevMCtx := state.term.meta.meta.mctx let nextMCtx ← getMCtx -- Generate a list of mvarIds that exist in the parent state; Also test the -- assertion that the types have not changed on any mvars. let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then assert! prevMVarDecl.type == mvarDecl.type return acc else return mvarId :: acc ) [] let nextGoals ← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)) let nextState : Elab.Tactic.SavedState := { term := (← Elab.Term.saveState), tactic := { goals := nextGoals } } return nextState def execute_term_elab (termElabM: Elab.TermElabM α): M IO (α × Core.State) := do let context ← read let metaM : MetaM α := termElabM.run' (ctx := context.elabContext) let coreM : CoreM α := metaM.run' let coreState : Core.State := { env := context.env } coreM.toIO context.coreContext coreState def proof: M IO Unit := do let context ← read let (_, _) ← execute_term_elab <| do let expr ← parse_expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))" let state ← start_tactic_state expr let state ← execute_tactic state 0 "intro p q h" let branch ← try_assign state 0 "Or.inl (Or.inl h)" IO.println "Completed" def main := do let env: Environment ← importModules (imports := #[`Init]) (opts := {}) (trustLevel := 1) proof |>.run { env := env } ``` Seems like the parser is not defined.

aniva added 1 commit

2025-06-16 13:46:11 -07:00

fix: Load environment extensions 0fa5ac335e