From 8b67e7006aa242e178dcb978585c5473abaac428 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 5 Feb 2024 11:49:01 -0800 Subject: [PATCH 01/30] feat: Add lake and lean to the package output --- flake.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/flake.nix b/flake.nix index 356323f..02de0a1 100644 --- a/flake.nix +++ b/flake.nix @@ -30,6 +30,7 @@ in rec { packages = project // { inherit (leanPkgs) lean; + lake = leanPkgs.Lake-Main.executable; default = packages.executable; }; devShells.default = project.devShell; From 3e321516f7852dc2c2c601ccc1f3c07aba6b03c3 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 13 Feb 2024 15:30:56 -0500 Subject: [PATCH 02/30] chore: Expose `leanPkgs` in flake --- flake.nix | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index 02de0a1..7610209 100644 --- a/flake.nix +++ b/flake.nix @@ -29,8 +29,7 @@ }; in rec { packages = project // { - inherit (leanPkgs) lean; - lake = leanPkgs.Lake-Main.executable; + inherit leanPkgs; default = packages.executable; }; devShells.default = project.devShell; From d57612ec71e9f0416d1e42dc01f030522abbc901 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 15 Feb 2024 14:47:09 -0800 Subject: [PATCH 03/30] test: Delayed metavariable assignment --- Test/Proofs.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 07e4cea..85ba66d 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -232,6 +232,11 @@ def proof_or_comm: TestM Unit := do addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone + let state2parent ← serialize_expression_ast state2.parentExpr?.get! (sanitize := false) + -- This is due to delayed assignment + addTest $ LSpec.test "(2 parent)" (state2parent == + "((:mv _uniq.45) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") + let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state | other => do From 075bec6da23ee2b4545e0b2865b7a134d64940d0 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 6 Mar 2024 15:26:35 -0800 Subject: [PATCH 04/30] feat: Output shared library in flake --- flake.nix | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/flake.nix b/flake.nix index 7610209..9f586f6 100644 --- a/flake.nix +++ b/flake.nix @@ -28,9 +28,10 @@ src = ./.; }; in rec { - packages = project // { - inherit leanPkgs; - default = packages.executable; + packages = { + inherit (leanPkgs) lean lean-all; + inherit (project) sharedLib executable; + default = project.executable; }; devShells.default = project.devShell; }; From ecacf2107c5c56f94810c4f1eeedf6ac8bb153ec Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 6 Mar 2024 15:27:22 -0800 Subject: [PATCH 05/30] feat(build): Add shared facet for lean_lib --- lakefile.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/lakefile.lean b/lakefile.lean index f0832e2..89ad70f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,6 +4,7 @@ open Lake DSL package pantograph lean_lib Pantograph { + defaultFacets := #[LeanLib.sharedFacet] } @[default_target] From 021d0b5b7d10b821abb0e07f1341caa9bca8b405 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 8 Mar 2024 23:50:44 -0800 Subject: [PATCH 06/30] feat: Add exported version function --- Pantograph.lean | 1 + Pantograph/Library.lean | 8 ++++++++ 2 files changed, 9 insertions(+) create mode 100644 Pantograph/Library.lean diff --git a/Pantograph.lean b/Pantograph.lean index 46729fc..90ce2d2 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -2,6 +2,7 @@ import Pantograph.Goal import Pantograph.Protocol import Pantograph.Serial import Pantograph.Environment +import Pantograph.Library import Lean.Data.HashMap namespace Pantograph diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean new file mode 100644 index 0000000..330d84d --- /dev/null +++ b/Pantograph/Library.lean @@ -0,0 +1,8 @@ +import Pantograph.Version + +namespace Pantograph + +@[export pantograph_version] +def pantograph_version: String := version + +end Pantograph From 863c6d9e7d8342f833a05091758ffb30c2f7bc8f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 9 Mar 2024 16:50:36 -0800 Subject: [PATCH 07/30] feat(lib): Catalog command FFI --- Main.lean | 53 +++--------------------------- Pantograph.lean | 3 +- Pantograph/Environment.lean | 4 +-- Pantograph/Library.lean | 64 ++++++++++++++++++++++++++++++++++++- 4 files changed, 72 insertions(+), 52 deletions(-) diff --git a/Main.lean b/Main.lean index 68d1a3e..7c36db2 100644 --- a/Main.lean +++ b/Main.lean @@ -2,6 +2,7 @@ import Lean.Data.Json import Lean.Environment import Pantograph.Version +import Pantograph.Library import Pantograph -- Main IO functions @@ -39,35 +40,6 @@ partial def loop : MainM Unit := do IO.println str loop -namespace Lean - -/-- This is better than the default version since it handles `.` and doesn't - crash the program when it fails. -/ -def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO Options := do - let ps := (entry.splitOn "=").map String.trim - let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form ' = '" - let key := key.toName - let defValue ← getOptionDefaultValue key - match defValue with - | DataValue.ofString _ => pure $ opts.setString key val - | DataValue.ofBool _ => - match val with - | "true" => pure $ opts.setBool key true - | "false" => pure $ opts.setBool key false - | _ => throw s!"invalid Bool option value '{val}'" - | DataValue.ofName _ => pure $ opts.setName key val.toName - | DataValue.ofNat _ => - match val.toNat? with - | none => throw s!"invalid Nat option value '{val}'" - | some v => pure $ opts.setNat key v - | DataValue.ofInt _ => - match val.toInt? with - | none => throw s!"invalid Int option value '{val}'" - | some v => pure $ opts.setInt key v - | DataValue.ofSyntax _ => throw s!"invalid Syntax option value" - -end Lean - unsafe def main (args: List String): IO Unit := do -- NOTE: A more sophisticated scheme of command line argument handling is needed. @@ -79,32 +51,17 @@ unsafe def main (args: List String): IO Unit := do Lean.enableInitializersExecution Lean.initSearchPath (← Lean.findSysroot) - let options? ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none) - |>.foldlM Lean.setOptionFromString' Lean.Options.empty - |>.run - let options ← match options? with - | .ok options => pure options - | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}" + let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none) + |>.toArray |> createCoreContext let imports:= args.filter (λ s => ¬ (s.startsWith "--")) - - let env ← Lean.importModules - (imports := imports.toArray.map (λ str => { module := str.toName, runtimeOnly := false })) - (opts := {}) - (trustLevel := 1) + let coreState ← createCoreState imports.toArray let context: Context := { imports } - let coreContext: Lean.Core.Context := { - currNamespace := Lean.Name.str .anonymous "Aniva" - openDecls := [], -- No 'open' directives needed - fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] }, - options := options - } try let coreM := loop.run context |>.run' {} IO.println "ready." - discard <| coreM.toIO coreContext { env := env } + discard <| coreM.toIO coreContext coreState catch ex => IO.println "Uncaught IO exception" IO.println ex.toString diff --git a/Pantograph.lean b/Pantograph.lean index 90ce2d2..f1f194c 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -71,7 +71,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let nGoals := state.goalStates.size return .ok { nGoals } env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do - Environment.catalog args + let result ← Environment.catalog args + return .ok result env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do let state ← get Environment.inspect args state.options diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index b823e8f..df0bc7f 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -30,13 +30,13 @@ def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String : if is_symbol_unsafe_or_internal n info then Option.none else Option.some <| to_compact_symbol_name n info -def catalog (_: Protocol.EnvCatalog): CoreM (Protocol.CR Protocol.EnvCatalogResult) := do +def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do let env ← Lean.MonadEnv.getEnv let names := env.constants.fold (init := #[]) (λ acc name info => match to_filtered_symbol name info with | .some x => acc.push x | .none => acc) - return .ok { symbols := names } + return { symbols := names } def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do let env ← Lean.MonadEnv.getEnv let name := args.name.toName diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 330d84d..5b5e954 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -1,8 +1,70 @@ import Pantograph.Version +import Pantograph.Environment +import Pantograph.Protocol +import Lean + + +namespace Lean + +/-- This is better than the default version since it handles `.` and doesn't + crash the program when it fails. -/ +def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO Options := do + let ps := (entry.splitOn "=").map String.trim + let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form ' = '" + let key := key.toName + let defValue ← getOptionDefaultValue key + match defValue with + | DataValue.ofString _ => pure $ opts.setString key val + | DataValue.ofBool _ => + match val with + | "true" => pure $ opts.setBool key true + | "false" => pure $ opts.setBool key false + | _ => throw s!"invalid Bool option value '{val}'" + | DataValue.ofName _ => pure $ opts.setName key val.toName + | DataValue.ofNat _ => + match val.toNat? with + | none => throw s!"invalid Nat option value '{val}'" + | some v => pure $ opts.setNat key v + | DataValue.ofInt _ => + match val.toInt? with + | none => throw s!"invalid Int option value '{val}'" + | some v => pure $ opts.setInt key v + | DataValue.ofSyntax _ => throw s!"invalid Syntax option value" + +end Lean namespace Pantograph @[export pantograph_version] -def pantograph_version: String := version +def pantographVersion: String := version + +/-- Creates a Core.Context object needed to run all monads -/ +@[export pantograph_create_core_context] +def createCoreContext (options: Array String): IO Lean.Core.Context := do + let options? ← options.foldlM Lean.setOptionFromString' Lean.Options.empty |>.run + let options ← match options? with + | .ok options => pure options + | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}" + return { + currNamespace := Lean.Name.str .anonymous "Aniva" + openDecls := [], -- No 'open' directives needed + fileName := "", + fileMap := { source := "", positions := #[0], lines := #[1] }, + options := options + } + +@[export pantograph_create_core_state] +def createCoreState (imports: Array String): IO Lean.Core.State := do + let env ← Lean.importModules + (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false })) + (opts := {}) + (trustLevel := 1) + return { env := env } + +@[export pantograph_catalog] +def catalog (cc: Lean.Core.Context) (cs: Lean.Core.State): IO Protocol.EnvCatalogResult := do + let coreM: Lean.CoreM _ := Environment.catalog ({}: Protocol.EnvCatalog) + let (result, _) ← coreM.toIO cc cs + return result end Pantograph From 4706df22179a73c25af3ba9cb65ec4e3ee96b177 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 9 Mar 2024 19:36:25 -0800 Subject: [PATCH 08/30] feat(lib): Search path function --- Main.lean | 3 +-- Pantograph/Library.lean | 6 ++++++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/Main.lean b/Main.lean index 7c36db2..de73033 100644 --- a/Main.lean +++ b/Main.lean @@ -48,8 +48,7 @@ unsafe def main (args: List String): IO Unit := do println! s!"{version}" return - Lean.enableInitializersExecution - Lean.initSearchPath (← Lean.findSysroot) + initSearch "" let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none) |>.toArray |> createCoreContext diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 5b5e954..07e4656 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -38,6 +38,12 @@ namespace Pantograph @[export pantograph_version] def pantographVersion: String := version +/-- Adds the given paths to Lean package search path -/ +@[export pantograph_init_search] +unsafe def initSearch (sp: String): IO Unit := do + Lean.enableInitializersExecution + Lean.initSearchPath (← Lean.findSysroot) (sp := System.SearchPath.parse sp) + /-- Creates a Core.Context object needed to run all monads -/ @[export pantograph_create_core_context] def createCoreContext (options: Array String): IO Lean.Core.Context := do From ca89d671cc1b83acff63247b688eb92acb7c7398 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 9 Mar 2024 20:33:36 -0800 Subject: [PATCH 09/30] refactor: Move some functions to `Library.lean` --- Pantograph.lean | 28 +------------------- Pantograph/Library.lean | 57 +++++++++++++++++++++++++++++++++++++--- Pantograph/Protocol.lean | 2 +- Pantograph/Serial.lean | 2 +- 4 files changed, 57 insertions(+), 32 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index f1f194c..f9b5dc5 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -22,14 +22,6 @@ abbrev MainM := ReaderT Context (StateT State Lean.CoreM) -- certain monadic features in `MainM` abbrev CR α := Except Protocol.InteractionError α -def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α := - metaM.run' -def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α := - termElabM.run' (ctx := { - declName? := .none, - errToSorry := false, - }) |>.run' - def execute (command: Protocol.Command): MainM Lean.Json := do let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := match Lean.fromJson? command.payload with @@ -57,9 +49,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do errorCommand s!"Unknown command {cmd}" return Lean.toJson error where - errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } - errorCommand := errorI "command" - errorIndex := errorI "index" -- Command Functions reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get @@ -80,22 +69,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Environment.addDecl args expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do let state ← get - let env ← Lean.MonadEnv.getEnv - let syn ← match syntax_from_str env args.expr with - | .error str => return .error $ errorI "parsing" str - | .ok syn => pure syn - runTermElabM (do - match ← syntax_to_expr syn with - | .error str => return .error $ errorI "elab" str - | .ok expr => do - try - let type ← Lean.Meta.inferType expr - return .ok { - type := (← serialize_expression (options := state.options) type), - expr := (← serialize_expression (options := state.options) expr) - } - catch exception => - return .error $ errorI "typing" (← exception.toMessageData.toString)) + exprEcho args state.options options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do let state ← get let options := state.options diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 07e4656..cdc112f 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -3,7 +3,6 @@ import Pantograph.Environment import Pantograph.Protocol import Lean - namespace Lean /-- This is better than the default version since it handles `.` and doesn't @@ -35,6 +34,18 @@ end Lean namespace Pantograph +def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α := + metaM.run' +def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α := + termElabM.run' (ctx := { + declName? := .none, + errToSorry := false, + }) |>.run' + +def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } +def errorCommand := errorI "command" +def errorIndex := errorI "index" + @[export pantograph_version] def pantographVersion: String := version @@ -67,10 +78,50 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do (trustLevel := 1) return { env := env } -@[export pantograph_catalog] -def catalog (cc: Lean.Core.Context) (cs: Lean.Core.State): IO Protocol.EnvCatalogResult := do +@[export pantograph_env_catalog] +def envCatalog (cc: Lean.Core.Context) (cs: Lean.Core.State): IO Protocol.EnvCatalogResult := do let coreM: Lean.CoreM _ := Environment.catalog ({}: Protocol.EnvCatalog) let (result, _) ← coreM.toIO cc cs return result +@[export pantograph_env_inspect] +def envInspect (cc: Lean.Core.Context) (cs: Lean.Core.State) + (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options): IO (Protocol.CR Protocol.EnvInspectResult) := do + let coreM: Lean.CoreM _ := Environment.inspect ({ + name, value? := .some value, dependency?:= .some dependency + }: Protocol.EnvInspect) options + let (result, _) ← coreM.toIO cc cs + return result + +@[export pantograph_env_add] +def envAdd (cc: Lean.Core.Context) (cs: Lean.Core.State) + (name: String) (type: String) (value: String) (isTheorem: Bool): IO (Protocol.CR Protocol.EnvAddResult) := do + let coreM: Lean.CoreM _ := Environment.addDecl { name, type, value, isTheorem } + let (result, _) ← coreM.toIO cc cs + return result + +def exprEcho (args: Protocol.ExprEcho) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do + let env ← Lean.MonadEnv.getEnv + let syn ← match syntax_from_str env args.expr with + | .error str => return .error $ errorI "parsing" str + | .ok syn => pure syn + runTermElabM (do + match ← syntax_to_expr syn with + | .error str => return .error $ errorI "elab" str + | .ok expr => do + try + let type ← Lean.Meta.inferType expr + return .ok { + type := (← serialize_expression options type), + expr := (← serialize_expression options expr) + } + catch exception => + return .error $ errorI "typing" (← exception.toMessageData.toString)) + +@[export pantograph_expr_echo] +def exprEchoExport (cc: Lean.Core.Context) (cs: Lean.Core.State) (expr: String) (options: @&Protocol.Options): IO (Protocol.CR Protocol.ExprEchoResult) := do + let coreM: Lean.CoreM _ := exprEcho { expr } options + let (result, _) ← coreM.toIO cc cs + return result + end Pantograph diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 84e0cc2..5015ad1 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -163,7 +163,7 @@ structure EnvAdd where name: String type: String value: String - isTheorem?: Bool + isTheorem: Bool deriving Lean.FromJson structure EnvAddResult where deriving Lean.ToJson diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 38d1f14..547b3dc 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -157,7 +157,7 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta | .instImplicit => " :instImplicit" of_name (name: Name) := name_to_ast name sanitize -def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.Expression := do +def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do let pp := toString (← Meta.ppExpr e) let pp?: Option String := match options.printExprPretty with | true => .some pp From d958dbed9dd6bc3210b34170b87eec4969059bfa Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 10 Mar 2024 06:41:35 -0700 Subject: [PATCH 10/30] feat(lib): CoreM execution function --- Pantograph.lean | 5 +++- Pantograph/Library.lean | 63 +++++++++++++++++++++++------------------ 2 files changed, 40 insertions(+), 28 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index f9b5dc5..ad563f0 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -69,7 +69,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Environment.addDecl args expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do let state ← get - exprEcho args state.options + let expr ← match ← exprParse args.expr with + | .ok expr => pure $ expr + | .error e => return .error e + exprPrint expr state.options options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do let state ← get let options := state.options diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index cdc112f..a8c0ce7 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -1,6 +1,7 @@ -import Pantograph.Version import Pantograph.Environment +import Pantograph.Goal import Pantograph.Protocol +import Pantograph.Version import Lean namespace Lean @@ -70,6 +71,7 @@ def createCoreContext (options: Array String): IO Lean.Core.Context := do options := options } +/-- Creates a Core.State object needed to run all monads -/ @[export pantograph_create_core_state] def createCoreState (imports: Array String): IO Lean.Core.State := do let env ← Lean.importModules @@ -78,11 +80,14 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do (trustLevel := 1) return { env := env } +/-- Execute a `CoreM` monad -/ +@[export pantograph_exec_core] +def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α): IO (α × Lean.Core.State) := + coreM.toIO context state + @[export pantograph_env_catalog] -def envCatalog (cc: Lean.Core.Context) (cs: Lean.Core.State): IO Protocol.EnvCatalogResult := do - let coreM: Lean.CoreM _ := Environment.catalog ({}: Protocol.EnvCatalog) - let (result, _) ← coreM.toIO cc cs - return result +def envCatalog: Lean.CoreM Protocol.EnvCatalogResult := + Environment.catalog ({}: Protocol.EnvCatalog) @[export pantograph_env_inspect] def envInspect (cc: Lean.Core.Context) (cs: Lean.Core.State) @@ -100,28 +105,32 @@ def envAdd (cc: Lean.Core.Context) (cs: Lean.Core.State) let (result, _) ← coreM.toIO cc cs return result -def exprEcho (args: Protocol.ExprEcho) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do - let env ← Lean.MonadEnv.getEnv - let syn ← match syntax_from_str env args.expr with - | .error str => return .error $ errorI "parsing" str - | .ok syn => pure syn - runTermElabM (do - match ← syntax_to_expr syn with - | .error str => return .error $ errorI "elab" str - | .ok expr => do - try - let type ← Lean.Meta.inferType expr - return .ok { - type := (← serialize_expression options type), - expr := (← serialize_expression options expr) - } - catch exception => - return .error $ errorI "typing" (← exception.toMessageData.toString)) +@[export pantograph_expr_parse] +def exprParse (s: String): Lean.CoreM (Protocol.CR Lean.Expr) := do + let env ← Lean.MonadEnv.getEnv + let syn ← match syntax_from_str env s with + | .error str => return .error $ errorI "parsing" str + | .ok syn => pure syn + runTermElabM (do + match ← syntax_to_expr syn with + | .error str => return .error $ errorI "elab" str + | .ok expr => return .ok expr) -@[export pantograph_expr_echo] -def exprEchoExport (cc: Lean.Core.Context) (cs: Lean.Core.State) (expr: String) (options: @&Protocol.Options): IO (Protocol.CR Protocol.ExprEchoResult) := do - let coreM: Lean.CoreM _ := exprEcho { expr } options - let (result, _) ← coreM.toIO cc cs - return result +@[export pantograph_expr_print] +def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do + let termElabM: Lean.Elab.TermElabM _ := + try + let type ← Lean.Meta.inferType expr + return .ok { + type := (← serialize_expression options type), + expr := (← serialize_expression options expr) + } + catch exception => + return .error $ errorI "typing" (← exception.toMessageData.toString) + runTermElabM termElabM + +@[export pantograph_goal_start] +def goalStart (expr: Lean.Expr): Lean.CoreM GoalState := + runTermElabM (GoalState.create expr) end Pantograph From f42a27e0366a6f5fa858ffea1379675236494377 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 10 Mar 2024 08:13:10 -0700 Subject: [PATCH 11/30] feat(lib): Expose goal state interface --- Pantograph.lean | 24 +++++++--------- Pantograph/Library.lean | 62 +++++++++++++++++++++++++--------------- Pantograph/Protocol.lean | 2 +- Pantograph/Version.lean | 1 + 4 files changed, 52 insertions(+), 37 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index ad563f0..cc2471f 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -49,6 +49,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do errorCommand s!"Unknown command {cmd}" return Lean.toJson error where + errorCommand := errorI "command" + errorIndex := errorI "index" -- Command Functions reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get @@ -93,14 +95,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do let state ← get let env ← Lean.MonadEnv.getEnv - let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with - | .some expr, .none => - (match syntax_from_str env expr with - | .error str => return .error <| errorI "parsing" str - | .ok syn => do - (match ← syntax_to_expr syn with - | .error str => return .error <| errorI "elab" str - | .ok expr => return .ok (← GoalState.create expr))) + let expr?: Except Protocol.InteractionError GoalState ← runTermElabM (match args.expr, args.copyFrom with + | .some expr, .none => do + match ← exprParse expr with + | .ok expr => return .ok (← GoalState.create expr) + | .error e => return .error e | .none, .some copyFrom => (match env.find? <| copyFrom.toName with | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" @@ -123,9 +122,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .some goalState => do let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with | .some tactic, .none => do - pure ( Except.ok (← runTermElabM <| GoalState.execute goalState args.goalId tactic)) + pure ( Except.ok (← goalTactic goalState args.goalId tactic)) | .none, .some expr => do - pure ( Except.ok (← runTermElabM <| GoalState.tryAssign goalState args.goalId expr)) + pure ( Except.ok (← goalTryAssign goalState args.goalId expr)) | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied") match nextGoalState? with | .error error => return .error error @@ -157,8 +156,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .none => return .error $ errorIndex s!"Invalid state index {branchId}" | .some branch => pure $ target.continue branch | .none, .some goals => - let goals := goals.map (λ name => { name := name.toName }) - pure $ target.resume goals + pure $ goalResume target goals | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" match nextState? with | .error error => return .error <| errorI "structure" error @@ -168,7 +166,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do goalStates := state.goalStates.insert nextStateId nextGoalState, nextId := state.nextId + 1 } - let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) |>.run' + let goals ← goalSerialize nextGoalState (options := state.options) return .ok { nextStateId, goals, diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index a8c0ce7..b1a6864 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -1,6 +1,7 @@ import Pantograph.Environment import Pantograph.Goal import Pantograph.Protocol +import Pantograph.Serial import Pantograph.Version import Lean @@ -44,11 +45,6 @@ def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α := }) |>.run' def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } -def errorCommand := errorI "command" -def errorIndex := errorI "index" - -@[export pantograph_version] -def pantographVersion: String := version /-- Adds the given paths to Lean package search path -/ @[export pantograph_init_search] @@ -82,30 +78,27 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do /-- Execute a `CoreM` monad -/ @[export pantograph_exec_core] -def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α): IO (α × Lean.Core.State) := +def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α): + IO (α × Lean.Core.State) := coreM.toIO context state -@[export pantograph_env_catalog] +@[export pantograph_env_catalog_m] def envCatalog: Lean.CoreM Protocol.EnvCatalogResult := Environment.catalog ({}: Protocol.EnvCatalog) -@[export pantograph_env_inspect] -def envInspect (cc: Lean.Core.Context) (cs: Lean.Core.State) - (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options): IO (Protocol.CR Protocol.EnvInspectResult) := do - let coreM: Lean.CoreM _ := Environment.inspect ({ +@[export pantograph_env_inspect_m] +def envInspect (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options): + Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) := + Environment.inspect ({ name, value? := .some value, dependency?:= .some dependency }: Protocol.EnvInspect) options - let (result, _) ← coreM.toIO cc cs - return result -@[export pantograph_env_add] -def envAdd (cc: Lean.Core.Context) (cs: Lean.Core.State) - (name: String) (type: String) (value: String) (isTheorem: Bool): IO (Protocol.CR Protocol.EnvAddResult) := do - let coreM: Lean.CoreM _ := Environment.addDecl { name, type, value, isTheorem } - let (result, _) ← coreM.toIO cc cs - return result +@[export pantograph_env_add_m] +def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool): + Lean.CoreM (Protocol.CR Protocol.EnvAddResult) := + Environment.addDecl { name, type, value, isTheorem } -@[export pantograph_expr_parse] +@[export pantograph_expr_parse_m] def exprParse (s: String): Lean.CoreM (Protocol.CR Lean.Expr) := do let env ← Lean.MonadEnv.getEnv let syn ← match syntax_from_str env s with @@ -116,8 +109,9 @@ def exprParse (s: String): Lean.CoreM (Protocol.CR Lean.Expr) := do | .error str => return .error $ errorI "elab" str | .ok expr => return .ok expr) -@[export pantograph_expr_print] -def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do +@[export pantograph_expr_print_m] +def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): + Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do let termElabM: Lean.Elab.TermElabM _ := try let type ← Lean.Meta.inferType expr @@ -129,8 +123,30 @@ def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): Lean.CoreM (Proto return .error $ errorI "typing" (← exception.toMessageData.toString) runTermElabM termElabM -@[export pantograph_goal_start] +@[export pantograph_goal_start_m] def goalStart (expr: Lean.Expr): Lean.CoreM GoalState := runTermElabM (GoalState.create expr) +@[export pantograph_goal_tactic_m] +def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := + runTermElabM <| GoalState.execute state goalId tactic + +@[export pantograph_goal_try_assign_m] +def goalTryAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult := + runTermElabM <| GoalState.tryAssign state goalId expr + +@[export pantograph_goal_continue] +def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState := + target.continue branch + +@[export pantograph_goal_resume] +def goalResume (target: GoalState) (goals: Array String): Except String GoalState := + target.resume (goals.map (λ n => { name := n.toName }) |>.toList) + +@[export pantograph_goal_serialize_m] +def goalSerialize (state: GoalState) (options: Protocol.Options): Lean.CoreM (Array Protocol.Goal) := + runMetaM <| state.serializeGoals (parent := .none) options + + + end Pantograph diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 5015ad1..91c44a8 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -221,7 +221,7 @@ structure GoalContinue where -- The state which is an ancestor of `target` where goals will be extracted from branch?: Option Nat := .none -- Or, the particular goals that should be brought back into scope - goals?: Option (List String) := .none + goals?: Option (Array String) := .none deriving Lean.FromJson structure GoalContinueResult where nextStateId: Nat diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index 7bf12f9..e412ced 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,5 +1,6 @@ namespace Pantograph +@[export pantograph_version] def version := "0.2.12-alpha" end Pantograph From 5db727e30bc9d515ccfbb867c126c4c828bcbaea Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 10 Mar 2024 15:09:38 -0700 Subject: [PATCH 12/30] fix: Execute expr parsing within goal.start --- Pantograph.lean | 13 ++++++++----- Pantograph/Library.lean | 6 ------ 2 files changed, 8 insertions(+), 11 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index cc2471f..0168894 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -95,11 +95,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do let state ← get let env ← Lean.MonadEnv.getEnv - let expr?: Except Protocol.InteractionError GoalState ← runTermElabM (match args.expr, args.copyFrom with - | .some expr, .none => do - match ← exprParse expr with - | .ok expr => return .ok (← GoalState.create expr) - | .error e => return .error e + let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with + | .some expr, .none => + (match syntax_from_str env expr with + | .error str => return .error <| errorI "parsing" str + | .ok syn => do + (match ← syntax_to_expr syn with + | .error str => return .error <| errorI "elab" str + | .ok expr => return .ok (← GoalState.create expr))) | .none, .some copyFrom => (match env.find? <| copyFrom.toName with | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index b1a6864..f1115e1 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -76,12 +76,6 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do (trustLevel := 1) return { env := env } -/-- Execute a `CoreM` monad -/ -@[export pantograph_exec_core] -def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α): - IO (α × Lean.Core.State) := - coreM.toIO context state - @[export pantograph_env_catalog_m] def envCatalog: Lean.CoreM Protocol.EnvCatalogResult := Environment.catalog ({}: Protocol.EnvCatalog) From 285cf0416aa687cfd9d9b7cb1a2224f6eeef395d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 10 Mar 2024 15:33:32 -0700 Subject: [PATCH 13/30] feat(lib): Option creation function --- Pantograph.lean | 17 ++++------- Pantograph/Library.lean | 64 ++++++++++++++++++++++++++++------------- 2 files changed, 50 insertions(+), 31 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 0168894..fceac00 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -71,10 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Environment.addDecl args expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do let state ← get - let expr ← match ← exprParse args.expr with - | .ok expr => pure $ expr - | .error e => return .error e - exprPrint expr state.options + exprEcho args.expr state.options options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do let state ← get let options := state.options @@ -96,13 +93,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let state ← get let env ← Lean.MonadEnv.getEnv let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with - | .some expr, .none => - (match syntax_from_str env expr with - | .error str => return .error <| errorI "parsing" str - | .ok syn => do - (match ← syntax_to_expr syn with - | .error str => return .error <| errorI "elab" str - | .ok expr => return .ok (← GoalState.create expr))) + | .some expr, .none => do + let expr ← match ← exprParse expr with + | .error e => return .error e + | .ok expr => pure $ expr + return .ok $ ← GoalState.create expr | .none, .some copyFrom => (match env.find? <| copyFrom.toName with | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index f1115e1..b731fb3 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -80,6 +80,23 @@ 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) := @@ -92,34 +109,41 @@ def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool): Lean.CoreM (Protocol.CR Protocol.EnvAddResult) := Environment.addDecl { name, type, value, isTheorem } -@[export pantograph_expr_parse_m] -def exprParse (s: String): Lean.CoreM (Protocol.CR Lean.Expr) := do +/-- This must be a TermElabM since the parsed expr contains extra information -/ +def exprParse (s: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do let env ← Lean.MonadEnv.getEnv let syn ← match syntax_from_str env s with | .error str => return .error $ errorI "parsing" str | .ok syn => pure syn - runTermElabM (do - match ← syntax_to_expr syn with - | .error str => return .error $ errorI "elab" str - | .ok expr => return .ok expr) + match ← syntax_to_expr syn with + | .error str => return .error $ errorI "elab" str + | .ok expr => return .ok expr -@[export pantograph_expr_print_m] -def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): +@[export pantograph_expr_echo_m] +def exprEcho (expr: String) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do - let termElabM: Lean.Elab.TermElabM _ := - try - let type ← Lean.Meta.inferType expr - return .ok { - type := (← serialize_expression options type), - expr := (← serialize_expression options expr) - } - catch exception => - return .error $ errorI "typing" (← exception.toMessageData.toString) + let termElabM: Lean.Elab.TermElabM _ := do + let expr ← match ← exprParse expr with + | .error e => return .error e + | .ok expr => pure expr + try + let type ← Lean.Meta.inferType expr + return .ok { + type := (← serialize_expression options type), + expr := (← serialize_expression options expr) + } + catch exception => + return .error $ errorI "typing" (← exception.toMessageData.toString) runTermElabM termElabM -@[export pantograph_goal_start_m] -def goalStart (expr: Lean.Expr): Lean.CoreM GoalState := - runTermElabM (GoalState.create expr) +@[export pantograph_goal_start_expr_m] +def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) := + let termElabM: Lean.Elab.TermElabM _ := do + let expr ← match ← exprParse expr with + | .error e => return .error e + | .ok expr => pure $ expr + return .ok $ ← GoalState.create expr + runTermElabM termElabM @[export pantograph_goal_tactic_m] def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := From c83af044b4627eda5a12135b1ba197bea5ff3da2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 11 Mar 2024 21:31:59 -0700 Subject: [PATCH 14/30] fix: Pass options by reference --- Pantograph/Environment.lean | 2 +- Pantograph/Library.lean | 4 ++-- Pantograph/Serial.lean | 8 ++++++-- 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index df0bc7f..f37225f 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -37,7 +37,7 @@ def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do | .some x => acc.push x | .none => acc) return { symbols := names } -def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do +def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do let env ← Lean.MonadEnv.getEnv let name := args.name.toName let info? := env.find? name diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index b731fb3..d72fd3a 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -98,7 +98,7 @@ def mkOptions } @[export pantograph_env_inspect_m] -def envInspect (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options): +def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) := Environment.inspect ({ name, value? := .some value, dependency?:= .some dependency @@ -162,7 +162,7 @@ def goalResume (target: GoalState) (goals: Array String): Except String GoalStat target.resume (goals.map (λ n => { name := n.toName }) |>.toList) @[export pantograph_goal_serialize_m] -def goalSerialize (state: GoalState) (options: Protocol.Options): Lean.CoreM (Array Protocol.Goal) := +def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) := runMetaM <| state.serializeGoals (parent := .none) options diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 547b3dc..213ae6d 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -172,7 +172,7 @@ def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol } /-- Adapted from ppGoal -/ -def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) +def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) : MetaM Protocol.Goal := do -- Options for printing; See Meta.ppGoal for details let showLetValues := true @@ -242,7 +242,11 @@ def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: Metavar where of_name (n: Name) := name_to_ast n (sanitize := false) -protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do +protected def GoalState.serializeGoals + (state: GoalState) + (parent: Option GoalState := .none) + (options: @&Protocol.Options := {}): + MetaM (Array Protocol.Goal):= do state.restoreMetaM let goals := state.goals.toArray let parentDecl? := parent.bind (λ parentState => From b64adf31cfa319bd220fb821ee6521c56d00b171 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 14 Mar 2024 16:34:01 -0700 Subject: [PATCH 15/30] feat(lib): Export goal.print function --- Pantograph.lean | 8 +------- Pantograph/Library.lean | 9 +++++++++ 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index fceac00..bcf8395 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -179,12 +179,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match state.goalStates.find? args.stateId with | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" | .some goalState => runMetaM <| do - goalState.restoreMetaM - let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr) - let parent? ← goalState.parentExpr?.mapM (λ expr => serialize_expression state.options expr) - return .ok { - root?, - parent?, - } + return .ok (← goalPrint goalState state.options) end Pantograph diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index d72fd3a..52a88b6 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -165,6 +165,15 @@ def goalResume (target: GoalState) (goals: Array String): Except String GoalStat def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) := runMetaM <| state.serializeGoals (parent := .none) options +@[export pantograph_goal_print_m] +def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do + let metaM := do + state.restoreMetaM + return { + root? := ← state.rootExpr?.mapM (λ expr => serialize_expression options expr), + parent? := ← state.parentExpr?.mapM (λ expr => serialize_expression options expr), + } + runMetaM metaM end Pantograph From 689112d973404ce6da01aae6bd476e0fb7892343 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 14 Mar 2024 22:40:14 -0700 Subject: [PATCH 16/30] fix: Use Arrays only in the ABI --- Pantograph/Environment.lean | 6 +++--- Pantograph/Protocol.lean | 7 ++++--- Test/Environment.lean | 8 ++++---- 3 files changed, 11 insertions(+), 10 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index f37225f..ecae517 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -66,8 +66,8 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr | .inductInfo induct => { core with inductInfo? := .some { numParams := induct.numParams, numIndices := induct.numIndices, - all := induct.all.map (·.toString), - ctors := induct.ctors.map (·.toString), + all := induct.all.toArray.map (·.toString), + ctors := induct.ctors.toArray.map (·.toString), isRec := induct.isRec, isReflexive := induct.isReflexive, isNested := induct.isNested, @@ -79,7 +79,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr numFields := ctor.numFields, } } | .recInfo r => { core with recursorInfo? := .some { - all := r.all.map (·.toString), + all := r.all.toArray.map (·.toString), numParams := r.numParams, numIndices := r.numIndices, numMotives := r.numMotives, diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 91c44a8..e9a5f87 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -124,8 +124,8 @@ structure EnvInspect where structure InductInfo where numParams: Nat numIndices: Nat - all: List String - ctors: List String + all: Array String + ctors: Array String isRec: Bool := false isReflexive: Bool := false isNested: Bool := false @@ -138,7 +138,7 @@ structure ConstructorInfo where numFields: Nat deriving Lean.ToJson structure RecursorInfo where - all: List String + all: Array String numParams: Nat numIndices: Nat numMotives: Nat @@ -230,6 +230,7 @@ structure GoalContinueResult where -- Remove goal states structure GoalDelete where + -- This is ok being a List because it doesn't show up in the ABI stateIds: List Nat deriving Lean.FromJson structure GoalDeleteResult where diff --git a/Test/Environment.lean b/Test/Environment.lean index df3f3ae..977ed7d 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -34,8 +34,8 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do ("Or", ConstantCat.induct { numParams := 2, numIndices := 0, - all := ["Or"], - ctors := ["Or.inl", "Or.inr"], + all := #["Or"], + ctors := #["Or.inl", "Or.inr"], }), ("Except.ok", ConstantCat.ctor { induct := "Except", @@ -44,7 +44,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do numFields := 1, }), ("Eq.rec", ConstantCat.recursor { - all := ["Eq"], + all := #["Eq"], numParams := 2, numIndices := 1, numMotives := 1, @@ -52,7 +52,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do k := true, }), ("ForM.rec", ConstantCat.recursor { - all := ["ForM"], + all := #["ForM"], numParams := 3, numIndices := 0, numMotives := 1, From b7542b4749015d8ee6f43f656256d955e00bf94b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 15 Mar 2024 06:01:25 -0700 Subject: [PATCH 17/30] chore: Lean version bump to 4.7.0-rc2 Multithreading in ABI was not stabilized in 4.1.0 --- Makefile | 8 ++++---- flake.lock | 8 ++++---- flake.nix | 2 +- lake-manifest.json | 24 +++++++++++++----------- lakefile.lean | 2 +- lean-toolchain | 2 +- 6 files changed, 24 insertions(+), 22 deletions(-) diff --git a/Makefile b/Makefile index 39350b6..5d4ad6b 100644 --- a/Makefile +++ b/Makefile @@ -1,8 +1,8 @@ -LIB := build/lib/Pantograph.olean -EXE := build/bin/pantograph +LIB := ./.lake/build/lib/Pantograph.olean +EXE := ./.lake/build/bin/pantograph SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain -TEST_EXE := build/bin/test +TEST_EXE := ./.lake/build/bin/test TEST_SOURCE := $(wildcard Test/*.lean) $(LIB) $(EXE): $(SOURCE) @@ -12,7 +12,7 @@ $(TEST_EXE): $(LIB) $(TEST_SOURCE) lake build test test: $(TEST_EXE) - lake env $(TEST_EXE) + $(TEST_EXE) clean: lake clean diff --git a/flake.lock b/flake.lock index 67246b6..89f0e9d 100644 --- a/flake.lock +++ b/flake.lock @@ -41,16 +41,16 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1695693562, - "narHash": "sha256-6qbCafG0bL5KxQt2gL6hV4PFDsEMM0UXfldeOOqxsaE=", + "lastModified": 1709691092, + "narHash": "sha256-jHY8BhDotfGcMS0Xzl5iawqCaug3dDEKuD5Y1WcM06I=", "owner": "leanprover", "repo": "lean4", - "rev": "a832f398b80a5ebb820d27b9e55ec949759043ff", + "rev": "6fce8f7d5cd18a4419bca7fd51780c71c9b1cc5a", "type": "github" }, "original": { "owner": "leanprover", - "ref": "v4.1.0", + "ref": "v4.7.0-rc2", "repo": "lean4", "type": "github" } diff --git a/flake.nix b/flake.nix index 9f586f6..54640d3 100644 --- a/flake.nix +++ b/flake.nix @@ -4,7 +4,7 @@ inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-parts.url = "github:hercules-ci/flake-parts"; - lean.url = "github:leanprover/lean4?ref=v4.1.0"; + lean.url = "github:leanprover/lean4?ref=v4.7.0-rc2"; }; outputs = inputs @ { diff --git a/lake-manifest.json b/lake-manifest.json index 6c2efa0..6ebbbe5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,12 +1,14 @@ -{"version": 6, - "packagesDir": "lake-packages", +{"version": 7, + "packagesDir": ".lake/packages", "packages": - [{"git": - {"url": "https://github.com/lurk-lab/LSpec.git", - "subDir?": null, - "rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41", - "opts": {}, - "name": "LSpec", - "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41", - "inherited": false}}], - "name": "pantograph"} + [{"url": "https://github.com/lurk-lab/LSpec.git", + "type": "git", + "subDir": null, + "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114", + "name": "LSpec", + "manifestFile": "lake-manifest.json", + "inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114", + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "pantograph", + "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 89ad70f..d7bc630 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -15,7 +15,7 @@ lean_exe pantograph { } require LSpec from git - "https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41" + "https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114" lean_lib Test { } lean_exe test { diff --git a/lean-toolchain b/lean-toolchain index a9bddf0..faa2254 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.1.0 +leanprover/lean4:4.7.0-rc2 From bb09d1e96457ae9f2ba3bfed5aaee6fb23661d41 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 15 Mar 2024 18:44:28 -0700 Subject: [PATCH 18/30] chore: Version bump to 4.8.0 prerelease --- flake.lock | 8 ++++---- flake.nix | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/flake.lock b/flake.lock index 89f0e9d..6278d68 100644 --- a/flake.lock +++ b/flake.lock @@ -41,16 +41,16 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1709691092, - "narHash": "sha256-jHY8BhDotfGcMS0Xzl5iawqCaug3dDEKuD5Y1WcM06I=", + "lastModified": 1710520221, + "narHash": "sha256-8Fm4bj9sqqsUHFZweSdGMM5GdUX3jkGK/ggGq27CeQc=", "owner": "leanprover", "repo": "lean4", - "rev": "6fce8f7d5cd18a4419bca7fd51780c71c9b1cc5a", + "rev": "f70895ede54501adf0db77474f452a7fef40d0b3", "type": "github" }, "original": { "owner": "leanprover", - "ref": "v4.7.0-rc2", + "ref": "f70895ede54501adf0db77474f452a7fef40d0b3", "repo": "lean4", "type": "github" } diff --git a/flake.nix b/flake.nix index 54640d3..dd98225 100644 --- a/flake.nix +++ b/flake.nix @@ -4,7 +4,7 @@ inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-parts.url = "github:hercules-ci/flake-parts"; - lean.url = "github:leanprover/lean4?ref=v4.7.0-rc2"; + lean.url = "github:leanprover/lean4?ref=f70895ede54501adf0db77474f452a7fef40d0b3"; }; outputs = inputs @ { From a3a244159bebd19677a18e0d6704a5ae18d631d6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 16 Mar 2024 19:00:28 -0700 Subject: [PATCH 19/30] chore: Version bump to 0.2.13 --- Pantograph/Version.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index e412ced..e23d886 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,6 +1,6 @@ namespace Pantograph @[export pantograph_version] -def version := "0.2.12-alpha" +def version := "0.2.13" end Pantograph From 60903bf31f995a1a88b74635888e936546f5dcc6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 00:06:35 -0700 Subject: [PATCH 20/30] feat: Bump toolchain version --- Pantograph/Library.lean | 2 +- Test/Common.lean | 15 ++++++++------- Test/Environment.lean | 3 ++- Test/Holes.lean | 16 ++++------------ Test/Integration.lean | 12 +++--------- Test/Proofs.lean | 20 ++++++-------------- Test/Serial.lean | 7 ++----- flake.lock | 28 +++++++++++++++++++++++----- flake.nix | 10 +++++++++- lean-toolchain | 2 +- 10 files changed, 59 insertions(+), 56 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 52a88b6..078ca0f 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -63,7 +63,7 @@ def createCoreContext (options: Array String): IO Lean.Core.Context := do currNamespace := Lean.Name.str .anonymous "Aniva" openDecls := [], -- No 'open' directives needed fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] }, + fileMap := { source := "", positions := #[0] }, options := options } diff --git a/Test/Common.lean b/Test/Common.lean index 2257c7c..7c5b6e5 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -1,5 +1,6 @@ -import Pantograph.Protocol import Pantograph.Goal +import Pantograph.Library +import Pantograph.Protocol import LSpec namespace Pantograph @@ -35,12 +36,7 @@ def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message fa open Lean def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq): IO LSpec.TestSeq := do - let coreContext: Core.Context := { - currNamespace := Name.str .anonymous "Aniva" - openDecls := [], -- No 'open' directives needed - fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] } - } + let coreContext: Core.Context ← createCoreContext #[] match ← (coreM.run' coreContext { env := env }).toBaseIO with | .error exception => return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "") @@ -53,4 +49,9 @@ def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α errToSorry := false, }) +def defaultTermElabMContext: Lean.Elab.Term.Context := { + declName? := some "_pantograph".toName, + errToSorry := false + } + end Pantograph diff --git a/Test/Environment.lean b/Test/Environment.lean index 977ed7d..9e3bd70 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -76,7 +76,8 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do def suite: IO LSpec.TestSeq := do let env: Environment ← importModules - (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false })) + (imports := #[`Init]) + --(imports := #["Prelude"].map (λ str => { module := str.toName, runtimeOnly := false })) (opts := {}) (trustLevel := 1) diff --git a/Test/Holes.lean b/Test/Holes.lean index afad4e8..af322e9 100644 --- a/Test/Holes.lean +++ b/Test/Holes.lean @@ -44,16 +44,8 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options - let coreContext: Lean.Core.Context := { - currNamespace := Name.append .anonymous "Aniva", - openDecls := [], -- No 'open' directives needed - fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] } - } - let metaM := termElabM.run' (ctx := { - declName? := some "_pantograph", - errToSorry := false - }) + let coreContext: Lean.Core.Context ← createCoreContext #[] + let metaM := termElabM.run' (ctx := defaultTermElabMContext) let coreM := metaM.run' match ← (coreM.run' coreContext { env := env }).toBaseIO with | .error exception => @@ -169,7 +161,7 @@ def test_partial_continuation: TestM Unit := do return () | .ok state => pure state addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = - #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]) + #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"]) addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone -- Roundtrip @@ -183,7 +175,7 @@ def test_partial_continuation: TestM Unit := do return () | .ok state => pure state addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = - #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]) + #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"]) addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone -- Continuation should fail if the state does not exist: diff --git a/Test/Integration.lean b/Test/Integration.lean index 0a6c210..83b3c9d 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -21,13 +21,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d let context: Context := { imports := ["Init"] } - let coreContext: Lean.Core.Context := { - currNamespace := Lean.Name.str .anonymous "Aniva" - openDecls := [], - fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] }, - options := Lean.Options.empty - } + let coreContext: Lean.Core.Context ← createCoreContext #[] let commands: MainM LSpec.TestSeq := steps.foldlM (λ suite step => do let result ← step @@ -39,7 +33,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d return LSpec.check s!"Uncaught IO exception: {ex.toString}" false def test_option_modify : IO LSpec.TestSeq := - let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n" + let pp? := Option.some "∀ (n : Nat), n + 1 = n.succ" let sexp? := Option.some "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))" let module? := Option.some "Init.Data.Nat.Basic" let options: Protocol.Options := {} @@ -142,7 +136,7 @@ def test_env : IO LSpec.TestSeq := subroutine_step "env.inspect" [("name", .str name2)] (Lean.toJson ({ - value? := .some { pp? := .some "fun a => Int.ofNat a + 1" }, + value? := .some { pp? := .some "fun a => ↑a + 1" }, type := { pp? := .some "Nat → Int" }, }: Protocol.EnvInspectResult)) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 85ba66d..833c02e 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -62,16 +62,8 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options - let coreContext: Lean.Core.Context := { - currNamespace := Name.append .anonymous "Aniva", - openDecls := [], -- No 'open' directives needed - fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] } - } - let metaM := termElabM.run' (ctx := { - declName? := some "_pantograph", - errToSorry := false - }) + let coreContext: Lean.Core.Context ← createCoreContext #[] + let metaM := termElabM.run' (ctx := defaultTermElabMContext) let coreM := metaM.run' match ← (coreM.run' coreContext { env := env }).toBaseIO with | .error exception => @@ -235,7 +227,7 @@ def proof_or_comm: TestM Unit := do let state2parent ← serialize_expression_ast state2.parentExpr?.get! (sanitize := false) -- This is due to delayed assignment addTest $ LSpec.test "(2 parent)" (state2parent == - "((:mv _uniq.45) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") + "((:mv _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state @@ -243,7 +235,7 @@ def proof_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () let state3_1parent ← serialize_expression_ast state3_1.parentExpr?.get! (sanitize := false) - addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.83))") + addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))") addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with | .success state => pure state @@ -252,7 +244,7 @@ def proof_or_comm: TestM Unit := do return () addTest $ LSpec.check " assumption" state4_1.goals.isEmpty let state4_1parent ← serialize_expression_ast state4_1.parentExpr?.get! (sanitize := false) - addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.49)") + addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)") addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with | .success state => pure state @@ -304,7 +296,7 @@ def proof_or_comm: TestM Unit := do def suite: IO LSpec.TestSeq := do let env: Lean.Environment ← Lean.importModules - (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}]) + (imports := #[{ module := "Init".toName, runtimeOnly := false}]) (opts := {}) (trustLevel := 1) let tests := [ diff --git a/Test/Serial.lean b/Test/Serial.lean index 70e86e8..490b538 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -20,7 +20,7 @@ def test_name_to_ast: LSpec.TestSeq := def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do let entries: List (Name × Protocol.BoundExpression) := [ ("Nat.add_comm".toName, { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }), - ("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" }) + ("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "n.succ ≤ m")], target := "n ≤ m" }) ] let coreM: CoreM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do let env ← MonadEnv.getEnv @@ -58,10 +58,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do let expr := (← syntax_to_expr s) |>.toOption |>.get! let test := LSpec.check source ((← serialize_expression_ast expr) = target) return LSpec.TestSeq.append suites test) LSpec.TestSeq.done - let metaM := termElabM.run' (ctx := { - declName? := some "_pantograph", - errToSorry := false - }) + let metaM := termElabM.run' (ctx := defaultTermElabMContext) runMetaMSeq env metaM -- Instance parsing diff --git a/flake.lock b/flake.lock index 6278d68..1878e87 100644 --- a/flake.lock +++ b/flake.lock @@ -38,19 +38,20 @@ "flake-utils": "flake-utils", "lean4-mode": "lean4-mode", "nix": "nix", - "nixpkgs": "nixpkgs_2" + "nixpkgs": "nixpkgs_2", + "nixpkgs-old": "nixpkgs-old" }, "locked": { - "lastModified": 1710520221, - "narHash": "sha256-8Fm4bj9sqqsUHFZweSdGMM5GdUX3jkGK/ggGq27CeQc=", + "lastModified": 1711508550, + "narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=", "owner": "leanprover", "repo": "lean4", - "rev": "f70895ede54501adf0db77474f452a7fef40d0b3", + "rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2", "type": "github" }, "original": { "owner": "leanprover", - "ref": "f70895ede54501adf0db77474f452a7fef40d0b3", + "ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2", "repo": "lean4", "type": "github" } @@ -141,6 +142,23 @@ "type": "github" } }, + "nixpkgs-old": { + "flake": false, + "locked": { + "lastModified": 1581379743, + "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-19.03", + "repo": "nixpkgs", + "type": "github" + } + }, "nixpkgs-regression": { "locked": { "lastModified": 1643052045, diff --git a/flake.nix b/flake.nix index dd98225..ed89fb0 100644 --- a/flake.nix +++ b/flake.nix @@ -4,7 +4,7 @@ inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-parts.url = "github:hercules-ci/flake-parts"; - lean.url = "github:leanprover/lean4?ref=f70895ede54501adf0db77474f452a7fef40d0b3"; + lean.url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2"; }; outputs = inputs @ { @@ -27,12 +27,20 @@ roots = [ "Main" "Pantograph" ]; src = ./.; }; + test = leanPkgs.buildLeanPackage { + name = "Test"; + roots = [ "Main" ]; + src = ./Test; + }; in rec { packages = { inherit (leanPkgs) lean lean-all; inherit (project) sharedLib executable; default = project.executable; }; + checks = { + test = test.executable; + }; devShells.default = project.devShell; }; }; diff --git a/lean-toolchain b/lean-toolchain index faa2254..c630636 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.7.0-rc2 +leanprover/lean4:nightly-2024-03-27 From 22fdb7bea91021478fa0e98057f585fc0c25ddb7 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 11:33:15 -0700 Subject: [PATCH 21/30] build: Nix build targets and checks --- flake.lock | 40 ++++++++++++++++++++++------------------ flake.nix | 36 ++++++++++++++++++++++++++++++++---- 2 files changed, 54 insertions(+), 22 deletions(-) diff --git a/flake.lock b/flake.lock index 1878e87..f7f3012 100644 --- a/flake.lock +++ b/flake.lock @@ -38,7 +38,9 @@ "flake-utils": "flake-utils", "lean4-mode": "lean4-mode", "nix": "nix", - "nixpkgs": "nixpkgs_2", + "nixpkgs": [ + "nixpkgs" + ], "nixpkgs-old": "nixpkgs-old" }, "locked": { @@ -88,6 +90,23 @@ "type": "github" } }, + "lspec": { + "flake": false, + "locked": { + "lastModified": 1701971219, + "narHash": "sha256-HYDRzkT2UaLDrqKNWesh9C4LJNt0JpW0u68wYVj4Byw=", + "owner": "lurk-lab", + "repo": "LSpec", + "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114", + "type": "github" + }, + "original": { + "owner": "lurk-lab", + "ref": "3388be5a1d1390594a74ec469fd54a5d84ff6114", + "repo": "LSpec", + "type": "github" + } + }, "nix": { "inputs": { "lowdown-src": "lowdown-src", @@ -176,22 +195,6 @@ } }, "nixpkgs_2": { - "locked": { - "lastModified": 1686089707, - "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397", - "type": "github" - }, - "original": { - "owner": "NixOS", - "ref": "nixpkgs-unstable", - "repo": "nixpkgs", - "type": "github" - } - }, - "nixpkgs_3": { "locked": { "lastModified": 1697456312, "narHash": "sha256-roiSnrqb5r+ehnKCauPLugoU8S36KgmWraHgRqVYndo=", @@ -211,7 +214,8 @@ "inputs": { "flake-parts": "flake-parts", "lean": "lean", - "nixpkgs": "nixpkgs_3" + "lspec": "lspec", + "nixpkgs": "nixpkgs_2" } } }, diff --git a/flake.nix b/flake.nix index ed89fb0..539d391 100644 --- a/flake.nix +++ b/flake.nix @@ -4,7 +4,14 @@ inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-parts.url = "github:hercules-ci/flake-parts"; - lean.url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2"; + lean = { + url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2"; + inputs.nixpkgs.follows = "nixpkgs"; + }; + lspec = { + url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114"; + flake = false; + }; }; outputs = inputs @ { @@ -12,6 +19,7 @@ nixpkgs, flake-parts, lean, + lspec, ... } : flake-parts.lib.mkFlake { inherit inputs; } { flake = { @@ -22,24 +30,44 @@ ]; perSystem = { system, pkgs, ... }: let leanPkgs = lean.packages.${system}; + lspecLib = leanPkgs.buildLeanPackage { + name = "LSpec"; + roots = [ "Main" "LSpec" ]; + src = "${lspec}"; + }; project = leanPkgs.buildLeanPackage { name = "Pantograph"; + #roots = pkgs.lib.optional pkgs.stdenv.isDarwin [ "Main" "Pantograph" ]; roots = [ "Main" "Pantograph" ]; src = ./.; }; test = leanPkgs.buildLeanPackage { name = "Test"; - roots = [ "Main" ]; - src = ./Test; + # NOTE: The src directory must be ./. since that is where the import + # root begins (e.g. `import Test.Environment` and not `import + # Environment`) and thats where `lakefile.lean` resides. + roots = [ "Test.Main" ]; + deps = [ lspecLib project ]; + src = pkgs.lib.cleanSourceWith { + src = ./.; + filter = path: type: + !(pkgs.lib.hasInfix "Pantograph" path); + }; }; in rec { packages = { inherit (leanPkgs) lean lean-all; inherit (project) sharedLib executable; + test = test.executable; default = project.executable; }; checks = { - test = test.executable; + test = pkgs.runCommand "test" { + buildInputs = [ test.executable leanPkgs.lean-all ]; + } '' + #export LEAN_SRC_PATH="${./.}" + ${test.executable}/bin/test > $out + ''; }; devShells.default = project.devShell; }; From 91e55245fae149b2e455dff84c3de976e2326f82 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 11:37:07 -0700 Subject: [PATCH 22/30] doc: Update README.md --- README.md | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 1ca4d7b..c845b89 100644 --- a/README.md +++ b/README.md @@ -6,6 +6,8 @@ An interaction system for Lean 4. ## Installation +For Nix based workflow, see below. + Install `elan` and `lake`. Execute ``` sh make build/bin/pantograph @@ -20,7 +22,7 @@ LEAN_PATH=$LEAN_PATH build/bin/pantograph $@ ``` The provided `flake.nix` has a develop environment with Lean already setup. -## Usage +## Executable Usage ``` sh pantograph MODULES|LEAN_OPTIONS @@ -63,7 +65,7 @@ stat ``` where the application of `assumption` should lead to a failure. -## Commands +### Commands See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. - `reset`: Delete all cached expressions and proof trees @@ -82,7 +84,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va - `goal.print {"stateId": }"`: Print a goal state - `stat`: Display resource usage -## Errors +### Errors When an error pertaining to the execution of a command happens, the returning JSON structure is @@ -97,16 +99,31 @@ Common error forms: input of another is broken. For example, attempting to query a symbol not existing in the library or indexing into a non-existent proof state. -## Troubleshooting +### Troubleshooting If lean encounters stack overflow problems when printing catalog, execute this before running lean: ```sh ulimit -s unlimited ``` +## Library Usage + +`Pantograph/Library.lean` exposes a series of interfaces which allow FFI call +with `Pantograph`. + ## Testing The tests are based on `LSpec`. To run tests, ``` sh make test ``` + +## Nix based workflow + +To run tests: +``` sh +nix build .#checks.${system}.test +``` + +For example, `${system}` could be `x86_64-linux`. Using `nix develop` drops the +current session into a development shell with fixed Lean version. From 01a23b338a66d255126cd3cfb85f429b136b7648 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 18:56:42 -0700 Subject: [PATCH 23/30] feat: Unfold aux lemmas when printing root expr --- Pantograph/Library.lean | 12 ++++++++++-- Test/Common.lean | 3 +++ Test/Environment.lean | 3 ++- Test/Main.lean | 4 ++-- Test/{Holes.lean => Metavar.lean} | 6 +++--- Test/Serial.lean | 3 ++- 6 files changed, 22 insertions(+), 9 deletions(-) rename Test/{Holes.lean => Metavar.lean} (98%) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 078ca0f..c40322a 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -165,13 +165,21 @@ def goalResume (target: GoalState) (goals: Array String): Except String GoalStat def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) := runMetaM <| state.serializeGoals (parent := .none) options +def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _ + +/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/ +def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do + Lean.Meta.deltaExpand e Lean.Name.isAuxLemma + @[export pantograph_goal_print_m] def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do let metaM := do state.restoreMetaM return { - root? := ← state.rootExpr?.mapM (λ expr => serialize_expression options expr), - parent? := ← state.parentExpr?.mapM (λ expr => serialize_expression options expr), + root? := ← state.rootExpr?.mapM (λ expr => do + serialize_expression options (← unfoldAuxLemmas expr)), + parent? := ← state.parentExpr?.mapM (λ expr => do + serialize_expression options (← unfoldAuxLemmas expr)), } runMetaM metaM diff --git a/Test/Common.lean b/Test/Common.lean index 7c5b6e5..2e7149d 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -1,8 +1,11 @@ import Pantograph.Goal import Pantograph.Library import Pantograph.Protocol +import Lean import LSpec +open Lean + namespace Pantograph namespace Protocol diff --git a/Test/Environment.lean b/Test/Environment.lean index 9e3bd70..ba99380 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -2,11 +2,12 @@ import LSpec import Pantograph.Serial import Pantograph.Environment import Test.Common +import Lean +open Lean namespace Pantograph.Test.Environment open Pantograph -open Lean deriving instance DecidableEq, Repr for Protocol.InductInfo deriving instance DecidableEq, Repr for Protocol.ConstructorInfo diff --git a/Test/Main.lean b/Test/Main.lean index 4a8ab1f..d24f45f 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,6 +1,6 @@ import LSpec import Test.Environment -import Test.Holes +import Test.Metavar import Test.Integration import Test.Proofs import Test.Serial @@ -11,7 +11,7 @@ def main := do Lean.initSearchPath (← Lean.findSysroot) let suites := [ - Holes.suite, + Metavar.suite, Integration.suite, Proofs.suite, Serial.suite, diff --git a/Test/Holes.lean b/Test/Metavar.lean similarity index 98% rename from Test/Holes.lean rename to Test/Metavar.lean index af322e9..cbbfc81 100644 --- a/Test/Holes.lean +++ b/Test/Metavar.lean @@ -3,7 +3,7 @@ import Pantograph.Goal import Pantograph.Serial import Test.Common -namespace Pantograph.Test.Holes +namespace Pantograph.Test.Metavar open Pantograph open Lean @@ -204,6 +204,6 @@ def suite: IO LSpec.TestSeq := do let tests ← proofRunner env tests return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done - return LSpec.group "Holes" tests + return LSpec.group "Metavar" tests -end Pantograph.Test.Holes +end Pantograph.Test.Metavar diff --git a/Test/Serial.lean b/Test/Serial.lean index 490b538..c2810c8 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -1,11 +1,12 @@ import LSpec import Pantograph.Serial import Test.Common +import Lean +open Lean namespace Pantograph.Test.Serial open Pantograph -open Lean deriving instance Repr, DecidableEq for Protocol.BoundExpression From d9af064888f5068f61bc8f6b4c7864ed506e11e2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 19:27:45 -0700 Subject: [PATCH 24/30] test: Elimination of aux lemmas --- Test/Metavar.lean | 58 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) diff --git a/Test/Metavar.lean b/Test/Metavar.lean index cbbfc81..734c1d9 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -2,6 +2,7 @@ import LSpec import Pantograph.Goal import Pantograph.Serial import Test.Common +import Lean namespace Pantograph.Test.Metavar open Pantograph @@ -85,6 +86,62 @@ def test_m_couple: TestM Unit := do addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = #[.some "2 ≤ 3", .some "3 ≤ 5"]) addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone + +def test_m_couple_simp: TestM Unit := do + let state? ← startProof "(2: Nat) ≤ 5" + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) + let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 2") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone + let state1b ← match state2.continue state1 with + | .error msg => do + addTest $ assertUnreachable $ msg + return () + | .ok state => pure state + addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "2 ≤ 2", .some "2 ≤ 5"]) + addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone + let state3 ← match ← state1b.execute (goalId := 0) (tactic := "simp") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + let state4 ← match state3.continue state1b with + | .error msg => do + addTest $ assertUnreachable $ msg + return () + | .ok state => pure state + let state5 ← match ← state4.execute (goalId := 0) (tactic := "simp") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + + state5.restoreMetaM + let root ← match state5.rootExpr? with + | .some e => pure e + | .none => + addTest $ assertUnreachable "(5 root)" + return () + let rootStr: String := toString (← Lean.Meta.ppExpr root) + addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))") + let rootStr: String := toString (← Lean.Meta.ppExpr (← unfoldAuxLemmas root)) + addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))") return () def test_proposition_generation: TestM Unit := do @@ -196,6 +253,7 @@ def suite: IO LSpec.TestSeq := do (trustLevel := 1) let tests := [ ("2 < 5", test_m_couple), + ("2 < 5", test_m_couple_simp), ("Proposition Generation", test_proposition_generation), ("Partial Continuation", test_partial_continuation) ] From 35c4ea693d22ca5695fb840a7fa824cde6c7f57b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 19:49:44 -0700 Subject: [PATCH 25/30] feat: Stop cataloging internal/detail dependencies --- Pantograph/Environment.lean | 25 ++++++++++++++++--------- Pantograph/Library.lean | 6 ------ Pantograph/Serial.lean | 17 ++++++++++------- Test/Environment.lean | 11 +++++------ 4 files changed, 31 insertions(+), 28 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index ecae517..a85342a 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -7,14 +7,15 @@ open Pantograph namespace Pantograph.Environment -def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool := - isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ info.isUnsafe +def isNameInternal (n: Lean.Name): Bool := + -- Returns true if the name is an implementation detail which should not be shown to the user. + isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma where isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with | .str _ name => name == "Lean" | _ => true -def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String := +def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String := let pref := match info with | .axiomInfo _ => "a" | .defnInfo _ => "d" @@ -26,14 +27,14 @@ def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String := | .recInfo _ => "r" s!"{pref}{toString n}" -def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String := - if is_symbol_unsafe_or_internal n info +def toFilteredSymbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String := + if isNameInternal n || info.isUnsafe then Option.none - else Option.some <| to_compact_symbol_name n info + else Option.some <| toCompactSymbolName n info def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do let env ← Lean.MonadEnv.getEnv let names := env.constants.fold (init := #[]) (λ acc name info => - match to_filtered_symbol name info with + match toFilteredSymbol name info with | .some x => acc.push x | .none => acc) return { symbols := names } @@ -58,8 +59,14 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr value? := ← value?.mapM (λ v => serialize_expression options v |>.run'), publicName? := Lean.privateToUserName? name |>.map (·.toString), -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug. - typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none, - valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none, + typeDependency? := if args.dependency?.getD false + then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) + else .none, + valueDependency? := ← if args.dependency?.getD false + then info.value?.mapM (λ e => do + let e ← (unfoldAuxLemmas e).run' + pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => name_to_ast n) ) + else pure (.none), module? := module? } let result := match info with diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index c40322a..7fda4d9 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -165,12 +165,6 @@ def goalResume (target: GoalState) (goals: Array String): Except String GoalStat def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) := runMetaM <| state.serializeGoals (parent := .none) options -def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _ - -/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/ -def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do - Lean.Meta.deltaExpand e Lean.Name.isAuxLemma - @[export pantograph_goal_print_m] def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do let metaM := do diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 213ae6d..bf79314 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -6,17 +6,20 @@ import Lean import Pantograph.Protocol import Pantograph.Goal -namespace Pantograph open Lean +-- Symbol processing functions -- + +def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _ + +namespace Pantograph + +/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/ +def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do + Lean.Meta.deltaExpand e Lean.Name.isAuxLemma + --- Input Functions --- - -/-- Read a theorem from the environment -/ -def expr_from_const (env: Environment) (name: Name): Except String Lean.Expr := - match env.find? name with - | none => throw s!"Symbol not found: {name}" - | some cInfo => return cInfo.type /-- Read syntax object from string -/ def syntax_from_str (env: Environment) (s: String): Except String Syntax := Parser.runParserCategory diff --git a/Test/Environment.lean b/Test/Environment.lean index ba99380..7014584 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -14,14 +14,14 @@ deriving instance DecidableEq, Repr for Protocol.ConstructorInfo deriving instance DecidableEq, Repr for Protocol.RecursorInfo deriving instance DecidableEq, Repr for Protocol.EnvInspectResult -def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do +def test_symbol_visibility: IO LSpec.TestSeq := do let entries: List (Name × Bool) := [ ("Nat.add_comm".toName, false), - ("Lean.Name".toName, true) + ("Lean.Name".toName, true), + ("Init.Data.Nat.Basic._auxLemma.4".toName, true), ] let suite := entries.foldl (λ suites (symbol, target) => - let constant := env.constants.find! symbol - let test := LSpec.check symbol.toString ((Environment.is_symbol_unsafe_or_internal symbol constant) == target) + let test := LSpec.check symbol.toString ((Environment.isNameInternal symbol) == target) LSpec.TestSeq.append suites test) LSpec.TestSeq.done return suite @@ -78,12 +78,11 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do def suite: IO LSpec.TestSeq := do let env: Environment ← importModules (imports := #[`Init]) - --(imports := #["Prelude"].map (λ str => { module := str.toName, runtimeOnly := false })) (opts := {}) (trustLevel := 1) return LSpec.group "Environment" $ - (LSpec.group "Symbol visibility" (← test_symbol_visibility env)) ++ + (LSpec.group "Symbol visibility" (← test_symbol_visibility)) ++ (LSpec.group "Inspect" (← test_inspect env)) end Pantograph.Test.Environment From 78a3b240ba6de1826d879801ceed5a4d61df4940 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 19:56:03 -0700 Subject: [PATCH 26/30] test: Catalog has no numeric symbols --- Pantograph/Environment.lean | 2 +- Test/Environment.lean | 29 ++++++++++++++++++++++------- 2 files changed, 23 insertions(+), 8 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index a85342a..19c3249 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -9,7 +9,7 @@ namespace Pantograph.Environment def isNameInternal (n: Lean.Name): Bool := -- Returns true if the name is an implementation detail which should not be shown to the user. - isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma + isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma ∨ n.hasMacroScopes where isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with | .str _ name => name == "Lean" diff --git a/Test/Environment.lean b/Test/Environment.lean index 7014584..7a398da 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -14,6 +14,21 @@ deriving instance DecidableEq, Repr for Protocol.ConstructorInfo deriving instance DecidableEq, Repr for Protocol.RecursorInfo deriving instance DecidableEq, Repr for Protocol.EnvInspectResult +def test_catalog: IO LSpec.TestSeq := do + let env: Environment ← importModules + (imports := #[`Init]) + (opts := {}) + (trustLevel := 1) + let inner: CoreM LSpec.TestSeq := do + let catalogResult ← Environment.catalog {} + let symbolsWithNum := env.constants.fold (init := #[]) (λ acc name info => + match (Environment.toFilteredSymbol name info).isSome && (name matches .num _ _) with + | false => acc + | true => acc.push name + ) + return LSpec.check "No num symbols" (symbolsWithNum.size == 0) + runCoreMSeq env inner + def test_symbol_visibility: IO LSpec.TestSeq := do let entries: List (Name × Bool) := [ ("Nat.add_comm".toName, false), @@ -30,7 +45,11 @@ inductive ConstantCat where | ctor (info: Protocol.ConstructorInfo) | recursor (info: Protocol.RecursorInfo) -def test_inspect (env: Environment): IO LSpec.TestSeq := do +def test_inspect: IO LSpec.TestSeq := do + let env: Environment ← importModules + (imports := #[`Init]) + (opts := {}) + (trustLevel := 1) let testCases: List (String × ConstantCat) := [ ("Or", ConstantCat.induct { numParams := 2, @@ -76,13 +95,9 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do runCoreMSeq env inner def suite: IO LSpec.TestSeq := do - let env: Environment ← importModules - (imports := #[`Init]) - (opts := {}) - (trustLevel := 1) - return LSpec.group "Environment" $ + (LSpec.group "Catalog" (← test_catalog)) ++ (LSpec.group "Symbol visibility" (← test_symbol_visibility)) ++ - (LSpec.group "Inspect" (← test_inspect env)) + (LSpec.group "Inspect" (← test_inspect)) end Pantograph.Test.Environment From d853cb8cc2ad3f523d9e1de9e24ddad2ae83ba7e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 22:08:22 -0700 Subject: [PATCH 27/30] chore: Version bump --- Pantograph/Version.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index e23d886..688fc60 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,6 +1,6 @@ namespace Pantograph @[export pantograph_version] -def version := "0.2.13" +def version := "0.2.14" end Pantograph From 1d1a151a4b2ccafb4897457fb09f857ffe9a9506 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 22:09:56 -0700 Subject: [PATCH 28/30] doc: Main README.md --- README.md | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index c845b89..cde0807 100644 --- a/README.md +++ b/README.md @@ -1,9 +1,12 @@ # Pantograph -An interaction system for Lean 4. +A Machine-to-Machine interaction system for Lean 4. ![Pantograph](doc/icon.svg) +Pantograph provides interfaces to execute proofs, construct expressions, and +examine the symbol list of a Lean project for machine learning. + ## Installation For Nix based workflow, see below. @@ -109,9 +112,12 @@ ulimit -s unlimited ## Library Usage `Pantograph/Library.lean` exposes a series of interfaces which allow FFI call -with `Pantograph`. +with `Pantograph` which mirrors the REPL commands above. It is recommended to +call Pantograph via this FFI since it provides a tremendous speed up. -## Testing +## Developing + +### Testing The tests are based on `LSpec`. To run tests, ``` sh @@ -120,6 +126,10 @@ make test ## Nix based workflow +The included Nix flake provides build targets for `sharedLib` and `executable`. +The executable can be used as-is, but linking against the shared library +requires the presence of `lean-all`. + To run tests: ``` sh nix build .#checks.${system}.test From c5404b8210bb39b74030327d1c19efd3cbff9d72 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 22:23:19 -0700 Subject: [PATCH 29/30] build: Ignore test files when building target --- flake.nix | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index 539d391..df63845 100644 --- a/flake.nix +++ b/flake.nix @@ -39,7 +39,13 @@ name = "Pantograph"; #roots = pkgs.lib.optional pkgs.stdenv.isDarwin [ "Main" "Pantograph" ]; roots = [ "Main" "Pantograph" ]; - src = ./.; + src = pkgs.lib.cleanSourceWith { + src = ./.; + filter = path: type: + !(pkgs.lib.hasInfix "/Test/" path) && + !(pkgs.lib.hasSuffix ".md" path) && + !(pkgs.lib.hasSuffix "Makefile" path); + }; }; test = leanPkgs.buildLeanPackage { name = "Test"; @@ -58,7 +64,6 @@ packages = { inherit (leanPkgs) lean lean-all; inherit (project) sharedLib executable; - test = test.executable; default = project.executable; }; checks = { From bdb060b79f35663c26bbcf4ed4f3bf7d4025a201 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 22:26:46 -0700 Subject: [PATCH 30/30] build: Dev shell --- flake.nix | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index df63845..fdb3f6b 100644 --- a/flake.nix +++ b/flake.nix @@ -37,7 +37,6 @@ }; project = leanPkgs.buildLeanPackage { name = "Pantograph"; - #roots = pkgs.lib.optional pkgs.stdenv.isDarwin [ "Main" "Pantograph" ]; roots = [ "Main" "Pantograph" ]; src = pkgs.lib.cleanSourceWith { src = ./.; @@ -74,7 +73,9 @@ ${test.executable}/bin/test > $out ''; }; - devShells.default = project.devShell; + devShells.default = pkgs.mkShell { + buildInputs = [ leanPkgs.lean-all leanPkgs.lean ]; + }; }; }; }