From adbb07af2d12d170fb097f8186be3526e8bade7b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 12 Apr 2024 22:39:47 -0700 Subject: [PATCH 1/4] 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 52e5b5df50fba53ead80135926cb838fc6771dce Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 15 Apr 2024 19:57:05 -0700 Subject: [PATCH 2/4] doc: README.md fix --- README.md | 58 +++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 37 insertions(+), 21 deletions(-) diff --git a/README.md b/README.md index 4a8f448..220e7a9 100644 --- a/README.md +++ b/README.md @@ -13,9 +13,15 @@ For Nix based workflow, see below. Install `elan` and `lake`. Execute ``` sh -make build/bin/pantograph +make ``` -setup the `LEAN_PATH` environment variable so it contains the library path of lean libraries. The libraries must be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`, +This builds the executable in `.lake/build/bin/pantograph`. + +To use Pantograph in a project environment, setup the `LEAN_PATH` environment +variable so it contains the library path of lean libraries. The libraries must +be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`, +the environment might be setup like this: + ``` sh LIB="../lib" LIB_MATHLIB="$LIB/mathlib4/lake-packages" @@ -23,7 +29,10 @@ export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATH LEAN_PATH=$LEAN_PATH build/bin/pantograph $@ ``` -The provided `flake.nix` has a develop environment with Lean already setup. +The `$LEAN_PATH` executable of any project can be extracted by +``` sh +lake env printenv LEAN_PATH +``` ## Executable Usage @@ -71,33 +80,38 @@ where the application of `assumption` should lead to a failure. ### Commands See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. -- `reset`: Delete all cached expressions and proof trees -- `expr.echo {"expr": , "type": }`: Determine the type of an expression and round-trip it -- `env.catalog`: Display a list of all safe Lean symbols in the current environment -- `env.inspect {"name": , "value": }`: Show the type and package of a +* `reset`: Delete all cached expressions and proof trees +* `stat`: Display resource usage +* `expr.echo {"expr": , "type": }`: Determine the type of an expression and format it +* `env.catalog`: Display a list of all safe Lean symbols in the current environment +* `env.inspect {"name": , "value": }`: Show the type and package of a given symbol; If value flag is set, the value is printed or hidden. By default only the values of definitions are printed. -- `options.set { key: value, ... }`: Set one or more options (not Lean options; those +* `options.set { key: value, ... }`: Set one or more options (not Lean options; those have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` -- `options.print`: Display the current set of options -- `goal.start {["name": ], ["expr": ], ["copyFrom": ]}`: Start a new goal from a given expression or symbol -- `goal.tactic {"stateId": , "goalId": , ["tactic": ], ["expr": - ]}`: Execute a tactic string on a given goal. `tactic` executes an - ordinary tactic, `expr` assigns an expression to the current goal, `have` - executes the have tactic, ``calc` (of the form `lhs op rhs`) executes one step - of `calc`, and `"conv": true`/`"conv": false` enters/exits conversion tactic - mode. -- `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: Continue from a proof state -- `goal.remove {"stateIds": []}"`: Remove a bunch of stored goals. -- `goal.print {"stateId": }"`: Print a goal state -- `stat`: Display resource usage +* `options.print`: Display the current set of options +* `goal.start {["name": ], ["expr": ], ["copyFrom": ]}`: + Start a new proof from a given expression or symbol +* `goal.tactic {"stateId": , "goalId": , ...}`: Execute a tactic string on a + given goal. The tactic is supplied as additional key-value pairs in one of the following formats: + - `{ "tactic": }`: Executes an ordinary tactic + - `{ "expr": }`: Assigns the given proof term to the current expression + - `{ "have": , "binderName": }`: Executes `have` and create a branch goal + - `{ "calc": }`: Executes one step of a `calc` tactic. Each step must + be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set + to the previous `rhs`. + - `{ "conv": }`: Enter or exit conversion tactic mode. In the case of + exit, the goal id is ignored. +* `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: Continue from a proof state +* `goal.remove {"stateIds": []}"`: Remove a bunch of stored goals. +* `goal.print {"stateId": }"`: Print a goal state ### Errors When an error pertaining to the execution of a command happens, the returning JSON structure is ``` json -{ error: "type", desc: "description" } +{ "error": "type", "desc": "description" } ``` Common error forms: * `command`: Indicates malformed command structure which results from either @@ -122,6 +136,8 @@ call Pantograph via this FFI since it provides a tremendous speed up. ## Developing +A Lean development shell is provided in the Nix flake. + ### Testing The tests are based on `LSpec`. To run tests, From 7531ad628cc7fc94a771e075cb5bc0c5c17d2730 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 15 Apr 2024 20:00:59 -0700 Subject: [PATCH 3/4] doc: Documentation about conditional arguments --- README.md | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 220e7a9..508d026 100644 --- a/README.md +++ b/README.md @@ -82,7 +82,8 @@ where the application of `assumption` should lead to a failure. See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. * `reset`: Delete all cached expressions and proof trees * `stat`: Display resource usage -* `expr.echo {"expr": , "type": }`: Determine the type of an expression and format it +* `expr.echo {"expr": , "type": }`: Determine the + type of an expression and format it * `env.catalog`: Display a list of all safe Lean symbols in the current environment * `env.inspect {"name": , "value": }`: Show the type and package of a given symbol; If value flag is set, the value is printed or hidden. By default @@ -94,16 +95,19 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va Start a new proof from a given expression or symbol * `goal.tactic {"stateId": , "goalId": , ...}`: Execute a tactic string on a given goal. The tactic is supplied as additional key-value pairs in one of the following formats: - - `{ "tactic": }`: Executes an ordinary tactic - - `{ "expr": }`: Assigns the given proof term to the current expression - - `{ "have": , "binderName": }`: Executes `have` and create a branch goal - - `{ "calc": }`: Executes one step of a `calc` tactic. Each step must + - `{ "tactic": }`: Execute an ordinary tactic + - `{ "expr": }`: Assign the given proof term to the current goal + - `{ "have": , "binderName": }`: Execute `have` and creates a branch goal + - `{ "calc": }`: Execute one step of a `calc` tactic. Each step must be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set to the previous `rhs`. - `{ "conv": }`: Enter or exit conversion tactic mode. In the case of exit, the goal id is ignored. -* `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: Continue from a proof state -* `goal.remove {"stateIds": []}"`: Remove a bunch of stored goals. +* `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: + Execute continuation/resumption + - `{ "branch": }`: Continue on branch state. The current state must have no goals. + - `{ "goals": }`: Resume the given goals +* `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list * `goal.print {"stateId": }"`: Print a goal state ### Errors From e165e41efa8a65628501f6b8390b14040eb0ac62 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 17 May 2024 20:31:45 -0700 Subject: [PATCH 4/4] 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