From adbb07af2d12d170fb097f8186be3526e8bade7b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 12 Apr 2024 22:39:47 -0700 Subject: [PATCH 1/2] fix: Option setting in REPL --- Pantograph.lean | 1 + Pantograph/Library.lean | 17 ----------------- 2 files changed, 1 insertion(+), 17 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index f59bc11..c637303 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -81,6 +81,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty, printExprPretty := args.printExprPretty?.getD options.printExprPretty, printExprAST := args.printExprAST?.getD options.printExprAST, + printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars, noRepeat := args.noRepeat?.getD options.noRepeat, printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls, printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 6b8e2e2..6505fec 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -82,23 +82,6 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do def envCatalog: Lean.CoreM Protocol.EnvCatalogResult := Environment.catalog ({}: Protocol.EnvCatalog) -@[export pantograph_mk_options] -def mkOptions - (printJsonPretty: Bool) - (printExprPretty: Bool) - (printExprAST: Bool) - (noRepeat: Bool) - (printAuxDecls: Bool) - (printImplementationDetailHyps: Bool) - : Protocol.Options := { - printJsonPretty, - printExprPretty, - printExprAST, - noRepeat, - printAuxDecls, - printImplementationDetailHyps, - } - @[export pantograph_env_inspect_m] def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) := From e165e41efa8a65628501f6b8390b14040eb0ac62 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 17 May 2024 20:31:45 -0700 Subject: [PATCH 2/2] chore: Version bump to v4.8.0-rc1 --- Pantograph/Goal.lean | 4 ++-- flake.lock | 8 ++++---- flake.nix | 2 +- lean-toolchain | 2 +- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 484ff51..e6a59d0 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -90,7 +90,7 @@ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax Elab.Tactic.evalTactic stx if (← getThe Core.State).messages.hasErrors then let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray - let errors ← (messages.map Message.data).mapM fun md => md.toString + let errors ← (messages.map (·.data)).mapM fun md => md.toString return .error errors else return .ok (← MonadBacktrack.saveState) @@ -161,7 +161,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): goal.assign expr if (← getThe Core.State).messages.hasErrors then let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray - let errors ← (messages.map Message.data).mapM fun md => md.toString + let errors ← (messages.map (·.data)).mapM fun md => md.toString return .failure errors let prevMCtx := state.savedState.term.meta.meta.mctx let nextMCtx ← getMCtx diff --git a/flake.lock b/flake.lock index 39888a8..1a50363 100644 --- a/flake.lock +++ b/flake.lock @@ -42,16 +42,16 @@ "nixpkgs-old": "nixpkgs-old" }, "locked": { - "lastModified": 1711508550, - "narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=", + "lastModified": 1714704934, + "narHash": "sha256-q0kLyIahUXolkSrBZSegPF+R99WAH1YC96JfKoFntDE=", "owner": "leanprover", "repo": "lean4", - "rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2", + "rev": "dcccfb73cb247e9478220375ab7de03f7c67e505", "type": "github" }, "original": { "owner": "leanprover", - "ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2", + "ref": "v4.8.0-rc1", "repo": "lean4", "type": "github" } diff --git a/flake.nix b/flake.nix index 2458805..ad40a3f 100644 --- a/flake.nix +++ b/flake.nix @@ -5,8 +5,8 @@ nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-parts.url = "github:hercules-ci/flake-parts"; lean = { - url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2"; # Do not follow input's nixpkgs since it could cause build failures + url = "github:leanprover/lean4?ref=v4.8.0-rc1"; }; lspec = { url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114"; diff --git a/lean-toolchain b/lean-toolchain index c630636..d8a6d7e 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-03-27 +leanprover/lean4:v4.8.0-rc1