From c404564a2b25f1ee4a0cb611904f944b0321f998 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 6 Jul 2024 19:53:50 -0700 Subject: [PATCH 1/2] chore: Bump Lean version to 4.10.0-rc1 --- Pantograph/Compile/Frontend.lean | 2 +- Pantograph/Environment.lean | 2 +- Pantograph/Goal.lean | 9 ++------- Pantograph/Version.lean | 2 +- flake.nix | 2 +- lean-toolchain | 2 +- 6 files changed, 7 insertions(+), 12 deletions(-) diff --git a/Pantograph/Compile/Frontend.lean b/Pantograph/Compile/Frontend.lean index 5cb3e63..3dbad85 100644 --- a/Pantograph/Compile/Frontend.lean +++ b/Pantograph/Compile/Frontend.lean @@ -52,7 +52,7 @@ def processOneCommand: Elab.Frontend.FrontendM (CompilationStep × Bool) := do let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos let s' := (← get).commandState let after := s'.env - let msgs := s'.messages.msgs.drop s.messages.msgs.size + let msgs := s'.messages.toList.drop s.messages.toList.length let trees := s'.infoState.trees.drop s.infoState.trees.size let ⟨_, fileName, fileMap⟩ := (← read).inputCtx return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index d5cdc3d..6d91abb 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -132,7 +132,7 @@ def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) : (hints := Lean.mkReducibilityHintsRegularEx 1) (safety := Lean.DefinitionSafety.safe) (all := []) - let env' ← match env.addDecl constant with + let env' ← match env.addDecl (← getOptions) constant with | .error e => do let options ← Lean.MonadOptions.getOptions let desc ← (e.toMessageData options).toString diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 46888e7..8c2324d 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -7,11 +7,6 @@ import Pantograph.Protocol import Pantograph.Tactic import Lean -def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := - { - msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false - } - namespace Pantograph open Lean @@ -178,7 +173,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab. try let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } if (← getThe Core.State).messages.hasErrors then - let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray + let messages := (← getThe Core.State).messages.toArray let errors ← (messages.map (·.data)).mapM fun md => md.toString return .failure errors let nextElabState ← MonadBacktrack.saveState @@ -223,7 +218,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): goal.checkNotAssigned `GoalState.assign goal.assign expr if (← getThe Core.State).messages.hasErrors then - let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray + let messages := (← getThe Core.State).messages.toArray let errors ← (messages.map (·.data)).mapM fun md => md.toString return .failure errors let prevMCtx := state.savedState.term.meta.meta.mctx diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index 207b597..f3bcf93 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,6 +1,6 @@ namespace Pantograph @[export pantograph_version] -def version := "0.2.16" +def version := "0.2.17" end Pantograph diff --git a/flake.nix b/flake.nix index ad40a3f..b96d5e2 100644 --- a/flake.nix +++ b/flake.nix @@ -6,7 +6,7 @@ flake-parts.url = "github:hercules-ci/flake-parts"; lean = { # Do not follow input's nixpkgs since it could cause build failures - url = "github:leanprover/lean4?ref=v4.8.0-rc1"; + url = "github:leanprover/lean4?ref=v4.10.0-rc1"; }; lspec = { url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114"; diff --git a/lean-toolchain b/lean-toolchain index d8a6d7e..d69d1ed 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0-rc1 +leanprover/lean4:v4.10.0-rc1 -- 2.44.1 From 9b1dd0ffda4d9b9122241da31747b15a55e0754d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 6 Jul 2024 19:58:55 -0700 Subject: [PATCH 2/2] chore: Update flake --- flake.lock | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/flake.lock b/flake.lock index 1a50363..c803f65 100644 --- a/flake.lock +++ b/flake.lock @@ -42,16 +42,16 @@ "nixpkgs-old": "nixpkgs-old" }, "locked": { - "lastModified": 1714704934, - "narHash": "sha256-q0kLyIahUXolkSrBZSegPF+R99WAH1YC96JfKoFntDE=", + "lastModified": 1719788866, + "narHash": "sha256-kB2cp1XJKODXiuiKp7J5OK+PFP+sOSBE5gdVNOKWCPI=", "owner": "leanprover", "repo": "lean4", - "rev": "dcccfb73cb247e9478220375ab7de03f7c67e505", + "rev": "3b58e0649156610ce3aeed4f7b5c652340c668d4", "type": "github" }, "original": { "owner": "leanprover", - "ref": "v4.8.0-rc1", + "ref": "v4.10.0-rc1", "repo": "lean4", "type": "github" } -- 2.44.1