diff --git a/.gitignore b/.gitignore index 21bcd46..53ec3bb 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,4 @@ .* !.gitignore - -*.olean -/build -/lake-packages +*.[io]lean +/result diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index be17729..4b3bd51 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -327,11 +327,11 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM -- Lean these are handled using a `#` prefix. pure s!"{deBruijnIndex}" | .fvar fvarId => - let name := ofName fvarId.name + let name := fvarId.name pure s!"(:fv {name})" | .mvar mvarId => do let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv" - let name := ofName mvarId.name + let name := mvarId.name pure s!"(:{pref} {name})" | .sort level => let level := serializeSortLevel level sanitize @@ -346,20 +346,20 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM let args := " ".intercalate args pure s!"({fn'} {args})" | .lam binderName binderType body binderInfo => do - let binderName' := ofName binderName + let binderName' := binderName.eraseMacroScopes let binderType' ← self binderType let body' ← self body let binderInfo' := binderInfoSexp binderInfo pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})" | .forallE binderName binderType body binderInfo => do - let binderName' := ofName binderName + let binderName' := binderName.eraseMacroScopes let binderType' ← self binderType let body' ← self body let binderInfo' := binderInfoSexp binderInfo pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})" | .letE name type value body _ => do -- Dependent boolean flag diacarded - let name' := serializeName name + let name' := name.eraseMacroScopes let type' ← self type let value' ← self value let body' ← self body @@ -387,7 +387,6 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM | .implicit => " :implicit" | .strictImplicit => " :strictImplicit" | .instImplicit => " :instImplicit" - ofName (name: Name) := serializeName name sanitize def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do let pp?: Option String ← match options.printExprPretty with @@ -420,13 +419,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava match localDecl with | .cdecl _ fvarId userName _ _ _ => return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName:= ofName userName.simpMacroScopes, isInaccessible := userName.isInaccessibleUserName } | .ldecl _ fvarId userName _ _ _ _ => do return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName := toString userName.simpMacroScopes, isInaccessible := userName.isInaccessibleUserName } @@ -436,7 +435,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava let userName := userName.simpMacroScopes let type ← instantiate type return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName:= ofName userName, isInaccessible := userName.isInaccessibleUserName type? := .some (← serializeExpression options type) @@ -450,7 +449,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava else pure $ .none return { - name := ofName fvarId.name, + name := fvarId.name.toString, userName:= ofName userName, isInaccessible := userName.isInaccessibleUserName type? := .some (← serializeExpression options type) @@ -469,7 +468,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava | false => ppVar localDecl return var::acc return { - name := ofName goal.name, + name := goal.name.toString, userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), isConversion := isLHSGoal? mvarDecl.type |>.isSome, target := (← serializeExpression options (← instantiate mvarDecl.type)), diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 79e3004..e190d5d 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -10,8 +10,6 @@ import Lean namespace Pantograph open Lean -def filename: String := "" - /-- Represents an interconnected set of metavariables, or a state in proof search -/ @@ -73,6 +71,8 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances } protected def GoalState.metaState (state: GoalState): Meta.State := state.savedState.term.meta.meta +protected def GoalState.coreState (state: GoalState): Core.SavedState := + state.savedState.term.meta.core protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do mvarId.withContext m |>.run' (← read) state.metaState @@ -202,16 +202,27 @@ inductive TacticResult where -- The given action cannot be executed in the state | invalidAction (message: String) -/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/ +/-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit): Elab.TermElabM TacticResult := do try let nextState ← state.step goal tacticM + + -- Check if error messages have been generated in the core. + let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length + |>.filterMapM λ m => do + if m.severity == .error then + return .some $ ← m.toString + else + return .none + if ¬ newMessages.isEmpty then + return .failure newMessages.toArray return .success nextState catch exception => return .failure #[← exception.toMessageData.toString] /-- Execute a string tactic on given state. Restores TermElabM -/ +@[export pantograph_goal_state_try_tactic_m] protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String): Elab.TermElabM TacticResult := do state.restoreElabM @@ -219,7 +230,7 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str (env := ← MonadEnv.getEnv) (catName := if state.isConv then `conv else `tactic) (input := tactic) - (fileName := filename) with + (fileName := ← getFileName) with | .ok stx => pure $ stx | .error error => return .parseError error state.tryTacticM goal $ Elab.Tactic.evalTactic tactic @@ -231,7 +242,7 @@ protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: Strin (env := ← MonadEnv.getEnv) (catName := `term) (input := expr) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => return .parseError error state.tryTacticM goal $ Tactic.evalAssign expr @@ -245,7 +256,7 @@ protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: St (env := ← MonadEnv.getEnv) (catName := `term) (input := type) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => return .parseError error state.tryTacticM goal $ Tactic.evalLet binderName.toName type @@ -332,7 +343,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String) (env := state.env) (catName := `term) (input := pred) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => return .parseError error goal.checkNotAssigned `GoalState.tryCalc @@ -353,7 +364,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String) throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}" if let some prevRhs := calcPrevRhs? then unless ← Meta.isDefEqGuarded lhs prevRhs do - throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- " + throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- Creates a mvar to represent the proof that the calc tactic solves the -- current branch diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index fcd5ebe..0cb6cac 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -289,6 +289,19 @@ structure GoalDiag where instantiate: Bool := true printSexp: Bool := false +structure GoalSave where + id: Nat + path: System.FilePath + deriving Lean.FromJson +structure GoalSaveResult where + deriving Lean.ToJson +structure GoalLoad where + path: System.FilePath + deriving Lean.FromJson +structure GoalLoadResult where + id: Nat + deriving Lean.ToJson + /-- Executes the Lean compiler on a single file -/ structure FrontendProcess where diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 2f04bdb..bd01169 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -2,6 +2,7 @@ import Lean.Environment import Lean.Replay import Init.System.IOError import Std.Data.HashMap +import Pantograph.Goal /-! Input/Output functions @@ -55,7 +56,7 @@ and when unpickling, we build a fresh `Environment` from the imports, and then add the new constants. -/ @[export pantograph_env_pickle_m] -def env_pickle (env : Environment) (path : System.FilePath) : IO Unit := +def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit := Pantograph.pickle path (env.header.imports, env.constants.map₂) /-- @@ -65,9 +66,97 @@ We construct a fresh `Environment` with the relevant imports, and then replace the new constants. -/ @[export pantograph_env_unpickle_m] -def env_unpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do +def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path let env ← importModules imports {} 0 return (← env.replay (Std.HashMap.ofList map₂.toList), region) + +open Lean.Core in +structure CompactCoreState where + -- env : Environment + nextMacroScope : MacroScope := firstFrontendMacroScope + 1 + ngen : NameGenerator := {} + -- traceState : TraceState := {} + -- cache : Cache := {} + -- messages : MessageLog := {} + -- infoState : Elab.InfoState := {} + +@[export pantograph_goal_state_pickle_m] +def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit := + let { + savedState := { + term := { + meta := { + core, + meta, + } + «elab», + }, + tactic + } + root, + parentMVar?, + convMVar?, + calcPrevRhs?, + } := goalState + --let env := core.env + Pantograph.pickle path ( + ({ core with } : CompactCoreState), + meta, + «elab», + tactic, + + root, + parentMVar?, + convMVar?, + calcPrevRhs?, + ) + +@[export pantograph_goal_state_unpickle_m] +def goalStateUnpickle (path : System.FilePath) (env : Environment) + : IO (GoalState × CompactedRegion) := unsafe do + let (( + compactCore, + meta, + «elab», + tactic, + + root, + parentMVar?, + convMVar?, + calcPrevRhs?, + ), region) ← Pantograph.unpickle ( + CompactCoreState × + Meta.State × + Elab.Term.State × + Elab.Tactic.State × + + MVarId × + Option MVarId × + Option (MVarId × MVarId × List MVarId) × + Option (MVarId × Expr) + ) path + let goalState := { + savedState := { + term := { + meta := { + core := { + compactCore with + passedHeartbeats := 0, + env, + }, + meta, + }, + «elab», + }, + tactic, + }, + root, + parentMVar?, + convMVar?, + calcPrevRhs?, + } + return (goalState, region) + end Pantograph diff --git a/README.md b/README.md index 04213ae..e070fff 100644 --- a/README.md +++ b/README.md @@ -7,6 +7,8 @@ A Machine-to-Machine interaction system for Lean 4. Pantograph provides interfaces to execute proofs, construct expressions, and examine the symbol list of a Lean project for machine learning. +See [documentations](doc/) for design rationale and references. + ## Installation For Nix users, run @@ -15,7 +17,9 @@ nix build .#{sharedLib,executable} ``` to build either the shared library or executable. -Install `elan` and `lake`, and run +Install `lake` and `lean` fixed to the version of the `lean-toolchain` file, and +run + ``` sh lake build ``` @@ -24,9 +28,12 @@ This builds the executable in `.lake/build/bin/pantograph-repl`. ## Executable Usage ``` sh -pantograph MODULES|LEAN_OPTIONS +pantograph-repl MODULES|LEAN_OPTIONS ``` +The `pantograph-repl` executable must be run with a list of modules to import. +It can also accept lean options of the form `--key=value` e.g. `--pp.raw=true`. + The REPL loop accepts commands as single-line JSON inputs and outputs either an `Error:` (indicating malformed command) or a JSON return value indicating the result of a command execution. The command can be passed in one of two formats @@ -37,8 +44,6 @@ command { ... } The list of available commands can be found in `Pantograph/Protocol.lean` and below. An empty command aborts the REPL. -The `pantograph` executable must be run with a list of modules to import. It can -also accept lean options of the form `--key=value` e.g. `--pp.raw=true`. Example: (~5k symbols) ``` @@ -64,62 +69,7 @@ stat ``` where the application of `assumption` should lead to a failure. -### Commands - -See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. -* `reset`: Delete all cached expressions and proof trees -* `stat`: Display resource usage -* `expr.echo {"expr": , "type": , ["levels": []]}`: Determine the - type of an expression and format it. -* `env.catalog`: Display a list of all safe Lean symbols in the current environment -* `env.inspect {"name": , "value": }`: Show the type and package of a - given symbol; If value flag is set, the value is printed or hidden. By default - only the values of definitions are printed. -* `options.set { key: value, ... }`: Set one or more options (not Lean options; those - have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` - - One particular option for interest for machine learning researchers is the - automatic mode (flag: `"automaticMode"`). By default it is turned on, with - all goals automatically resuming. This makes Pantograph act like a gym, - with no resumption necessary to manage your goals. -* `options.print`: Display the current set of options -* `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: - Start a new proof from a given expression or symbol -* `goal.tactic {"stateId": , "goalId": , ...}`: Execute a tactic string on a - given goal. The tactic is supplied as additional key-value pairs in one of the following formats: - - `{ "tactic": }`: Execute an ordinary tactic - - `{ "expr": }`: Assign the given proof term to the current goal - - `{ "have": , "binderName": }`: Execute `have` and creates a branch goal - - `{ "calc": }`: Execute one step of a `calc` tactic. Each step must - be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set - to the previous `rhs`. - - `{ "conv": }`: Enter or exit conversion tactic mode. In the case of - exit, the goal id is ignored. -* `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: - Execute continuation/resumption - - `{ "branch": }`: Continue on branch state. The current state must have no goals. - - `{ "goals": }`: Resume the given goals -* `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list -* `goal.print {"stateId": }"`: Print a goal state -* `frontend.process { ["fileName": ",] ["file": ], invocations: - , sorrys: }`: Executes the Lean frontend on a file, collecting - either the tactic invocations (`"invocations": true`) or the sorrys into goal - states (`"sorrys": true`) - -### Errors - -When an error pertaining to the execution of a command happens, the returning JSON structure is - -``` json -{ "error": "type", "desc": "description" } -``` -Common error forms: -* `command`: Indicates malformed command structure which results from either - invalid command or a malformed JSON structure that cannot be fed to an - individual command. -* `index`: Indicates an invariant maintained by the output of one command and - 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. +For a list of commands, see [REPL Documentation](doc/repl.md). ### Project Environment @@ -130,7 +80,7 @@ the environment might be setup like this: ``` sh LIB="../lib" -LIB_MATHLIB="$LIB/mathlib4/lake-packages" +LIB_MATHLIB="$LIB/mathlib4/.lake" export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib" LEAN_PATH=$LEAN_PATH build/bin/pantograph $@ diff --git a/Repl.lean b/Repl.lean index e162f05..3f8a3c6 100644 --- a/Repl.lean +++ b/Repl.lean @@ -15,6 +15,16 @@ structure State where /-- Main state monad for executing commands -/ abbrev MainM := ReaderT Context (StateT State Lean.CoreM) +def newGoalState (goalState: GoalState) : MainM Nat := do + let state ← get + let stateId := state.nextId + set { state with + goalStates := state.goalStates.insert stateId goalState, + nextId := state.nextId + 1 + } + return stateId + + -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables -- certain monadic features in `MainM` abbrev CR α := Except Protocol.InteractionError α @@ -50,6 +60,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | "goal.continue" => run goal_continue | "goal.delete" => run goal_delete | "goal.print" => run goal_print + | "goal.save" => run goal_save + | "goal.load" => run goal_load | "frontend.process" => run frontend_process | cmd => let error: Protocol.InteractionError := @@ -62,14 +74,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do errorCommand := errorI "command" errorIndex := errorI "index" errorIO := errorI "io" - newGoalState (goalState: GoalState) : MainM Nat := do - let state ← get - let stateId := state.nextId - set { state with - goalStates := state.goalStates.insert stateId goalState, - nextId := state.nextId + 1 - } - return stateId -- Command Functions reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get @@ -90,10 +94,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Environment.addDecl args env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do let env ← Lean.MonadEnv.getEnv - env_pickle env args.path + environmentPickle env args.path return .ok {} env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do - let (env, _) ← env_unpickle args.path + let (env, _) ← environmentUnpickle args.path Lean.setEnv env return .ok {} expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do @@ -203,11 +207,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match nextState? with | .error error => return .error <| errorI "structure" error | .ok nextGoalState => - let nextStateId := state.nextId - set { state with - goalStates := state.goalStates.insert nextStateId nextGoalState, - nextId := state.nextId + 1 - } + let nextStateId ← newGoalState nextGoalState let goals ← goalSerialize nextGoalState (options := state.options) return .ok { nextStateId, @@ -224,6 +224,16 @@ def execute (command: Protocol.Command): MainM Lean.Json := do return .error $ errorIndex s!"Invalid state index {args.stateId}" let result ← runMetaInMainM <| goalPrint goalState state.options return .ok result + goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do + let state ← get + let .some goalState := state.goalStates[args.id]? | + return .error $ errorIndex s!"Invalid state index {args.id}" + goalStatePickle goalState args.path + return .ok {} + goal_load (args: Protocol.GoalLoad): MainM (CR Protocol.GoalLoadResult) := do + let (goalState, _) ← goalStateUnpickle args.path (← Lean.MonadEnv.getEnv) + let id ← newGoalState goalState + return .ok { id } frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do let options := (← get).options try diff --git a/Test/Common.lean b/Test/Common.lean index 3998293..53adaa0 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -95,19 +95,19 @@ def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq) def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e -def strToTermSyntax [Monad m] [MonadEnv m] (s: String): m Syntax := do +def strToTermSyntax (s: String): CoreM Syntax := do let .ok stx := Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := s) - (fileName := filename) | panic! s!"Failed to parse {s}" + (fileName := ← getFileName) | panic! s!"Failed to parse {s}" return stx def parseSentence (s: String): Elab.TermElabM Expr := do let stx ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := s) - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" Elab.Term.elabTerm (stx := stx) .none @@ -123,13 +123,28 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do -- Monadic testing -abbrev TestT := StateT LSpec.TestSeq +abbrev TestT := StateRefT' IO.RealWorld LSpec.TestSeq -def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do +section Monadic + +variable [Monad m] [MonadLiftT (ST IO.RealWorld) m] + +def addTest (test: LSpec.TestSeq) : TestT m Unit := do set $ (← get) ++ test -def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq := +def checkEq [DecidableEq α] [Repr α] (desc : String) (lhs rhs : α) : TestT m Unit := do + addTest $ LSpec.check desc (lhs = rhs) +def checkTrue (desc : String) (flag : Bool) : TestT m Unit := do + addTest $ LSpec.check desc flag +def fail (desc : String) : TestT m Unit := do + addTest $ LSpec.check desc false + +def runTest (t: TestT m Unit): m LSpec.TestSeq := Prod.snd <$> t.run LSpec.TestSeq.done +def runTestWithResult { α } (t: TestT m α): m (α × LSpec.TestSeq) := + t.run LSpec.TestSeq.done + +end Monadic def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit): IO LSpec.TestSeq := diff --git a/Test/Delate.lean b/Test/Delate.lean index 227ab24..d918dc8 100644 --- a/Test/Delate.lean +++ b/Test/Delate.lean @@ -32,7 +32,7 @@ def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do let entries: List (String × String) := [ -- This one contains unhygienic variable names which must be suppressed - ("Nat.add", "(:forall _ (:c Nat) (:forall _ (:c Nat) (:c Nat)))"), + ("Nat.add", "(:forall a (:c Nat) (:forall a (:c Nat) (:c Nat)))"), -- These ones are normal and easy ("Nat.add_one", "(: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)))"), ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"), diff --git a/Test/Library.lean b/Test/Library.lean index d995374..df1ba4d 100644 --- a/Test/Library.lean +++ b/Test/Library.lean @@ -24,7 +24,7 @@ def test_expr_echo (env: Environment): IO LSpec.TestSeq := do }, expr := { pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩", - sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall _ 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))", + sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall a 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))", } })) return tests diff --git a/Test/Main.lean b/Test/Main.lean index 25bb0d9..6bf410e 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,11 +1,12 @@ import LSpec +import Test.Delate import Test.Environment import Test.Frontend import Test.Integration import Test.Library import Test.Metavar import Test.Proofs -import Test.Delate +import Test.Serial import Test.Tactic -- Test running infrastructure @@ -51,6 +52,7 @@ def main (args: List String) := do ("Metavar", Metavar.suite env_default), ("Proofs", Proofs.suite env_default), ("Delate", Delate.suite env_default), + ("Serial", Serial.suite env_default), ("Tactic/Congruence", Tactic.Congruence.suite env_default), ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default), ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default), diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 506e963..c6fc4f0 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -8,10 +8,7 @@ namespace Pantograph.Test.Metavar open Pantograph open Lean -abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM) - -def addTest (test: LSpec.TestSeq): TestM Unit := do - set $ (← get) ++ test +abbrev TestM := TestT $ ReaderT Protocol.Options Elab.TermElabM -- Tests that all delay assigned mvars are instantiated def test_instantiate_mvar: TestM Unit := do @@ -32,8 +29,6 @@ def test_instantiate_mvar: TestM Unit := do "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))") return () - - def startProof (expr: String): TestM (Option GoalState) := do let env ← Lean.MonadEnv.getEnv let syn? := parseTerm env expr diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 8e3e2a2..65f099f 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -14,10 +14,7 @@ inductive Start where | copy (name: String) -- Start from some name in the environment | expr (expr: String) -- Start from some expression -abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM) - -def addTest (test: LSpec.TestSeq): TestM Unit := do - set $ (← get) ++ test +abbrev TestM := TestT $ ReaderT Protocol.Options $ Elab.TermElabM def startProof (start: Start): TestM (Option GoalState) := do let env ← Lean.MonadEnv.getEnv @@ -282,9 +279,9 @@ def test_or_comm: TestM Unit := do serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false) let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))" let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))" - let motive := s!"(:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))" - let caseL := s!"(:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))" - let caseR := s!"(:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))" + let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))" + let caseL := s!"(:lambda h (:fv {fvP}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))" + let caseR := s!"(:lambda h (:fv {fvQ}) (:lambda h ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))" let conduit := s!"((:c Eq.refl) {orPQ} (:fv {fvH}))" addTest $ LSpec.test "(2 parent)" (state2parent == s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})") @@ -704,6 +701,25 @@ def test_nat_zero_add_alt: TestM Unit := do } ]) +def test_composite_tactic_failure: TestM Unit := do + let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let tactic := "intro p" + let state1 ← match ← state0.tacticOn 0 tactic with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + + let tactic := "exact ⟨0, by simp⟩" + let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail" + checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"] + def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ ("identity", test_identity), @@ -716,6 +732,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("calc", test_calc), ("Nat.zero_add", test_nat_zero_add), ("Nat.zero_add alt", test_nat_zero_add_alt), + ("composite tactic failure", test_composite_tactic_failure), ] tests.map (fun (name, test) => (name, proofRunner env test)) diff --git a/Test/Serial.lean b/Test/Serial.lean new file mode 100644 index 0000000..fcdc155 --- /dev/null +++ b/Test/Serial.lean @@ -0,0 +1,109 @@ +import LSpec +import Test.Common +import Lean +import Pantograph.Library + +open Lean + +namespace Pantograph.Test.Serial + +def tempPath : IO System.FilePath := do + Prod.snd <$> IO.FS.createTempFile + +structure MultiState where + coreContext : Core.Context + env: Environment + +abbrev TestM := TestT $ StateRefT MultiState $ IO + +instance : MonadEnv TestM where + getEnv := return (← getThe MultiState).env + modifyEnv f := do modifyThe MultiState fun s => { s with env := f s.env } + +def runCoreM { α } (state : Core.State) (testCoreM : TestT CoreM α) : TestM (α × Core.State) := do + let multiState ← getThe MultiState + let coreM := runTestWithResult testCoreM + match ← (coreM.run multiState.coreContext state).toBaseIO with + | .error e => do + throw $ .userError $ ← e.toMessageData.toString + | .ok ((a, tests), state') => do + set $ (← getThe LSpec.TestSeq) ++ tests + return (a, state') + +def test_environment_pickling : TestM Unit := do + let coreSrc : Core.State := { env := ← getEnv } + let coreDst : Core.State := { env := ← getEnv } + + let name := `mystery + let envPicklePath ← tempPath + let ((), _) ← runCoreM coreSrc do + let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default + let value: Expr := .lam `p (.sort 0) (.lam `h (.bvar 0) (.bvar 0) .default) .default + let c := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx + (name := name) + (levelParams := []) + (type := type) + (value := value) + (hints := Lean.mkReducibilityHintsRegularEx 1) + (safety := Lean.DefinitionSafety.safe) + (all := []) + let env' ← match (← getEnv).addDecl (← getOptions) c with + | .error e => do + let error ← (e.toMessageData (← getOptions)).toString + throwError error + | .ok env' => pure env' + environmentPickle env' envPicklePath + + let _ ← runCoreM coreDst do + let (env', _) ← environmentUnpickle envPicklePath + checkTrue s!"Has symbol {name}" (env'.find? name).isSome + let anotherName := `mystery2 + checkTrue s!"Doesn't have symbol {anotherName}" (env'.find? anotherName).isNone + + IO.FS.removeFile envPicklePath + +def test_goal_state_pickling_simple : TestM Unit := do + let coreSrc : Core.State := { env := ← getEnv } + let coreDst : Core.State := { env := ← getEnv } + let statePath ← tempPath + + let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default + let stateGenerate : MetaM GoalState := runTermElabMInMeta do + GoalState.create type + + let ((), _) ← runCoreM coreSrc do + let state ← stateGenerate.run' + goalStatePickle state statePath + + let ((), _) ← runCoreM coreDst do + let (goalState, _) ← goalStateUnpickle statePath (← getEnv) + let metaM : MetaM (List Expr) := do + goalState.goals.mapM λ goal => goalState.withContext goal goal.getType + let types ← metaM.run' + checkTrue "Goals" $ types[0]!.equal type + + IO.FS.removeFile statePath + +structure Test where + name : String + routine: TestM Unit + +protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq := do + -- Create the state + let state : MultiState := { + coreContext := ← createCoreContext #[], + env, + } + match ← ((runTest $ test.routine).run' state).toBaseIO with + | .ok e => return e + | .error e => + return LSpec.check s!"Emitted exception: {e.toString}" (e.toString == "") + +def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := + let tests: List Test := [ + { name := "environment_pickling", routine := test_environment_pickling, }, + { name := "goal_state_pickling_simple", routine := test_goal_state_pickling_simple, }, + ] + tests.map (fun test => (test.name, test.run env)) + +end Pantograph.Test.Serial diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 4fb05e3..61d7d6c 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -28,7 +28,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "@Nat.brecOn") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -52,7 +52,7 @@ def test_list_brec_on : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "@List.brecOn") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -74,7 +74,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "@Nat.brecOn") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" let expr ← parseSentence expr diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean index ac277e2..93f0606 100644 --- a/Test/Tactic/NoConfuse.lean +++ b/Test/Tactic/NoConfuse.lean @@ -15,7 +15,7 @@ def test_nat : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -32,7 +32,7 @@ def test_nat_fail : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic @@ -52,7 +52,7 @@ def test_list : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index 132718a..b3347cb 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -15,7 +15,7 @@ def test_define : TestT Elab.TermElabM Unit := do (env := ← MonadEnv.getEnv) (catName := `term) (input := "Or.inl h") - (fileName := filename) with + (fileName := ← getFileName) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" -- Apply the tactic diff --git a/doc/icon.svg b/doc/icon.svg index 394b412..eb26a19 100644 --- a/doc/icon.svg +++ b/doc/icon.svg @@ -4,17 +4,17 @@ + + + + + + + + + + + + + + + id="layer4" + inkscape:label="bg" /> + + + + + + + + + + + diff --git a/doc/rationale.md b/doc/rationale.md new file mode 100644 index 0000000..87c1606 --- /dev/null +++ b/doc/rationale.md @@ -0,0 +1,30 @@ +# Design Rationale + +A great problem in machine learning is to use ML agents to automatically prove +mathematical theorems. This sort of proof necessarily involves *search*. +Compatibility for search is the main reason for creating Pantograph. The Lean 4 +LSP interface is not conducive to search. Pantograph is designed with this in +mind. It emphasizes the difference between 3 views of a proof: + +- **Presentation View**: The view of a written, polished proof. e.g. Mathlib and + math papers are almost always written in this form. +- **Search View**: The view of a proof exploration trajectory. This is not + explicitly supported by Lean LSP. +- **Kernel View**: The proof viewed as a set of metavariables. + +Pantograph enables proof agents to operate on the search view. + +## Name + +The name Pantograph is a pun. It means two things +- A pantograph is an instrument for copying down writing. As an agent explores + the vast proof search space, Pantograph records the current state to ensure + the proof is sound. +- A pantograph is also an equipment for an electric train. It supplies power to + a locomotive. In comparison the (relatively) simple Pantograph software powers + theorem proving projects. + +## References + +* [Pantograph Paper](https://arxiv.org/abs/2410.16429) + diff --git a/doc/repl.md b/doc/repl.md new file mode 100644 index 0000000..464c7cc --- /dev/null +++ b/doc/repl.md @@ -0,0 +1,64 @@ +# REPL + +## Commands + +See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. +* `reset`: Delete all cached expressions and proof trees +* `stat`: Display resource usage +* `expr.echo {"expr": , "type": , ["levels": []]}`: Determine the + type of an expression and format it. +* `env.catalog`: Display a list of all safe Lean symbols in the current environment +* `env.inspect {"name": , "value": }`: Show the type and package of a + given symbol; If value flag is set, the value is printed or hidden. By default + only the values of definitions are printed. +* `env.save { "path": }`, `env.load { "path": }`: Save/Load the + current environment to/from a file +* `options.set { key: value, ... }`: Set one or more options (not Lean options; those + have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` + + One particular option for interest for machine learning researchers is the + automatic mode (flag: `"automaticMode"`). By default it is turned on, with + all goals automatically resuming. This makes Pantograph act like a gym, + with no resumption necessary to manage your goals. +* `options.print`: Display the current set of options +* `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: + Start a new proof from a given expression or symbol +* `goal.tactic {"stateId": , "goalId": , ...}`: Execute a tactic string on a + given goal. The tactic is supplied as additional key-value pairs in one of the following formats: + - `{ "tactic": }`: Execute an ordinary tactic + - `{ "expr": }`: Assign the given proof term to the current goal + - `{ "have": , "binderName": }`: Execute `have` and creates a branch goal + - `{ "calc": }`: Execute one step of a `calc` tactic. Each step must + be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set + to the previous `rhs`. + - `{ "conv": }`: Enter or exit conversion tactic mode. In the case of + exit, the goal id is ignored. +* `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: + Execute continuation/resumption + - `{ "branch": }`: Continue on branch state. The current state must have no goals. + - `{ "goals": }`: Resume the given goals +* `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list +* `goal.print {"stateId": }"`: Print a goal state +* `goal.save { "id": , "path": }`, `goal.load { "path": }`: + Save/Load a goal state to/from a file. The environment is not carried with the + state. The user is responsible to ensure the sender/receiver instances share + the same environment. +* `frontend.process { ["fileName": ,] ["file": ], invocations: + , sorrys: }`: Executes the Lean frontend on a file, collecting + either the tactic invocations (`"invocations": true`) or the sorrys into goal + states (`"sorrys": true`) + +## Errors + +When an error pertaining to the execution of a command happens, the returning JSON structure is + +``` json +{ "error": "type", "desc": "description" } +``` +Common error forms: +* `command`: Indicates malformed command structure which results from either + invalid command or a malformed JSON structure that cannot be fed to an + individual command. +* `index`: Indicates an invariant maintained by the output of one command and + 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.