Compare commits
No commits in common. "c19fd1bcfb104d6563baaf3990013b219e089a24" and "71327d2d55f541c532d74c9e4563f47a23b2f458" have entirely different histories.
c19fd1bcfb
...
71327d2d55
|
@ -1,6 +1,5 @@
|
|||
.*
|
||||
!.gitignore
|
||||
|
||||
*.olean
|
||||
/build
|
||||
/lake-packages
|
||||
|
|
|
@ -8,7 +8,7 @@ import Pantograph
|
|||
open Pantograph
|
||||
|
||||
/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
|
||||
def parseCommand (s: String): Except String Protocol.Command := do
|
||||
def parse_command (s: String): Except String Commands.Command := do
|
||||
let s := s.trim
|
||||
match s.get? 0 with
|
||||
| .some '{' => -- Parse in Json mode
|
||||
|
@ -26,9 +26,9 @@ unsafe def loop : MainM Unit := do
|
|||
let state ← get
|
||||
let command ← (← IO.getStdin).getLine
|
||||
if command.trim.length = 0 then return ()
|
||||
match parseCommand command with
|
||||
match parse_command command with
|
||||
| .error error =>
|
||||
let error := Lean.toJson ({ error := "command", desc := error }: Protocol.InteractionError)
|
||||
let error := Lean.toJson ({ error := "command", desc := error }: Commands.InteractionError)
|
||||
-- Using `Lean.Json.compress` here to prevent newline
|
||||
IO.println error.compress
|
||||
| .ok command =>
|
||||
|
@ -88,7 +88,7 @@ unsafe def main (args: List String): IO Unit := do
|
|||
let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
|
||||
|
||||
let env ← Lean.importModules
|
||||
(imports := imports.toArray.map (λ str => { module := str_to_name str, runtimeOnly := false }))
|
||||
(imports := imports.map (λ str => { module := str_to_name str, runtimeOnly := false }))
|
||||
(opts := {})
|
||||
(trustLevel := 1)
|
||||
let context: Context := {
|
||||
|
@ -108,7 +108,6 @@ unsafe def main (args: List String): IO Unit := do
|
|||
errToSorry := false
|
||||
})
|
||||
let coreM := metaM.run'
|
||||
IO.println "ready."
|
||||
discard <| coreM.toIO coreContext { env := env }
|
||||
catch ex =>
|
||||
IO.println "Uncaught IO exception"
|
||||
|
|
20
Makefile
20
Makefile
|
@ -1,20 +0,0 @@
|
|||
LIB := build/lib/Pantograph.olean
|
||||
EXE := build/bin/pantograph
|
||||
SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain
|
||||
|
||||
TEST_EXE := build/bin/test
|
||||
TEST_SOURCE := $(wildcard Test/*.lean)
|
||||
|
||||
$(LIB) $(EXE): $(SOURCE)
|
||||
lake build pantograph
|
||||
|
||||
$(TEST_EXE): $(LIB) $(TEST_SOURCE)
|
||||
lake build test
|
||||
|
||||
test: $(TEST_EXE)
|
||||
lake env $(TEST_EXE)
|
||||
|
||||
clean:
|
||||
lake clean
|
||||
|
||||
.PHONY: test clean
|
143
Pantograph.lean
143
Pantograph.lean
|
@ -1,8 +1,7 @@
|
|||
import Pantograph.Goal
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.SemihashMap
|
||||
import Pantograph.Commands
|
||||
import Pantograph.Serial
|
||||
import Pantograph.Symbol
|
||||
import Pantograph.Symbols
|
||||
import Pantograph.Tactic
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
|
@ -11,16 +10,17 @@ structure Context where
|
|||
|
||||
/-- Stores state of the REPL -/
|
||||
structure State where
|
||||
options: Protocol.Options := {}
|
||||
goalStates: SemihashMap GoalState := SemihashMap.empty
|
||||
options: Commands.Options := {}
|
||||
--environments: Array Lean.Environment := #[]
|
||||
proofTrees: Array ProofTree := #[]
|
||||
|
||||
/-- Main state monad for executing commands -/
|
||||
-- State monad
|
||||
abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM)
|
||||
-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
|
||||
-- certain monadic features in `MainM`
|
||||
abbrev CR α := Except Protocol.InteractionError α
|
||||
-- For some reason writing `CommandM α := MainM (Except ... α)` disables certain
|
||||
-- monadic features in `MainM`
|
||||
abbrev CR α := Except Commands.InteractionError α
|
||||
|
||||
def execute (command: Protocol.Command): MainM Lean.Json := do
|
||||
def execute (command: Commands.Command): MainM Lean.Json := do
|
||||
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
|
||||
match Lean.fromJson? command.payload with
|
||||
| .ok args => do
|
||||
|
@ -29,43 +29,37 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
| .error ierror => return Lean.toJson ierror
|
||||
| .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
|
||||
match command.cmd with
|
||||
| "reset" => run reset
|
||||
| "stat" => run stat
|
||||
| "expr.echo" => run expr_echo
|
||||
| "lib.catalog" => run lib_catalog
|
||||
| "lib.inspect" => run lib_inspect
|
||||
| "options.set" => run options_set
|
||||
| "options.print" => run options_print
|
||||
| "goal.start" => run goal_start
|
||||
| "goal.tactic" => run goal_tactic
|
||||
| "goal.delete" => run goal_delete
|
||||
| "goal.print" => run goal_print
|
||||
| "reset" => run reset
|
||||
| "expr.echo" => run expr_echo
|
||||
| "lib.catalog" => run lib_catalog
|
||||
| "lib.inspect" => run lib_inspect
|
||||
| "options.set" => run options_set
|
||||
| "options.print" => run options_print
|
||||
| "proof.start" => run proof_start
|
||||
| "proof.tactic" => run proof_tactic
|
||||
| "proof.printTree" => run proof_print_tree
|
||||
| cmd =>
|
||||
let error: Protocol.InteractionError :=
|
||||
let error: Commands.InteractionError :=
|
||||
errorCommand s!"Unknown command {cmd}"
|
||||
return Lean.toJson error
|
||||
where
|
||||
errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
|
||||
errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc }
|
||||
errorCommand := errorI "command"
|
||||
errorIndex := errorI "index"
|
||||
-- Command Functions
|
||||
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
|
||||
reset (_: Commands.Reset): MainM (CR Commands.ResetResult) := do
|
||||
let state ← get
|
||||
let nGoals := state.goalStates.size
|
||||
set { state with goalStates := SemihashMap.empty }
|
||||
return .ok { nGoals }
|
||||
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
|
||||
let state ← get
|
||||
let nGoals := state.goalStates.size
|
||||
return .ok { nGoals }
|
||||
lib_catalog (_: Protocol.LibCatalog): MainM (CR Protocol.LibCatalogResult) := do
|
||||
let nTrees := state.proofTrees.size
|
||||
set { state with proofTrees := #[] }
|
||||
return .ok { nTrees := nTrees }
|
||||
lib_catalog (_: Commands.LibCatalog): MainM (CR Commands.LibCatalogResult) := 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 }
|
||||
lib_inspect (args: Protocol.LibInspect): MainM (CR Protocol.LibInspectResult) := do
|
||||
lib_inspect (args: Commands.LibInspect): MainM (CR Commands.LibInspectResult) := do
|
||||
let state ← get
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
let name := str_to_name args.name
|
||||
|
@ -85,7 +79,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
value? := ← value?.mapM (λ v => serialize_expression state.options v),
|
||||
module? := module?
|
||||
}
|
||||
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
|
||||
expr_echo (args: Commands.ExprEcho): MainM (CR Commands.ExprEchoResult) := do
|
||||
let state ← get
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
match syntax_from_str env args.expr with
|
||||
|
@ -102,7 +96,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
}
|
||||
catch exception =>
|
||||
return .error $ errorI "typing" (← exception.toMessageData.toString)
|
||||
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
|
||||
options_set (args: Commands.OptionsSet): MainM (CR Commands.OptionsSetResult) := do
|
||||
let state ← get
|
||||
let options := state.options
|
||||
set { state with
|
||||
|
@ -111,15 +105,15 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
|
||||
printExprPretty := args.printExprPretty?.getD options.printExprPretty,
|
||||
printExprAST := args.printExprAST?.getD options.printExprAST,
|
||||
noRepeat := args.noRepeat?.getD options.noRepeat,
|
||||
proofVariableDelta := args.proofVariableDelta?.getD options.proofVariableDelta,
|
||||
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
|
||||
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
|
||||
}
|
||||
}
|
||||
return .ok { }
|
||||
options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.OptionsPrintResult) := do
|
||||
options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do
|
||||
return .ok (← get).options
|
||||
goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
|
||||
proof_start (args: Commands.ProofStart): MainM (CR Commands.ProofStartResult) := do
|
||||
let state ← get
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with
|
||||
|
@ -134,55 +128,38 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
(match env.find? <| str_to_name copyFrom with
|
||||
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
|
||||
| .some cInfo => return .ok cInfo.type)
|
||||
| _, _ =>
|
||||
return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
|
||||
| .none, .none =>
|
||||
return .error <| errorI "arguments" "At least one of {expr, copyFrom} must be supplied"
|
||||
| _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}")
|
||||
match expr? with
|
||||
| .error error => return .error error
|
||||
| .ok expr =>
|
||||
let goalState ← GoalState.create expr
|
||||
let (goalStates, stateId) := state.goalStates.insert goalState
|
||||
set { state with goalStates }
|
||||
return .ok { stateId }
|
||||
goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
|
||||
let tree ← ProofTree.create expr
|
||||
-- Put the new tree in the environment
|
||||
let nextTreeId := state.proofTrees.size
|
||||
set { state with proofTrees := state.proofTrees.push tree }
|
||||
return .ok { treeId := nextTreeId }
|
||||
proof_tactic (args: Commands.ProofTactic): MainM (CR Commands.ProofTacticResult) := do
|
||||
let state ← get
|
||||
match state.goalStates.get? args.stateId with
|
||||
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
|
||||
| .some goalState => do
|
||||
let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
|
||||
| .some tactic, .none => do
|
||||
pure ( Except.ok (← GoalState.execute goalState args.goalId tactic))
|
||||
| .none, .some expr => do
|
||||
pure ( Except.ok (← GoalState.tryAssign 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
|
||||
| .ok (.success nextGoalState) =>
|
||||
let (goalStates, nextStateId) := state.goalStates.insert nextGoalState
|
||||
set { state with goalStates }
|
||||
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options)
|
||||
return .ok {
|
||||
nextStateId? := .some nextStateId,
|
||||
goals? := .some goals,
|
||||
}
|
||||
| .ok (.parseError message) =>
|
||||
return .ok { parseError? := .some message }
|
||||
| .ok (.indexError goalId) =>
|
||||
return .error $ errorIndex s!"Invalid goal id index {goalId}"
|
||||
| .ok (.failure messages) =>
|
||||
match state.proofTrees.get? args.treeId with
|
||||
| .none => return .error $ errorIndex "Invalid tree index {args.treeId}"
|
||||
| .some tree =>
|
||||
let (result, nextTree) ← ProofTree.execute
|
||||
(stateId := args.stateId)
|
||||
(goalId := args.goalId.getD 0)
|
||||
(tactic := args.tactic) |>.run state.options |>.run tree
|
||||
match result with
|
||||
| .invalid message => return .error $ errorIndex message
|
||||
| .success nextId? goals =>
|
||||
set { state with proofTrees := state.proofTrees.set! args.treeId nextTree }
|
||||
return .ok { nextId? := nextId?, goals? := .some goals }
|
||||
| .failure messages =>
|
||||
return .ok { tacticErrors? := .some messages }
|
||||
goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
|
||||
proof_print_tree (args: Commands.ProofPrintTree): MainM (CR Commands.ProofPrintTreeResult) := do
|
||||
let state ← get
|
||||
let goalStates := args.stateIds.foldl (λ map id => map.remove id) state.goalStates
|
||||
set { state with goalStates }
|
||||
return .ok {}
|
||||
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
|
||||
let state ← get
|
||||
match state.goalStates.get? args.stateId with
|
||||
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
|
||||
| .some goalState => do
|
||||
let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
|
||||
return .ok {
|
||||
root?,
|
||||
}
|
||||
match state.proofTrees.get? args.treeId with
|
||||
| .none => return .error $ errorIndex "Invalid tree index {args.treeId}"
|
||||
| .some tree =>
|
||||
return .ok { parents := tree.structure_array }
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -6,7 +6,7 @@ its field names to avoid confusion with error messages generated by the REPL.
|
|||
-/
|
||||
import Lean.Data.Json
|
||||
|
||||
namespace Pantograph.Protocol
|
||||
namespace Pantograph.Commands
|
||||
|
||||
|
||||
/-- Main Option structure, placed here to avoid name collision -/
|
||||
|
@ -18,10 +18,9 @@ structure Options where
|
|||
printExprPretty: Bool := true
|
||||
-- When enabled, print the raw AST of expressions
|
||||
printExprAST: Bool := false
|
||||
-- When enabled, the types and values of persistent variables in a goal
|
||||
-- are not shown unless they are new to the proof step. Reduces overhead.
|
||||
-- NOTE: that this assumes the type and assignment of variables can never change.
|
||||
noRepeat: Bool := false
|
||||
-- When enabled, the types and values of persistent variables in a proof goal
|
||||
-- are not shown unless they are new to the proof step. Reduces overhead
|
||||
proofVariableDelta: Bool := false
|
||||
-- See `pp.auxDecls`
|
||||
printAuxDecls: Bool := false
|
||||
-- See `pp.implementationDetailHyps`
|
||||
|
@ -44,10 +43,7 @@ structure Expression where
|
|||
deriving Lean.ToJson
|
||||
|
||||
structure Variable where
|
||||
/-- The internal name used in raw expressions -/
|
||||
name: String := ""
|
||||
/-- The name displayed to the user -/
|
||||
userName: String
|
||||
name: String
|
||||
/-- Does the name contain a dagger -/
|
||||
isInaccessible?: Option Bool := .none
|
||||
type?: Option Expression := .none
|
||||
|
@ -84,11 +80,8 @@ structure InteractionError where
|
|||
|
||||
structure Reset where
|
||||
deriving Lean.FromJson
|
||||
structure Stat where
|
||||
deriving Lean.FromJson
|
||||
structure StatResult where
|
||||
-- Number of goals states
|
||||
nGoals: Nat
|
||||
structure ResetResult where
|
||||
nTrees: Nat
|
||||
deriving Lean.ToJson
|
||||
|
||||
-- Return the type of an expression
|
||||
|
@ -124,7 +117,7 @@ structure OptionsSet where
|
|||
printJsonPretty?: Option Bool
|
||||
printExprPretty?: Option Bool
|
||||
printExprAST?: Option Bool
|
||||
noRepeat?: Option Bool
|
||||
proofVariableDelta?: Option Bool
|
||||
printAuxDecls?: Option Bool
|
||||
printImplementationDetailHyps?: Option Bool
|
||||
deriving Lean.FromJson
|
||||
|
@ -134,57 +127,35 @@ structure OptionsPrint where
|
|||
deriving Lean.FromJson
|
||||
abbrev OptionsPrintResult := Options
|
||||
|
||||
structure GoalStart where
|
||||
structure ProofStart where
|
||||
-- Only one of the fields below may be populated.
|
||||
expr: Option String -- Directly parse in an expression
|
||||
copyFrom: Option String -- Copy the type from a theorem in the environment
|
||||
expr: Option String -- Proof expression
|
||||
copyFrom: Option String -- Theorem name
|
||||
deriving Lean.FromJson
|
||||
structure GoalStartResult where
|
||||
stateId: Nat := 0
|
||||
structure ProofStartResult where
|
||||
treeId: Nat := 0 -- Proof tree id
|
||||
deriving Lean.ToJson
|
||||
structure GoalTactic where
|
||||
structure ProofTactic where
|
||||
-- Identifiers for tree, state, and goal
|
||||
treeId: Nat
|
||||
stateId: Nat
|
||||
goalId: Nat := 0
|
||||
-- One of the fields here must be filled
|
||||
tactic?: Option String := .none
|
||||
expr?: Option String := .none
|
||||
goalId: Option Nat -- Defaults to 0
|
||||
tactic: String
|
||||
deriving Lean.FromJson
|
||||
structure GoalTacticResult where
|
||||
-- The next goal state id. Existence of this field shows success
|
||||
nextStateId?: Option Nat := .none
|
||||
-- If the array is empty, it shows the goals have been fully resolved.
|
||||
structure ProofTacticResult where
|
||||
-- Existence of this field shows success
|
||||
goals?: Option (Array Goal) := .none
|
||||
|
||||
-- Existence of this field shows tactic execution failure
|
||||
-- Next proof state id, if successful
|
||||
nextId?: Option Nat := .none
|
||||
-- Existence of this field shows failure
|
||||
tacticErrors?: Option (Array String) := .none
|
||||
|
||||
-- Existence of this field shows the tactic parsing has failed
|
||||
parseError?: Option String := .none
|
||||
deriving Lean.ToJson
|
||||
|
||||
-- Remove goal states
|
||||
structure GoalDelete where
|
||||
stateIds: List Nat
|
||||
structure ProofPrintTree where
|
||||
treeId: Nat
|
||||
deriving Lean.FromJson
|
||||
structure GoalDeleteResult where
|
||||
structure ProofPrintTreeResult where
|
||||
-- "" if no parents, otherwise "parentId.goalId"
|
||||
parents: Array String
|
||||
deriving Lean.ToJson
|
||||
|
||||
structure GoalPrint where
|
||||
stateId: Nat
|
||||
deriving Lean.FromJson
|
||||
structure GoalPrintResult where
|
||||
-- The root expression
|
||||
root?: Option Expression
|
||||
deriving Lean.ToJson
|
||||
|
||||
-- Diagnostic Options, not available in REPL
|
||||
structure GoalDiag where
|
||||
printContext: Bool := true
|
||||
printValue: Bool := true
|
||||
printNewMVars: Bool := false
|
||||
-- Print all mvars
|
||||
printAll: Bool := false
|
||||
|
||||
|
||||
end Pantograph.Protocol
|
||||
end Pantograph.Commands
|
|
@ -1,204 +0,0 @@
|
|||
import Lean
|
||||
|
||||
import Pantograph.Symbol
|
||||
|
||||
def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
|
||||
{
|
||||
msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false
|
||||
}
|
||||
|
||||
|
||||
namespace Pantograph
|
||||
open Lean
|
||||
|
||||
structure GoalState where
|
||||
savedState : Elab.Tactic.SavedState
|
||||
|
||||
-- The root hole which is the search target
|
||||
root: MVarId
|
||||
-- New metavariables acquired in this state
|
||||
newMVars: SSet MVarId
|
||||
|
||||
-- The id of the goal in the parent
|
||||
parentGoalId: Nat := 0
|
||||
|
||||
abbrev M := Elab.TermElabM
|
||||
|
||||
protected def GoalState.create (expr: Expr): M GoalState := do
|
||||
-- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context.
|
||||
-- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
|
||||
|
||||
--Elab.Term.synthesizeSyntheticMVarsNoPostponing
|
||||
--let expr ← instantiateMVars expr
|
||||
let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous))
|
||||
let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
|
||||
let root := goal.mvarId!
|
||||
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]}
|
||||
return {
|
||||
savedState,
|
||||
root,
|
||||
newMVars := SSet.insert .empty root,
|
||||
}
|
||||
protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals
|
||||
|
||||
protected def GoalState.runM {α: Type} (state: GoalState) (m: Elab.TermElabM α) : M α := do
|
||||
state.savedState.term.restore
|
||||
m
|
||||
|
||||
protected def GoalState.mctx (state: GoalState): MetavarContext :=
|
||||
state.savedState.term.meta.meta.mctx
|
||||
protected def GoalState.env (state: GoalState): Environment :=
|
||||
state.savedState.term.meta.core.env
|
||||
private def GoalState.mvars (state: GoalState): SSet MVarId :=
|
||||
state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
|
||||
|
||||
/-- Inner function for executing tactic on goal state -/
|
||||
def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
|
||||
M (Except (Array String) Elab.Tactic.SavedState):= do
|
||||
let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := do
|
||||
state.restore
|
||||
Elab.Tactic.setGoals [goal]
|
||||
try
|
||||
Elab.Tactic.evalTactic stx
|
||||
if (← getThe Core.State).messages.hasErrors then
|
||||
let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
|
||||
let errors ← (messages.map Message.data).mapM fun md => md.toString
|
||||
return .error errors
|
||||
else
|
||||
return .ok (← MonadBacktrack.saveState)
|
||||
catch exception =>
|
||||
return .error #[← exception.toMessageData.toString]
|
||||
tacticM tactic { elaborator := .anonymous } |>.run' state.tactic
|
||||
|
||||
/-- Response for executing a tactic -/
|
||||
inductive TacticResult where
|
||||
-- Goes to next state
|
||||
| success (state: GoalState)
|
||||
-- Tactic failed with messages
|
||||
| failure (messages: Array String)
|
||||
-- Could not parse tactic
|
||||
| parseError (message: String)
|
||||
-- The goal index is out of bounds
|
||||
| indexError (goalId: Nat)
|
||||
|
||||
/-- Execute tactic on given state -/
|
||||
protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String):
|
||||
M TacticResult := do
|
||||
let goal ← match state.savedState.tactic.goals.get? goalId with
|
||||
| .some goal => pure $ goal
|
||||
| .none => return .indexError goalId
|
||||
let tactic ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `tactic)
|
||||
(input := tactic)
|
||||
(fileName := "<stdin>") with
|
||||
| .ok stx => pure $ stx
|
||||
| .error error => return .parseError error
|
||||
match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
|
||||
| .error errors =>
|
||||
return .failure errors
|
||||
| .ok nextSavedState =>
|
||||
-- Assert that the definition of metavariables are the same
|
||||
let nextMCtx := nextSavedState.term.meta.meta.mctx
|
||||
let prevMCtx := state.savedState.term.meta.meta.mctx
|
||||
-- Generate a list of mvarIds that exist in the parent state; Also test the
|
||||
-- assertion that the types have not changed on any mvars.
|
||||
let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
|
||||
if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
|
||||
assert! prevMVarDecl.type == mvarDecl.type
|
||||
return acc
|
||||
else
|
||||
return acc.insert mvarId
|
||||
) SSet.empty
|
||||
return .success {
|
||||
state with
|
||||
savedState := nextSavedState
|
||||
newMVars,
|
||||
parentGoalId := goalId,
|
||||
}
|
||||
|
||||
protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
|
||||
let goal ← match state.savedState.tactic.goals.get? goalId with
|
||||
| .some goal => pure goal
|
||||
| .none => return .indexError goalId
|
||||
let expr ← match Parser.runParserCategory
|
||||
(env := state.env)
|
||||
(catName := `term)
|
||||
(input := expr)
|
||||
(fileName := "<stdin>") with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
let tacticM: Elab.Tactic.TacticM TacticResult := do
|
||||
state.savedState.restore
|
||||
Elab.Tactic.setGoals [goal]
|
||||
try
|
||||
let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
|
||||
-- Attempt to unify the expression
|
||||
let goalType ← goal.getType
|
||||
let exprType ← Meta.inferType expr
|
||||
if !(← Meta.isDefEq goalType exprType) then
|
||||
return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)]
|
||||
goal.checkNotAssigned `GoalState.tryAssign
|
||||
goal.assign expr
|
||||
if (← getThe Core.State).messages.hasErrors then
|
||||
let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
|
||||
let errors ← (messages.map Message.data).mapM fun md => md.toString
|
||||
return .failure errors
|
||||
else
|
||||
let prevMCtx := state.savedState.term.meta.meta.mctx
|
||||
let nextMCtx ← getMCtx
|
||||
-- Generate a list of mvarIds that exist in the parent state; Also test the
|
||||
-- assertion that the types have not changed on any mvars.
|
||||
let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
|
||||
if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
|
||||
assert! prevMVarDecl.type == mvarDecl.type
|
||||
return acc
|
||||
else
|
||||
return mvarId :: acc
|
||||
) []
|
||||
-- The new goals are the newMVars that lack an assignment
|
||||
Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)))
|
||||
let nextSavedState ← MonadBacktrack.saveState
|
||||
return .success {
|
||||
state with
|
||||
savedState := nextSavedState,
|
||||
newMVars := newMVars.toSSet,
|
||||
parentGoalId := goalId,
|
||||
}
|
||||
catch exception =>
|
||||
return .failure #[← exception.toMessageData.toString]
|
||||
tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
|
||||
|
||||
/-- After finishing one branch of a proof (`graftee`), pick up from the point where the proof was left off (`target`) -/
|
||||
protected def GoalState.continue (target: GoalState) (graftee: GoalState): Except String GoalState :=
|
||||
if target.root != graftee.root then
|
||||
.error s!"Roots of two continued goal states do not match: {target.root.name} != {graftee.root.name}"
|
||||
-- Ensure goals are not dangling
|
||||
else if ¬ (target.goals.all (λ goal => graftee.mvars.contains goal)) then
|
||||
.error s!"Some goals in target are not present in the graftee"
|
||||
else
|
||||
-- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
|
||||
let unassigned := target.goals.filter (λ goal =>
|
||||
let mctx := graftee.mctx
|
||||
¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
|
||||
.ok {
|
||||
savedState := {
|
||||
term := graftee.savedState.term,
|
||||
tactic := { goals := unassigned },
|
||||
},
|
||||
root := target.root,
|
||||
newMVars := graftee.newMVars,
|
||||
}
|
||||
|
||||
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr :=
|
||||
let expr := goalState.mctx.eAssignment.find! goalState.root
|
||||
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
|
||||
if expr.hasMVar then
|
||||
-- Must not assert that the goal state is empty here. We could be in a branch goal.
|
||||
--assert! ¬goalState.goals.isEmpty
|
||||
.none
|
||||
else
|
||||
assert! goalState.goals.isEmpty
|
||||
.some expr
|
||||
|
||||
end Pantograph
|
|
@ -1,149 +0,0 @@
|
|||
|
||||
namespace Pantograph.SemihashMap
|
||||
|
||||
structure Imp (β: Type u) where
|
||||
data: Array (Option β)
|
||||
|
||||
-- Number of elements currently in use
|
||||
size: Nat
|
||||
|
||||
-- Next index that has never been touched
|
||||
allocFront: Nat
|
||||
|
||||
-- Deallocated indices
|
||||
deallocs: Array Nat
|
||||
|
||||
-- Number of valid entries in `deallocs` array
|
||||
lastDealloc: Nat
|
||||
|
||||
namespace Imp
|
||||
|
||||
structure WF (m: Imp β): Prop where
|
||||
capacity: m.data.size = m.deallocs.size
|
||||
front_dealloc: ∀ i: Fin m.deallocs.size, (i < m.allocFront) → (m.deallocs.get i) < m.allocFront
|
||||
front_data: ∀ i: Fin m.data.size, (i ≥ m.allocFront) → (m.data.get i).isNone
|
||||
|
||||
def empty (capacity := 16): Imp β :=
|
||||
{
|
||||
data := mkArray capacity .none,
|
||||
size := 0,
|
||||
allocFront := 0,
|
||||
deallocs := mkArray capacity 0,
|
||||
lastDealloc := 0,
|
||||
}
|
||||
|
||||
private theorem list_get_replicate (x: α) (i: Fin (List.replicate n x).length):
|
||||
List.get (List.replicate n x) i = x := by
|
||||
sorry
|
||||
|
||||
theorem empty_wf : WF (empty n: Imp β) := by
|
||||
unfold empty
|
||||
apply WF.mk
|
||||
case capacity =>
|
||||
conv =>
|
||||
lhs
|
||||
congr
|
||||
simp
|
||||
conv =>
|
||||
rhs
|
||||
congr
|
||||
simp
|
||||
simp
|
||||
case front_dealloc =>
|
||||
simp_all
|
||||
intro i
|
||||
intro a
|
||||
contradiction
|
||||
case front_data =>
|
||||
simp_all
|
||||
intro i
|
||||
unfold Imp.data at i
|
||||
simp at i
|
||||
conv =>
|
||||
lhs
|
||||
unfold Array.get
|
||||
unfold mkArray
|
||||
simp [List.replicate]
|
||||
rewrite [list_get_replicate]
|
||||
|
||||
-- FIXME: Merge this with the well-formed versions below so proof and code can
|
||||
-- mesh seamlessly.
|
||||
@[inline] def insert (map: Imp β) (v: β): (Imp β × Nat) :=
|
||||
match map.lastDealloc with
|
||||
| 0 => -- Capacity is full, buffer expansion is required
|
||||
if map.size == map.data.size then
|
||||
let nextIndex := map.data.size
|
||||
let extendCapacity := map.size
|
||||
let result: Imp β := {
|
||||
data := (map.data.append #[Option.some v]).append (mkArray extendCapacity .none),
|
||||
size := map.size + 1,
|
||||
allocFront := map.size + 1,
|
||||
deallocs := mkArray (map.data.size + 1 + extendCapacity) 0,
|
||||
lastDealloc := 0,
|
||||
}
|
||||
(result, nextIndex)
|
||||
else
|
||||
let nextIndex := map.size
|
||||
let result: Imp β := {
|
||||
map
|
||||
with
|
||||
data := map.data.set ⟨nextIndex, sorry⟩ (Option.some v),
|
||||
size := map.size + 1,
|
||||
allocFront := map.allocFront + 1,
|
||||
}
|
||||
(result, nextIndex)
|
||||
| (.succ k) => -- Allocation list has space
|
||||
let nextIndex := map.deallocs.get! k
|
||||
let result: Imp β := {
|
||||
map with
|
||||
data := map.data.set ⟨nextIndex, sorry⟩ (Option.some v),
|
||||
size := map.size + 1,
|
||||
lastDealloc := map.lastDealloc - 1
|
||||
}
|
||||
(result, nextIndex)
|
||||
|
||||
@[inline] def remove (map: Imp β) (index: Fin (map.size)): Imp β :=
|
||||
have h: index.val < map.data.size := by sorry
|
||||
match map.data.get ⟨index.val, h⟩ with
|
||||
| .none => map
|
||||
| .some _ =>
|
||||
{
|
||||
map with
|
||||
data := map.data.set ⟨index, sorry⟩ .none,
|
||||
size := map.size - 1,
|
||||
deallocs := map.deallocs.set ⟨map.lastDealloc, sorry⟩ index,
|
||||
lastDealloc := map.lastDealloc + 1,
|
||||
}
|
||||
|
||||
/-- Retrieval is efficient -/
|
||||
@[inline] def get? (map: Imp β) (index: Fin (map.size)): Option β :=
|
||||
have h: index.val < map.data.size := by sorry
|
||||
map.data.get ⟨index.val, h⟩
|
||||
@[inline] def capacity (map: Imp β): Nat := map.data.size
|
||||
|
||||
end Imp
|
||||
|
||||
|
||||
/--
|
||||
This is like a hashmap but you cannot control the keys.
|
||||
-/
|
||||
def _root_.Pantograph.SemihashMap β := {m: Imp β // m.WF}
|
||||
|
||||
@[inline] def empty (capacity := 16): SemihashMap β :=
|
||||
⟨ Imp.empty capacity, Imp.empty_wf ⟩
|
||||
@[inline] def insert (map: SemihashMap β) (v: β): (SemihashMap β × Nat) :=
|
||||
let ⟨imp, pre⟩ := map
|
||||
let ⟨result, id⟩ := imp.insert v
|
||||
( ⟨ result, sorry ⟩, id)
|
||||
@[inline] def remove (map: SemihashMap β) (index: Nat): SemihashMap β :=
|
||||
let ⟨imp, pre⟩ := map
|
||||
let result := imp.remove ⟨index, sorry⟩
|
||||
⟨ result, sorry ⟩
|
||||
@[inline] def get? (map: SemihashMap β) (index: Nat): Option β :=
|
||||
let ⟨imp, _⟩ := map
|
||||
imp.get? ⟨index, sorry⟩
|
||||
@[inline] def size (map: SemihashMap β): Nat :=
|
||||
let ⟨imp, _⟩ := map
|
||||
imp.size
|
||||
|
||||
end Pantograph.SemihashMap
|
|
@ -3,8 +3,7 @@ All serialisation functions
|
|||
-/
|
||||
import Lean
|
||||
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Commands
|
||||
|
||||
namespace Pantograph
|
||||
open Lean
|
||||
|
@ -29,28 +28,34 @@ def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
|
|||
def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
|
||||
try
|
||||
let expr ← Elab.Term.elabType syn
|
||||
-- Immediately synthesise all metavariables if we need to leave the elaboration context.
|
||||
-- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
|
||||
--Elab.Term.synthesizeSyntheticMVarsNoPostponing
|
||||
let expr ← instantiateMVars expr
|
||||
return .ok expr
|
||||
catch ex => return .error (← ex.toMessageData.toString)
|
||||
def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
|
||||
try
|
||||
let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none)
|
||||
-- Immediately synthesise all metavariables if we need to leave the elaboration context.
|
||||
-- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
|
||||
--Elab.Term.synthesizeSyntheticMVarsNoPostponing
|
||||
let expr ← instantiateMVars expr
|
||||
return .ok expr
|
||||
catch ex => return .error (← ex.toMessageData.toString)
|
||||
|
||||
|
||||
--- Output Functions ---
|
||||
|
||||
def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := do
|
||||
def type_expr_to_bound (expr: Expr): MetaM Commands.BoundExpression := do
|
||||
Meta.forallTelescope expr fun arr body => do
|
||||
let binders ← arr.mapM fun fvar => do
|
||||
return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
|
||||
return { binders, target := toString (← Meta.ppExpr body) }
|
||||
|
||||
private def name_to_ast (name: Lean.Name) (sanitize: Bool := true): String := match name with
|
||||
| .anonymous => ":anon"
|
||||
| .num n i => match sanitize with
|
||||
| false => s!"{toString n} {i}"
|
||||
| true => ":anon"
|
||||
private def name_to_ast: Lean.Name → String
|
||||
| .anonymous
|
||||
| .num _ _ => ":anon"
|
||||
| n@(.str _ _) => toString n
|
||||
|
||||
private def level_depth: Level → Nat
|
||||
|
@ -103,91 +108,89 @@ def serialize_sort_level_ast (level: Level): String :=
|
|||
/--
|
||||
Completely serializes an expression tree. Json not used due to compactness
|
||||
-/
|
||||
def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
|
||||
self expr
|
||||
def serialize_expression_ast (expr: Expr): MetaM String := do
|
||||
match expr with
|
||||
| .bvar deBruijnIndex =>
|
||||
-- This is very common so the index alone is shown. Literals are handled below.
|
||||
-- The raw de Bruijn index should never appear in an unbound setting. In
|
||||
-- Lean these are handled using a `#` prefix.
|
||||
return s!"{deBruijnIndex}"
|
||||
| .fvar fvarId =>
|
||||
let name := (← fvarId.getDecl).userName
|
||||
return s!"(:fv {name})"
|
||||
| .mvar mvarId =>
|
||||
let name := name_to_ast mvarId.name
|
||||
return s!"(:mv {name})"
|
||||
| .sort level =>
|
||||
let level := serialize_sort_level_ast level
|
||||
return s!"(:sort {level})"
|
||||
| .const declName _ =>
|
||||
-- The universe level of the const expression is elided since it should be
|
||||
-- inferrable from surrounding expression
|
||||
return s!"(:c {declName})"
|
||||
| .app fn arg =>
|
||||
let fn' ← serialize_expression_ast fn
|
||||
let arg' ← serialize_expression_ast arg
|
||||
return s!"({fn'} {arg'})"
|
||||
| .lam binderName binderType body binderInfo =>
|
||||
let binderName' := name_to_ast binderName
|
||||
let binderType' ← serialize_expression_ast binderType
|
||||
let body' ← serialize_expression_ast body
|
||||
let binderInfo' := binder_info_to_ast binderInfo
|
||||
return s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
|
||||
| .forallE binderName binderType body binderInfo =>
|
||||
let binderName' := name_to_ast binderName
|
||||
let binderType' ← serialize_expression_ast binderType
|
||||
let body' ← serialize_expression_ast body
|
||||
let binderInfo' := binder_info_to_ast binderInfo
|
||||
return s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
|
||||
| .letE name type value body _ =>
|
||||
-- Dependent boolean flag diacarded
|
||||
let name' := name_to_ast name
|
||||
let type' ← serialize_expression_ast type
|
||||
let value' ← serialize_expression_ast value
|
||||
let body' ← serialize_expression_ast body
|
||||
return s!"(:let {name'} {type'} {value'} {body'})"
|
||||
| .lit v =>
|
||||
-- To not burden the downstream parser who needs to handle this, the literal
|
||||
-- is wrapped in a :lit sexp.
|
||||
let v' := match v with
|
||||
| .natVal val => toString val
|
||||
| .strVal val => s!"\"{val}\""
|
||||
return s!"(:lit {v'})"
|
||||
| .mdata _ expr =>
|
||||
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
|
||||
-- It may become necessary to incorporate the metadata.
|
||||
return (← serialize_expression_ast expr)
|
||||
| .proj typeName idx struct =>
|
||||
let struct' ← serialize_expression_ast struct
|
||||
return s!"(:proj {typeName} {idx} {struct'})"
|
||||
|
||||
where
|
||||
self (e: Expr): String :=
|
||||
match e with
|
||||
| .bvar deBruijnIndex =>
|
||||
-- This is very common so the index alone is shown. Literals are handled below.
|
||||
-- The raw de Bruijn index should never appear in an unbound setting. In
|
||||
-- Lean these are handled using a `#` prefix.
|
||||
s!"{deBruijnIndex}"
|
||||
| .fvar fvarId =>
|
||||
let name := of_name fvarId.name
|
||||
s!"(:fv {name})"
|
||||
| .mvar mvarId =>
|
||||
let name := of_name mvarId.name
|
||||
s!"(:mv {name})"
|
||||
| .sort level =>
|
||||
let level := serialize_sort_level_ast level
|
||||
s!"(:sort {level})"
|
||||
| .const declName _ =>
|
||||
-- The universe level of the const expression is elided since it should be
|
||||
-- inferrable from surrounding expression
|
||||
s!"(:c {declName})"
|
||||
| .app fn arg =>
|
||||
let fn' := self fn
|
||||
let arg' := self arg
|
||||
s!"({fn'} {arg'})"
|
||||
| .lam binderName binderType body binderInfo =>
|
||||
let binderName' := of_name binderName
|
||||
let binderType' := self binderType
|
||||
let body' := self body
|
||||
let binderInfo' := binder_info_to_ast binderInfo
|
||||
s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
|
||||
| .forallE binderName binderType body binderInfo =>
|
||||
let binderName' := of_name binderName
|
||||
let binderType' := self binderType
|
||||
let body' := self body
|
||||
let binderInfo' := binder_info_to_ast binderInfo
|
||||
s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
|
||||
| .letE name type value body _ =>
|
||||
-- Dependent boolean flag diacarded
|
||||
let name' := name_to_ast name
|
||||
let type' := self type
|
||||
let value' := self value
|
||||
let body' := self body
|
||||
s!"(:let {name'} {type'} {value'} {body'})"
|
||||
| .lit v =>
|
||||
-- To not burden the downstream parser who needs to handle this, the literal
|
||||
-- is wrapped in a :lit sexp.
|
||||
let v' := match v with
|
||||
| .natVal val => toString val
|
||||
| .strVal val => s!"\"{val}\""
|
||||
s!"(:lit {v'})"
|
||||
| .mdata _ inner =>
|
||||
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
|
||||
-- It may become necessary to incorporate the metadata.
|
||||
self inner
|
||||
| .proj typeName idx struct =>
|
||||
let struct' := self struct
|
||||
s!"(:proj {typeName} {idx} {struct'})"
|
||||
-- Elides all unhygenic names
|
||||
binder_info_to_ast : Lean.BinderInfo → String
|
||||
| .default => ""
|
||||
| .implicit => " :implicit"
|
||||
| .strictImplicit => " :strictImplicit"
|
||||
| .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: Commands.Options) (e: Expr): MetaM Commands.Expression := do
|
||||
let pp := toString (← Meta.ppExpr e)
|
||||
let pp?: Option String := match options.printExprPretty with
|
||||
| true => .some pp
|
||||
| false => .none
|
||||
let sexp: String := serialize_expression_ast e
|
||||
| true => .some pp
|
||||
| false => .none
|
||||
let sexp: String := (← serialize_expression_ast e)
|
||||
let sexp?: Option String := match options.printExprAST with
|
||||
| true => .some sexp
|
||||
| false => .none
|
||||
| true => .some sexp
|
||||
| false => .none
|
||||
return {
|
||||
pp?,
|
||||
sexp?
|
||||
}
|
||||
|
||||
/-- Adapted from ppGoal -/
|
||||
def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
|
||||
: MetaM Protocol.Goal := do
|
||||
def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
|
||||
: MetaM Commands.Goal := do
|
||||
-- Options for printing; See Meta.ppGoal for details
|
||||
let showLetValues := true
|
||||
let ppAuxDecls := options.printAuxDecls
|
||||
|
@ -195,32 +198,29 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe
|
|||
let lctx := mvarDecl.lctx
|
||||
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
|
||||
Meta.withLCtx lctx mvarDecl.localInstances do
|
||||
let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
|
||||
let ppVarNameOnly (localDecl: LocalDecl): MetaM Commands.Variable := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName _ _ _ =>
|
||||
let userName := userName.simpMacroScopes
|
||||
| .cdecl _ _ varName _ _ _ =>
|
||||
let varName := varName.simpMacroScopes
|
||||
return {
|
||||
name := of_name fvarId.name,
|
||||
userName:= of_name userName.simpMacroScopes,
|
||||
name := toString varName,
|
||||
}
|
||||
| .ldecl _ fvarId userName _ _ _ _ => do
|
||||
| .ldecl _ _ varName _ _ _ _ => do
|
||||
return {
|
||||
name := of_name fvarId.name,
|
||||
userName := toString userName.simpMacroScopes,
|
||||
name := toString varName,
|
||||
}
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Commands.Variable := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName type _ _ =>
|
||||
let userName := userName.simpMacroScopes
|
||||
| .cdecl _ _ varName type _ _ =>
|
||||
let varName := varName.simpMacroScopes
|
||||
let type ← instantiateMVars type
|
||||
return {
|
||||
name := of_name fvarId.name,
|
||||
userName:= of_name userName,
|
||||
isInaccessible? := .some userName.isInaccessibleUserName
|
||||
name := toString varName,
|
||||
isInaccessible? := .some varName.isInaccessibleUserName
|
||||
type? := .some (← serialize_expression options type)
|
||||
}
|
||||
| .ldecl _ fvarId userName type val _ _ => do
|
||||
let userName := userName.simpMacroScopes
|
||||
| .ldecl _ _ varName type val _ _ => do
|
||||
let varName := varName.simpMacroScopes
|
||||
let type ← instantiateMVars type
|
||||
let value? ← if showLetValues then
|
||||
let val ← instantiateMVars val
|
||||
|
@ -228,9 +228,8 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe
|
|||
else
|
||||
pure $ .none
|
||||
return {
|
||||
name := of_name fvarId.name,
|
||||
userName:= of_name userName,
|
||||
isInaccessible? := .some userName.isInaccessibleUserName
|
||||
name := toString varName,
|
||||
isInaccessible? := .some varName.isInaccessibleUserName
|
||||
type? := .some (← serialize_expression options type)
|
||||
value? := value?
|
||||
}
|
||||
|
@ -240,79 +239,21 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe
|
|||
if skip then
|
||||
return acc
|
||||
else
|
||||
let nameOnly := options.noRepeat && (parentDecl?.map
|
||||
let nameOnly := options.proofVariableDelta && (parentDecl?.map
|
||||
(λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
|
||||
let var ← match nameOnly with
|
||||
| true => ppVarNameOnly localDecl
|
||||
| false => ppVar localDecl
|
||||
return var::acc
|
||||
return {
|
||||
caseName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName),
|
||||
isConversion := isLHSGoal? mvarDecl.type |>.isSome,
|
||||
caseName? := match mvarDecl.userName with
|
||||
| Name.anonymous => .none
|
||||
| name => .some <| toString name,
|
||||
isConversion := "| " == (Meta.getGoalPrefix mvarDecl)
|
||||
target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
|
||||
vars := vars.reverse.toArray
|
||||
}
|
||||
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
|
||||
let goals := state.goals.toArray
|
||||
state.savedState.term.meta.restore
|
||||
let parentDecl? := parent.bind (λ parentState =>
|
||||
let parentGoal := parentState.goals.get! state.parentGoalId
|
||||
parentState.mctx.findDecl? parentGoal)
|
||||
goals.mapM fun goal => do
|
||||
match state.mctx.findDecl? goal with
|
||||
| .some mvarDecl =>
|
||||
let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?)
|
||||
pure serializedGoal
|
||||
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
|
||||
|
||||
/-- Print the metavariables in a readable format -/
|
||||
protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
|
||||
let savedState := goalState.savedState
|
||||
savedState.term.meta.restore
|
||||
let goals := savedState.tactic.goals
|
||||
let mctx ← getMCtx
|
||||
let root := goalState.root
|
||||
-- Print the root
|
||||
match mctx.decls.find? root with
|
||||
| .some decl => printMVar ">" root decl
|
||||
| .none => IO.println s!">{root.name}: ??"
|
||||
goals.forM (fun mvarId => do
|
||||
if mvarId != root then
|
||||
match mctx.decls.find? mvarId with
|
||||
| .some decl => printMVar "⊢" mvarId decl
|
||||
| .none => IO.println s!"⊢{mvarId.name}: ??"
|
||||
)
|
||||
let goals := goals.toSSet
|
||||
mctx.decls.forM (fun mvarId decl => do
|
||||
if goals.contains mvarId || mvarId == root then
|
||||
pure ()
|
||||
-- Always print the root goal
|
||||
else if mvarId == goalState.root then
|
||||
printMVar (pref := ">") mvarId decl
|
||||
-- Print the remainig ones that users don't see in Lean
|
||||
else if options.printAll then
|
||||
let pref := if goalState.newMVars.contains mvarId then "~" else " "
|
||||
printMVar pref mvarId decl
|
||||
else
|
||||
pure ()
|
||||
--IO.println s!" {mvarId.name}{userNameToString decl.userName}"
|
||||
)
|
||||
where
|
||||
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
|
||||
if options.printContext then
|
||||
decl.lctx.fvarIdToDecl.forM printFVar
|
||||
let type_sexp := serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
|
||||
IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
|
||||
if options.printValue then
|
||||
if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
|
||||
IO.println s!" = {← Meta.ppExpr value}"
|
||||
printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do
|
||||
IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
|
||||
userNameToString : Name → String
|
||||
| .anonymous => ""
|
||||
| other => s!"[{other}]"
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -1,8 +1,10 @@
|
|||
/-
|
||||
- Manages the visibility status of symbols
|
||||
-/
|
||||
import Lean.Declaration
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
/-- Converts a symbol of the form `aa.bb.cc` to a name -/
|
||||
def str_to_name (s: String): Lean.Name :=
|
||||
(s.splitOn ".").foldl Lean.Name.str Lean.Name.anonymous
|
||||
|
|
@ -0,0 +1,121 @@
|
|||
import Lean
|
||||
|
||||
import Pantograph.Symbols
|
||||
import Pantograph.Serial
|
||||
|
||||
/-
|
||||
The proof state manipulation system
|
||||
|
||||
A proof state is launched by providing
|
||||
1. Environment: `Environment`
|
||||
2. Expression: `Expr`
|
||||
The expression becomes the first meta variable in the saved tactic state
|
||||
`Elab.Tactic.SavedState`.
|
||||
From this point on, any proof which extends
|
||||
`Elab.Term.Context` and
|
||||
-/
|
||||
|
||||
def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
|
||||
{
|
||||
msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false
|
||||
}
|
||||
|
||||
|
||||
namespace Pantograph
|
||||
open Lean
|
||||
|
||||
structure ProofState where
|
||||
goals : List MVarId
|
||||
savedState : Elab.Tactic.SavedState
|
||||
parent : Option Nat := none
|
||||
parentGoalId : Nat := 0
|
||||
structure ProofTree where
|
||||
-- Set of proof states
|
||||
states : Array ProofState := #[]
|
||||
|
||||
abbrev M := Elab.TermElabM
|
||||
|
||||
def ProofTree.create (expr: Expr): M ProofTree := do
|
||||
let expr ← instantiateMVars expr
|
||||
let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic))
|
||||
let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
|
||||
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]}
|
||||
return {
|
||||
states := #[{
|
||||
savedState := savedState,
|
||||
goals := [goal.mvarId!]
|
||||
}]
|
||||
}
|
||||
|
||||
-- Print the tree structures in readable form
|
||||
def ProofTree.structure_array (tree: ProofTree): Array String :=
|
||||
tree.states.map λ state => match state.parent with
|
||||
| .none => ""
|
||||
| .some parent => s!"{parent}.{state.parentGoalId}"
|
||||
|
||||
def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: String) :
|
||||
M (Except (Array String) (Elab.Tactic.SavedState × List MVarId)):= do
|
||||
let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) (Elab.Tactic.SavedState × List MVarId)) := do
|
||||
state.restore
|
||||
Elab.Tactic.setGoals [goal]
|
||||
try
|
||||
Elab.Tactic.evalTactic stx
|
||||
if (← getThe Core.State).messages.hasErrors then
|
||||
let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
|
||||
let errors ← (messages.map Message.data).mapM fun md => md.toString
|
||||
return .error errors
|
||||
else
|
||||
return .ok (← MonadBacktrack.saveState, ← Elab.Tactic.getUnsolvedGoals)
|
||||
catch exception =>
|
||||
return .error #[← exception.toMessageData.toString]
|
||||
match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `tactic)
|
||||
(input := tactic)
|
||||
(fileName := "<stdin>") with
|
||||
| Except.error err => return .error #[err]
|
||||
| Except.ok stx => tacticM stx { elaborator := .anonymous } |>.run' state.tactic
|
||||
|
||||
/-- Response for executing a tactic -/
|
||||
inductive TacticResult where
|
||||
-- Invalid id
|
||||
| invalid (message: String): TacticResult
|
||||
-- Goes to next state
|
||||
| success (nextId?: Option Nat) (goals: Array Commands.Goal)
|
||||
-- Fails with messages
|
||||
| failure (messages: Array String)
|
||||
|
||||
/-- Execute tactic on given state -/
|
||||
def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String):
|
||||
Commands.OptionsT StateRefT ProofTree M TacticResult := do
|
||||
let options ← read
|
||||
let tree ← get
|
||||
match tree.states.get? stateId with
|
||||
| .none => return .invalid s!"Invalid state id {stateId}"
|
||||
| .some state =>
|
||||
match state.goals.get? goalId with
|
||||
| .none => return .invalid s!"Invalid goal id {goalId}"
|
||||
| .some goal =>
|
||||
match (← execute_tactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
|
||||
| .error errors =>
|
||||
return .failure errors
|
||||
| .ok (nextState, nextGoals) =>
|
||||
let nextId := tree.states.size
|
||||
if nextGoals.isEmpty then
|
||||
return .success .none #[]
|
||||
else
|
||||
let proofState: ProofState := {
|
||||
savedState := nextState,
|
||||
goals := nextGoals,
|
||||
parent := stateId,
|
||||
parentGoalId := goalId
|
||||
}
|
||||
modify fun s => { s with states := s.states.push proofState }
|
||||
let parentDecl? := (← MonadMCtx.getMCtx).findDecl? goal
|
||||
let goals ← nextGoals.mapM fun mvarId => do
|
||||
match (← MonadMCtx.getMCtx).findDecl? mvarId with
|
||||
| .some mvarDecl => serialize_goal options mvarDecl (parentDecl? := parentDecl?)
|
||||
| .none => throwError mvarId
|
||||
return .success (.some nextId) goals.toArray
|
||||
|
||||
end Pantograph
|
|
@ -1,5 +1,5 @@
|
|||
namespace Pantograph
|
||||
|
||||
def version := "0.2.6"
|
||||
def version := "0.2.3"
|
||||
|
||||
end Pantograph
|
||||
|
|
43
README.md
43
README.md
|
@ -6,11 +6,11 @@ An interaction system for Lean 4.
|
|||
|
||||
## Installation
|
||||
|
||||
Install `elan` and `lake`. Execute
|
||||
Install `elan` and `lean4`. Then, execute
|
||||
``` sh
|
||||
make build/bin/pantograph
|
||||
lake build
|
||||
```
|
||||
setup the `LEAN_PATH` environment variable so it contains the library path of lean libraries. The libraries must be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
|
||||
Then, setup the `LEAN_PATH` environment variable so it contains the library path of lean libraries. The libraries must be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
|
||||
``` sh
|
||||
LIB="../lib"
|
||||
LIB_MATHLIB="$LIB/mathlib4/lake-packages"
|
||||
|
@ -18,12 +18,12 @@ export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATH
|
|||
|
||||
LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
|
||||
```
|
||||
The provided `flake.nix` has a develop environment with Lean already setup.
|
||||
Note that `lean-toolchain` must be present in the `$PWD` in order to run Pantograph! This is because Pantograph taps into Lean's internals.
|
||||
|
||||
## Usage
|
||||
|
||||
``` sh
|
||||
pantograph MODULES|LEAN_OPTIONS
|
||||
build/bin/pantograph MODULES|LEAN_OPTIONS
|
||||
```
|
||||
|
||||
The REPL loop accepts commands as single-line JSON inputs and outputs either an
|
||||
|
@ -36,30 +36,29 @@ command { ... }
|
|||
The list of available commands can be found in `Pantograph/Commands.lean` and below. An
|
||||
empty command aborts the REPL.
|
||||
|
||||
The `pantograph` executable must be run with a list of modules to import. It can
|
||||
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)
|
||||
```
|
||||
$ pantograph Init
|
||||
$ build/bin/Pantograph Init
|
||||
lib.catalog
|
||||
lib.inspect {"name": "Nat.le_add_left"}
|
||||
```
|
||||
Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
|
||||
```
|
||||
$ pantograph Mathlib.Analysis.Seminorm
|
||||
$ lake env build/bin/Pantograph Mathlib.Analysis.Seminorm
|
||||
lib.catalog
|
||||
```
|
||||
Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
|
||||
Example proving a theorem: (alternatively use `proof.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
|
||||
```
|
||||
$ pantograph Init
|
||||
goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
|
||||
goal.tactic {"goalId": 0, "tactic": "intro n m"}
|
||||
goal.tactic {"goalId": 1, "tactic": "assumption"}
|
||||
goal.delete {"goalIds": [0]}
|
||||
stat {}
|
||||
goal.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"}
|
||||
stat
|
||||
$ env build/bin/Pantograph Init
|
||||
proof.start {"expr": "∀ (n m : Nat), n + m = m + n"}
|
||||
proof.tactic {"treeId": 0, "stateId": 0, "goalId": 0, "tactic": "intro n m"}
|
||||
proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "assumption"}
|
||||
proof.printTree {"treeId": 0}
|
||||
proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"}
|
||||
proof.printTree {"treeId": 0}
|
||||
```
|
||||
where the application of `assumption` should lead to a failure.
|
||||
|
||||
|
@ -75,11 +74,9 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va
|
|||
- `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/Commands.lean`
|
||||
- `options.print`: Display the current set of options
|
||||
- `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
|
||||
- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr": <expr>]}`: Execute a tactic string on a given goal
|
||||
- `goal.remove {"stateIds": [<id>]}"`: Remove a bunch of stored goals.
|
||||
- `goal.print {"stateId": <id>}"`: Print a goal state
|
||||
- `stat`: Display resource usage
|
||||
- `proof.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new proof state from a given expression or symbol
|
||||
- `proof.tactic {"treeId": <id>, "stateId": <id>, "goalId": <id>, "tactic": string}`: Execute a tactic on a given proof state
|
||||
- `proof.printTree {"treeId": <id>}`: Print the topological structure of a proof tree
|
||||
|
||||
## Errors
|
||||
|
||||
|
@ -107,5 +104,5 @@ ulimit -s unlimited
|
|||
|
||||
The tests are based on `LSpec`. To run tests,
|
||||
``` sh
|
||||
make test
|
||||
test/all.sh
|
||||
```
|
||||
|
|
|
@ -1,19 +0,0 @@
|
|||
import Pantograph.Protocol
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
namespace Protocol
|
||||
/-- Set internal names to "" -/
|
||||
def Goal.devolatilize (goal: Goal): Goal :=
|
||||
{
|
||||
goal with
|
||||
vars := goal.vars.map removeInternalAux,
|
||||
}
|
||||
where removeInternalAux (v: Variable): Variable :=
|
||||
{
|
||||
v with
|
||||
name := ""
|
||||
}
|
||||
end Protocol
|
||||
|
||||
end Pantograph
|
101
Test/Holes.lean
101
Test/Holes.lean
|
@ -1,101 +0,0 @@
|
|||
import LSpec
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Serial
|
||||
|
||||
namespace Pantograph.Test.Holes
|
||||
open Pantograph
|
||||
open Lean
|
||||
|
||||
abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M)
|
||||
|
||||
deriving instance DecidableEq, Repr for Commands.Expression
|
||||
deriving instance DecidableEq, Repr for Commands.Variable
|
||||
deriving instance DecidableEq, Repr for Commands.Goal
|
||||
|
||||
def add_test (test: LSpec.TestSeq): TestM Unit := do
|
||||
set $ (← get) ++ test
|
||||
|
||||
def start_goal (hole: String): TestM (Option GoalState) := do
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
let syn? := syntax_from_str env hole
|
||||
add_test $ LSpec.check s!"Parsing {hole}" (syn?.isOk)
|
||||
match syn? with
|
||||
| .error error =>
|
||||
IO.println error
|
||||
return Option.none
|
||||
| .ok syn =>
|
||||
let expr? ← syntax_to_expr syn
|
||||
add_test $ LSpec.check s!"Elaborating" expr?.isOk
|
||||
match expr? with
|
||||
| .error error =>
|
||||
IO.println error
|
||||
return Option.none
|
||||
| .ok expr =>
|
||||
let goal ← GoalState.create (expr := expr)
|
||||
return Option.some goal
|
||||
|
||||
def assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false
|
||||
|
||||
def build_goal (nameType: List (String × String)) (target: String): Commands.Goal :=
|
||||
{
|
||||
target := { pp? := .some target},
|
||||
vars := (nameType.map fun x => ({
|
||||
name := x.fst,
|
||||
type? := .some { pp? := .some x.snd },
|
||||
isInaccessible? := .some false
|
||||
})).toArray
|
||||
}
|
||||
-- Like `build_goal` but allow certain variables to be elided.
|
||||
def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal :=
|
||||
{
|
||||
target := { pp? := .some target},
|
||||
vars := (nameType.map fun x => ({
|
||||
name := x.fst,
|
||||
type? := x.snd.map (λ type => { pp? := type }),
|
||||
isInaccessible? := x.snd.map (λ _ => false)
|
||||
})).toArray
|
||||
}
|
||||
|
||||
def construct_sigma: TestM Unit := do
|
||||
let goal? ← start_goal "∀ (n m: Nat), n + m = m + n"
|
||||
add_test $ LSpec.check "Start goal" goal?.isSome
|
||||
if let .some goal := goal? then
|
||||
return ()
|
||||
|
||||
|
||||
def proof_runner (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 := str_to_name "Aniva",
|
||||
openDecls := [], -- No 'open' directives needed
|
||||
fileName := "<Pantograph>",
|
||||
fileMap := { source := "", positions := #[0], lines := #[1] }
|
||||
}
|
||||
let metaM := termElabM.run' (ctx := {
|
||||
declName? := some "_pantograph",
|
||||
errToSorry := false
|
||||
})
|
||||
let coreM := metaM.run'
|
||||
match ← (coreM.run' coreContext { env := env }).toBaseIO with
|
||||
| .error exception =>
|
||||
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
|
||||
| .ok (_, a) =>
|
||||
return a
|
||||
|
||||
def suite: IO LSpec.TestSeq := do
|
||||
let env: Lean.Environment ← Lean.importModules
|
||||
(imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
|
||||
(opts := {})
|
||||
(trustLevel := 1)
|
||||
let tests := [
|
||||
("Σ'", construct_sigma)
|
||||
]
|
||||
let tests ← tests.foldlM (fun acc tests => do
|
||||
let (name, tests) := tests
|
||||
let tests ← proof_runner env tests
|
||||
return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
|
||||
|
||||
return LSpec.group "Holes" tests
|
||||
|
||||
end Pantograph.Test.Holes
|
|
@ -2,7 +2,7 @@
|
|||
-/
|
||||
import LSpec
|
||||
import Pantograph
|
||||
namespace Pantograph.Test.Integration
|
||||
namespace Pantograph.Test
|
||||
open Pantograph
|
||||
|
||||
def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json))
|
||||
|
@ -15,7 +15,7 @@ def subroutine_step (cmd: String) (payload: List (String × Lean.Json))
|
|||
def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do
|
||||
-- Setup the environment for execution
|
||||
let env ← Lean.importModules
|
||||
(imports := #[{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }])
|
||||
(imports := [{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }])
|
||||
(opts := {})
|
||||
(trustLevel := 1)
|
||||
let context: Context := {
|
||||
|
@ -47,26 +47,26 @@ def test_option_modify : IO LSpec.TestSeq :=
|
|||
let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n"
|
||||
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 := {}
|
||||
let options: Commands.Options := {}
|
||||
subroutine_runner [
|
||||
subroutine_step "lib.inspect"
|
||||
[("name", .str "Nat.add_one")]
|
||||
(Lean.toJson ({
|
||||
type := { pp? }, module? }:
|
||||
Protocol.LibInspectResult)),
|
||||
Commands.LibInspectResult)),
|
||||
subroutine_step "options.set"
|
||||
[("printExprAST", .bool true)]
|
||||
(Lean.toJson ({ }:
|
||||
Protocol.OptionsSetResult)),
|
||||
Commands.OptionsSetResult)),
|
||||
subroutine_step "lib.inspect"
|
||||
[("name", .str "Nat.add_one")]
|
||||
(Lean.toJson ({
|
||||
type := { pp?, sexp? }, module? }:
|
||||
Protocol.LibInspectResult)),
|
||||
Commands.LibInspectResult)),
|
||||
subroutine_step "options.print"
|
||||
[]
|
||||
(Lean.toJson ({ options with printExprAST := true }:
|
||||
Protocol.OptionsPrintResult))
|
||||
Commands.OptionsPrintResult))
|
||||
]
|
||||
def test_malformed_command : IO LSpec.TestSeq :=
|
||||
let invalid := "invalid"
|
||||
|
@ -75,38 +75,19 @@ def test_malformed_command : IO LSpec.TestSeq :=
|
|||
[("name", .str "Nat.add_one")]
|
||||
(Lean.toJson ({
|
||||
error := "command", desc := s!"Unknown command {invalid}"}:
|
||||
Protocol.InteractionError)),
|
||||
Commands.InteractionError)),
|
||||
subroutine_named_step "JSON Deserialization" "expr.echo"
|
||||
[(invalid, .str "Random garbage data")]
|
||||
(Lean.toJson ({
|
||||
error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}:
|
||||
Protocol.InteractionError))
|
||||
]
|
||||
def test_tactic : IO LSpec.TestSeq :=
|
||||
let goal: Protocol.Goal := {
|
||||
target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
|
||||
vars := #[{ name := "_uniq 9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
|
||||
}
|
||||
subroutine_runner [
|
||||
subroutine_step "goal.start"
|
||||
[("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
|
||||
(Lean.toJson ({stateId := 0}:
|
||||
Protocol.GoalStartResult)),
|
||||
subroutine_step "goal.tactic"
|
||||
[("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
|
||||
(Lean.toJson ({
|
||||
nextStateId? := .some 1,
|
||||
goals? := #[goal],
|
||||
}:
|
||||
Protocol.GoalTacticResult))
|
||||
error := "command", desc := s!"Unable to parse json: Pantograph.Commands.ExprEcho.expr: String expected"}:
|
||||
Commands.InteractionError))
|
||||
]
|
||||
|
||||
def suite: IO LSpec.TestSeq := do
|
||||
def test_integration: IO LSpec.TestSeq := do
|
||||
|
||||
return LSpec.group "Integration" $
|
||||
(LSpec.group "Option modify" (← test_option_modify)) ++
|
||||
(LSpec.group "Malformed command" (← test_malformed_command)) ++
|
||||
(LSpec.group "Tactic" (← test_tactic))
|
||||
(LSpec.group "Malformed command" (← test_malformed_command))
|
||||
|
||||
|
||||
end Pantograph.Test.Integration
|
||||
end Pantograph.Test
|
||||
|
|
|
@ -1,5 +1,4 @@
|
|||
import LSpec
|
||||
--import Test.Holes
|
||||
import Test.Integration
|
||||
import Test.Proofs
|
||||
import Test.Serial
|
||||
|
@ -11,10 +10,9 @@ unsafe def main := do
|
|||
Lean.initSearchPath (← Lean.findSysroot)
|
||||
|
||||
let suites := [
|
||||
--Holes.suite,
|
||||
Integration.suite,
|
||||
Proofs.suite,
|
||||
Serial.suite
|
||||
test_integration,
|
||||
test_proofs,
|
||||
test_serial
|
||||
]
|
||||
let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
|
||||
LSpec.lspecIO $ all
|
||||
|
|
476
Test/Proofs.lean
476
Test/Proofs.lean
|
@ -1,23 +1,8 @@
|
|||
/-
|
||||
Tests pertaining to goals with no interdependencies
|
||||
-/
|
||||
import LSpec
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Tactic
|
||||
import Pantograph.Serial
|
||||
import Test.Common
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
def TacticResult.toString : TacticResult → String
|
||||
| .success state => s!".success ({state.goals.length} goals)"
|
||||
| .failure messages =>
|
||||
let messages := "\n".intercalate messages.toList
|
||||
s!".failure {messages}"
|
||||
| .parseError error => s!".parseError {error}"
|
||||
| .indexError index => s!".indexError {index}"
|
||||
end Pantograph
|
||||
|
||||
namespace Pantograph.Test.Proofs
|
||||
namespace Pantograph.Test
|
||||
open Pantograph
|
||||
open Lean
|
||||
|
||||
|
@ -25,62 +10,74 @@ 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 M)
|
||||
abbrev TestM := ReaderT Commands.Options StateRefT ProofTree M
|
||||
|
||||
deriving instance DecidableEq, Repr for Protocol.Expression
|
||||
deriving instance DecidableEq, Repr for Protocol.Variable
|
||||
deriving instance DecidableEq, Repr for Protocol.Goal
|
||||
|
||||
def addTest (test: LSpec.TestSeq): TestM Unit := do
|
||||
set $ (← get) ++ test
|
||||
|
||||
def startProof (start: Start): TestM (Option GoalState) := do
|
||||
def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
let mut testSeq := LSpec.TestSeq.done
|
||||
match start with
|
||||
| .copy name =>
|
||||
let cInfo? := str_to_name name |> env.find?
|
||||
addTest $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
|
||||
testSeq := testSeq ++ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
|
||||
match cInfo? with
|
||||
| .some cInfo =>
|
||||
let goal ← GoalState.create (expr := cInfo.type)
|
||||
return Option.some goal
|
||||
let state ← ProofTree.create
|
||||
(expr := cInfo.type)
|
||||
return (testSeq, Option.some state)
|
||||
| .none =>
|
||||
return Option.none
|
||||
return (testSeq, Option.none)
|
||||
| .expr expr =>
|
||||
let syn? := syntax_from_str env expr
|
||||
addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
|
||||
testSeq := testSeq ++ LSpec.check s!"Parsing {expr}" (syn?.isOk)
|
||||
match syn? with
|
||||
| .error error =>
|
||||
IO.println error
|
||||
return Option.none
|
||||
return (testSeq, Option.none)
|
||||
| .ok syn =>
|
||||
let expr? ← syntax_to_expr_type syn
|
||||
addTest $ LSpec.check s!"Elaborating" expr?.isOk
|
||||
let expr? ← syntax_to_expr syn
|
||||
testSeq := testSeq ++ LSpec.check s!"Elaborating" expr?.isOk
|
||||
match expr? with
|
||||
| .error error =>
|
||||
IO.println error
|
||||
return Option.none
|
||||
return (testSeq, Option.none)
|
||||
| .ok expr =>
|
||||
let goal ← GoalState.create (expr := expr)
|
||||
return Option.some goal
|
||||
let state ← ProofTree.create
|
||||
(expr := expr)
|
||||
return (testSeq, Option.some state)
|
||||
|
||||
def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
|
||||
deriving instance DecidableEq, Repr for Commands.Expression
|
||||
deriving instance DecidableEq, Repr for Commands.Variable
|
||||
deriving instance DecidableEq, Repr for Commands.Goal
|
||||
deriving instance DecidableEq, Repr for TacticResult
|
||||
|
||||
def buildGoal (nameType: List (String × String)) (target: String) (caseName?: Option String := .none): Protocol.Goal :=
|
||||
{
|
||||
caseName?,
|
||||
target := { pp? := .some target},
|
||||
vars := (nameType.map fun x => ({
|
||||
userName := x.fst,
|
||||
type? := .some { pp? := .some x.snd },
|
||||
isInaccessible? := .some false
|
||||
})).toArray
|
||||
}
|
||||
def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
|
||||
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
|
||||
/-- Check the output of each proof step -/
|
||||
def proof_step (stateId: Nat) (goalId: Nat) (tactic: String)
|
||||
(expected: TacticResult) : TestM LSpec.TestSeq := do
|
||||
let options ← read
|
||||
let result: TacticResult ← ProofTree.execute stateId goalId tactic |>.run options
|
||||
match expected, result with
|
||||
| .success (.some i) #[], .success (.some _) goals =>
|
||||
-- If the goals are omitted but the next state is specified, we imply that
|
||||
-- the tactic succeeded.
|
||||
let expected := .success (.some i) goals
|
||||
return LSpec.test s!"{stateId}.{goalId} {tactic}" (result = expected)
|
||||
| _, _ =>
|
||||
return LSpec.test s!"{stateId}.{goalId} {tactic}" (result = expected)
|
||||
|
||||
/-- Check that the tree structure is correct -/
|
||||
def proof_inspect (expected: Array String) : TestM LSpec.TestSeq := do
|
||||
let result := (← get).structure_array
|
||||
return LSpec.test s!"tree structure" (result = expected)
|
||||
|
||||
def proof_runner (env: Lean.Environment) (options: Commands.Options) (start: Start) (steps: List (TestM LSpec.TestSeq)): IO LSpec.TestSeq := do
|
||||
let termElabM := do
|
||||
let (testSeq, state?) ← start_proof start
|
||||
match state? with
|
||||
| .none => return testSeq
|
||||
| .some state => steps.foldlM (fun tests m => do pure $ tests ++ (← m)) testSeq |>.run options |>.run' state
|
||||
|
||||
let coreContext: Lean.Core.Context := {
|
||||
currNamespace := Name.append .anonymous "Aniva",
|
||||
currNamespace := str_to_name "Aniva",
|
||||
openDecls := [], -- No 'open' directives needed
|
||||
fileName := "<Pantograph>",
|
||||
fileMap := { source := "", positions := #[0], lines := #[1] }
|
||||
|
@ -93,117 +90,41 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
|
|||
match ← (coreM.run' coreContext { env := env }).toBaseIO with
|
||||
| .error exception =>
|
||||
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
|
||||
| .ok (_, a) =>
|
||||
return a
|
||||
| .ok a => return a
|
||||
|
||||
def build_goal (nameType: List (String × String)) (target: String): Commands.Goal :=
|
||||
{
|
||||
target := { pp? := .some target},
|
||||
vars := (nameType.map fun x => ({
|
||||
name := x.fst,
|
||||
type? := .some { pp? := .some x.snd },
|
||||
isInaccessible? := .some false
|
||||
})).toArray
|
||||
}
|
||||
|
||||
-- Individual test cases
|
||||
example: ∀ (a b: Nat), a + b = b + a := by
|
||||
intro n m
|
||||
rw [Nat.add_comm]
|
||||
def proof_nat_add_comm (manual: Bool): TestM Unit := do
|
||||
let state? ← startProof <| match manual with
|
||||
| false => .copy "Nat.add_comm"
|
||||
| true => .expr "∀ (a b: Nat), a + b = b + a"
|
||||
addTest $ LSpec.check "Start goal" state?.isSome
|
||||
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 := "intro n m") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"])
|
||||
|
||||
match ← state1.execute (goalId := 0) (tactic := "assumption") with
|
||||
| .failure #[message] =>
|
||||
addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
||||
let state2 ← match ← state1.execute (goalId := 0) (tactic := "rw [Nat.add_comm]") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty
|
||||
|
||||
return ()
|
||||
def proof_delta_variable: TestM Unit := do
|
||||
let options: Protocol.Options := { noRepeat := true }
|
||||
let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a"
|
||||
addTest $ LSpec.check "Start goal" state?.isSome
|
||||
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 := "intro n") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
|
||||
#[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
|
||||
let state2 ← match ← state1.execute (goalId := 0) (tactic := "intro m") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check "intro m" ((← state2.serializeGoals (parent := state1) options).map (·.devolatilize) =
|
||||
#[buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n"])
|
||||
return ()
|
||||
where
|
||||
-- Like `buildGoal` but allow certain variables to be elided.
|
||||
buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal :=
|
||||
{
|
||||
target := { pp? := .some target},
|
||||
vars := (nameType.map fun x => ({
|
||||
userName := x.fst,
|
||||
type? := x.snd.map (λ type => { pp? := type }),
|
||||
isInaccessible? := x.snd.map (λ _ => false)
|
||||
})).toArray
|
||||
}
|
||||
|
||||
example (w x y z : Nat) (p : Nat → Prop)
|
||||
(h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
|
||||
simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
|
||||
assumption
|
||||
def proof_arith: TestM Unit := do
|
||||
let state? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
|
||||
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 := "intros") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check "intros" (state1.goals.length = 1)
|
||||
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
|
||||
let state2 ← match ← state1.execute (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
|
||||
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
|
||||
let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.test "assumption" state3.goals.isEmpty
|
||||
addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
|
||||
return ()
|
||||
def proof_nat_add_comm (env: Lean.Environment): IO LSpec.TestSeq := do
|
||||
let goal1: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
|
||||
proof_runner env {} (.copy "Nat.add_comm") [
|
||||
proof_step 0 0 "intro n m"
|
||||
(.success (.some 1) #[goal1]),
|
||||
proof_step 1 0 "assumption"
|
||||
(.failure #[s!"tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n"]),
|
||||
proof_step 1 0 "rw [Nat.add_comm]"
|
||||
(.success .none #[])
|
||||
]
|
||||
def proof_nat_add_comm_manual (env: Lean.Environment): IO LSpec.TestSeq := do
|
||||
let goal1: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
|
||||
proof_runner env {} (.expr "∀ (a b: Nat), a + b = b + a") [
|
||||
proof_step 0 0 "intro n m"
|
||||
(.success (.some 1) #[goal1]),
|
||||
proof_step 1 0 "assumption"
|
||||
(.failure #[s!"tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n"]),
|
||||
proof_step 1 0 "rw [Nat.add_comm]"
|
||||
(.success .none #[])
|
||||
]
|
||||
|
||||
-- Two ways to write the same theorem
|
||||
example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
|
||||
|
@ -220,181 +141,80 @@ example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
|
|||
assumption
|
||||
. apply Or.inl
|
||||
assumption
|
||||
def proof_or_comm: TestM Unit := do
|
||||
let state? ← startProof (.expr "∀ (p q: Prop), p ∨ q → q ∨ p")
|
||||
let state0 ← match state? with
|
||||
| .some state => pure state
|
||||
| .none => do
|
||||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
def proof_or_comm (env: Lean.Environment): IO LSpec.TestSeq := do
|
||||
let typeProp: Commands.Expression := { pp? := .some "Prop" }
|
||||
let branchGoal (caseName name: String): Commands.Goal := {
|
||||
caseName? := .some caseName,
|
||||
target := { pp? := .some "q ∨ p" },
|
||||
vars := #[
|
||||
{ name := "p", type? := .some typeProp, isInaccessible? := .some false },
|
||||
{ name := "q", type? := .some typeProp, isInaccessible? := .some false },
|
||||
{ name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
|
||||
]
|
||||
}
|
||||
proof_runner env {} (.expr "∀ (p q: Prop), p ∨ q → q ∨ p") [
|
||||
proof_step 0 0 "intro p q h"
|
||||
(.success (.some 1) #[build_goal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"]),
|
||||
proof_step 1 0 "cases h"
|
||||
(.success (.some 2) #[branchGoal "inl" "p", branchGoal "inr" "q"]),
|
||||
proof_inspect #["", "0.0", "1.0"],
|
||||
proof_step 2 0 "apply Or.inr"
|
||||
(.success (.some 3) #[]),
|
||||
proof_inspect #["", "0.0", "1.0", "2.0"],
|
||||
proof_step 3 0 "assumption"
|
||||
(.success .none #[]),
|
||||
proof_step 2 1 "apply Or.inl"
|
||||
(.success (.some 4) #[]),
|
||||
proof_step 4 0 "assumption"
|
||||
(.success .none #[]),
|
||||
proof_inspect #["", "0.0", "1.0", "2.0", "2.1"]
|
||||
]
|
||||
|
||||
let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"])
|
||||
let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[branchGoal "inl" "p", branchGoal "inr" "q"])
|
||||
example (w x y z : Nat) (p : Nat → Prop)
|
||||
(h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
|
||||
simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
|
||||
assumption
|
||||
def proof_arith_1 (env: Lean.Environment): IO LSpec.TestSeq := do
|
||||
proof_runner env {} (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)") [
|
||||
proof_step 0 0 "intros"
|
||||
(.success (.some 1) #[]),
|
||||
proof_step 1 0 "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *"
|
||||
(.success (.some 2) #[]),
|
||||
proof_step 2 0 "assumption"
|
||||
(.success .none #[])
|
||||
]
|
||||
|
||||
let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
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
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check " assumption" state4_1.goals.isEmpty
|
||||
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
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1)
|
||||
let state4_2 ← match ← state3_2.execute (goalId := 0) (tactic := "assumption") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check " assumption" state4_2.goals.isEmpty
|
||||
addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone
|
||||
-- Ensure the proof can continue from `state4_2`.
|
||||
let state2b ← match state2.continue state4_2 with
|
||||
| .error msg => do
|
||||
addTest $ assertUnreachable $ msg
|
||||
return ()
|
||||
| .ok state => pure state
|
||||
addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0])
|
||||
let state3_1 ← match ← state2b.execute (goalId := 0) (tactic := "apply Or.inr") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
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
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check " assumption" state4_1.goals.isEmpty
|
||||
addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isSome
|
||||
def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal :=
|
||||
{
|
||||
target := { pp? := .some target},
|
||||
vars := (nameType.map fun x => ({
|
||||
name := x.fst,
|
||||
type? := x.snd.map (λ type => { pp? := type }),
|
||||
isInaccessible? := x.snd.map (λ _ => false)
|
||||
})).toArray
|
||||
}
|
||||
def proof_delta_variable (env: Lean.Environment): IO LSpec.TestSeq := do
|
||||
let goal1: Commands.Goal := build_goal_selective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"
|
||||
let goal2: Commands.Goal := build_goal_selective [("n", .none), ("m", .some "Nat")] "n + m = m + n"
|
||||
proof_runner env { proofVariableDelta := true } (.expr "∀ (a b: Nat), a + b = b + a") [
|
||||
proof_step 0 0 "intro n"
|
||||
(.success (.some 1) #[goal1]),
|
||||
proof_step 1 0 "intro m"
|
||||
(.success (.some 2) #[goal2])
|
||||
]
|
||||
|
||||
return ()
|
||||
where
|
||||
typeProp: Protocol.Expression := { pp? := .some "Prop" }
|
||||
branchGoal (caseName name: String): Protocol.Goal := {
|
||||
caseName? := .some caseName,
|
||||
target := { pp? := .some "q ∨ p" },
|
||||
vars := #[
|
||||
{ userName := "p", type? := .some typeProp, isInaccessible? := .some false },
|
||||
{ userName := "q", type? := .some typeProp, isInaccessible? := .some false },
|
||||
{ userName := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
|
||||
]
|
||||
}
|
||||
|
||||
/-- M-coupled goals -/
|
||||
def proof_m_couple: TestM Unit := do
|
||||
let state? ← startProof (.expr "(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"])
|
||||
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
|
||||
-- Set m to 3
|
||||
let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
|
||||
let state1b ← match state1.continue state2 with
|
||||
| .error msg => do
|
||||
addTest $ assertUnreachable $ msg
|
||||
return ()
|
||||
| .ok state => pure state
|
||||
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
|
||||
return ()
|
||||
|
||||
def proof_proposition_generation: TestM Unit := do
|
||||
let state? ← startProof (.expr "Σ' p:Prop, p")
|
||||
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 PSigma.mk") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[
|
||||
buildGoal [] "?fst" (caseName? := .some "snd"),
|
||||
buildGoal [] "Prop" (caseName? := .some "fst")
|
||||
])
|
||||
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
|
||||
|
||||
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
|
||||
#[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"])
|
||||
addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
|
||||
|
||||
let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
|
||||
#[])
|
||||
addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
|
||||
return ()
|
||||
|
||||
def suite: IO LSpec.TestSeq := do
|
||||
def test_proofs : IO LSpec.TestSeq := do
|
||||
let env: Lean.Environment ← Lean.importModules
|
||||
(imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}])
|
||||
(imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
|
||||
(opts := {})
|
||||
(trustLevel := 1)
|
||||
let tests := [
|
||||
("Nat.add_comm", proof_nat_add_comm false),
|
||||
("Nat.add_comm manual", proof_nat_add_comm true),
|
||||
("Nat.add_comm delta", proof_delta_variable),
|
||||
("arithmetic", proof_arith),
|
||||
("Or.comm", proof_or_comm),
|
||||
("2 < 5", proof_m_couple),
|
||||
("Proposition Generation", proof_proposition_generation)
|
||||
]
|
||||
let tests ← tests.foldlM (fun acc tests => do
|
||||
let (name, tests) := tests
|
||||
let tests ← proofRunner env tests
|
||||
return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
|
||||
|
||||
return LSpec.group "Proofs" tests
|
||||
return LSpec.group "Proofs" $
|
||||
(LSpec.group "Nat.add_comm" $ (← proof_nat_add_comm env)) ++
|
||||
(LSpec.group "Nat.add_comm manual" $ (← proof_nat_add_comm_manual env)) ++
|
||||
(LSpec.group "Or.comm" $ (← proof_or_comm env)) ++
|
||||
(LSpec.group "Arithmetic 1" $ (← proof_arith_1 env)) ++
|
||||
(LSpec.group "Delta variable" $ (← proof_delta_variable env))
|
||||
|
||||
end Pantograph.Test
|
||||
|
||||
end Pantograph.Test.Proofs
|
||||
|
|
|
@ -1,19 +1,19 @@
|
|||
import LSpec
|
||||
import Pantograph.Serial
|
||||
import Pantograph.Symbol
|
||||
import Pantograph.Symbols
|
||||
|
||||
namespace Pantograph.Test.Serial
|
||||
namespace Pantograph.Test
|
||||
|
||||
open Pantograph
|
||||
open Lean
|
||||
|
||||
deriving instance Repr, DecidableEq for Protocol.BoundExpression
|
||||
deriving instance Repr, DecidableEq for Commands.BoundExpression
|
||||
|
||||
def test_str_to_name: LSpec.TestSeq :=
|
||||
LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")
|
||||
|
||||
def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
|
||||
let entries: List (String × Protocol.BoundExpression) := [
|
||||
let entries: List (String × Commands.BoundExpression) := [
|
||||
("Nat.add_comm", { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }),
|
||||
("Nat.le_of_succ_le", { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" })
|
||||
]
|
||||
|
@ -47,8 +47,8 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
|
|||
let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
|
||||
let env ← MonadEnv.getEnv
|
||||
let expr := str_to_name symbol |> env.find? |>.get! |>.type
|
||||
let test := LSpec.check symbol ((serialize_expression_ast expr) = target)
|
||||
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
|
||||
let test := LSpec.check symbol ((← serialize_expression_ast expr) = target)
|
||||
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
|
||||
let coreM := metaM.run'
|
||||
let coreContext: Core.Context := {
|
||||
currNamespace := Lean.Name.str .anonymous "Aniva"
|
||||
|
@ -62,15 +62,15 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
|
|||
| .ok a => return a
|
||||
|
||||
|
||||
def suite: IO LSpec.TestSeq := do
|
||||
def test_serial: IO LSpec.TestSeq := do
|
||||
let env: Environment ← importModules
|
||||
(imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
|
||||
(imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
|
||||
(opts := {})
|
||||
(trustLevel := 1)
|
||||
|
||||
return LSpec.group "Serialization" $
|
||||
return LSpec.group "Serialisation" $
|
||||
(LSpec.group "str_to_name" test_str_to_name) ++
|
||||
(LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
|
||||
(LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env))
|
||||
|
||||
end Pantograph.Test.Serial
|
||||
end Pantograph.Test
|
||||
|
|
|
@ -0,0 +1,3 @@
|
|||
#!/bin/bash
|
||||
|
||||
lake build test && lake env build/bin/test
|
202
flake.lock
202
flake.lock
|
@ -1,202 +0,0 @@
|
|||
{
|
||||
"nodes": {
|
||||
"flake-parts": {
|
||||
"inputs": {
|
||||
"nixpkgs-lib": "nixpkgs-lib"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1696343447,
|
||||
"narHash": "sha256-B2xAZKLkkeRFG5XcHHSXXcP7To9Xzr59KXeZiRf4vdQ=",
|
||||
"owner": "hercules-ci",
|
||||
"repo": "flake-parts",
|
||||
"rev": "c9afaba3dfa4085dbd2ccb38dfade5141e33d9d4",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "hercules-ci",
|
||||
"repo": "flake-parts",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"flake-utils": {
|
||||
"locked": {
|
||||
"lastModified": 1656928814,
|
||||
"narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"lean": {
|
||||
"inputs": {
|
||||
"flake-utils": "flake-utils",
|
||||
"lean4-mode": "lean4-mode",
|
||||
"nix": "nix",
|
||||
"nixpkgs": "nixpkgs_2"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1695693562,
|
||||
"narHash": "sha256-6qbCafG0bL5KxQt2gL6hV4PFDsEMM0UXfldeOOqxsaE=",
|
||||
"owner": "leanprover",
|
||||
"repo": "lean4",
|
||||
"rev": "a832f398b80a5ebb820d27b9e55ec949759043ff",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "leanprover",
|
||||
"ref": "v4.1.0",
|
||||
"repo": "lean4",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"lean4-mode": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
"lastModified": 1676498134,
|
||||
"narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
|
||||
"owner": "leanprover",
|
||||
"repo": "lean4-mode",
|
||||
"rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "leanprover",
|
||||
"repo": "lean4-mode",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"lowdown-src": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
"lastModified": 1633514407,
|
||||
"narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
|
||||
"owner": "kristapsdz",
|
||||
"repo": "lowdown",
|
||||
"rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "kristapsdz",
|
||||
"repo": "lowdown",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nix": {
|
||||
"inputs": {
|
||||
"lowdown-src": "lowdown-src",
|
||||
"nixpkgs": "nixpkgs",
|
||||
"nixpkgs-regression": "nixpkgs-regression"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1657097207,
|
||||
"narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nix",
|
||||
"rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"repo": "nix",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs": {
|
||||
"locked": {
|
||||
"lastModified": 1653988320,
|
||||
"narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"ref": "nixos-22.05-small",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs-lib": {
|
||||
"locked": {
|
||||
"dir": "lib",
|
||||
"lastModified": 1696019113,
|
||||
"narHash": "sha256-X3+DKYWJm93DRSdC5M6K5hLqzSya9BjibtBsuARoPco=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "f5892ddac112a1e9b3612c39af1b72987ee5783a",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"dir": "lib",
|
||||
"owner": "NixOS",
|
||||
"ref": "nixos-unstable",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs-regression": {
|
||||
"locked": {
|
||||
"lastModified": 1643052045,
|
||||
"narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"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=",
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "ca012a02bf8327be9e488546faecae5e05d7d749",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "nixos",
|
||||
"ref": "nixos-unstable",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"root": {
|
||||
"inputs": {
|
||||
"flake-parts": "flake-parts",
|
||||
"lean": "lean",
|
||||
"nixpkgs": "nixpkgs_3"
|
||||
}
|
||||
}
|
||||
},
|
||||
"root": "root",
|
||||
"version": 7
|
||||
}
|
38
flake.nix
38
flake.nix
|
@ -1,38 +0,0 @@
|
|||
{
|
||||
description = "Pantograph";
|
||||
|
||||
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";
|
||||
};
|
||||
|
||||
outputs = inputs @ {
|
||||
self,
|
||||
nixpkgs,
|
||||
flake-parts,
|
||||
lean,
|
||||
...
|
||||
} : flake-parts.lib.mkFlake { inherit inputs; } {
|
||||
flake = {
|
||||
};
|
||||
systems = [
|
||||
"x86_64-linux"
|
||||
"x86_64-darwin"
|
||||
];
|
||||
perSystem = { system, pkgs, ... }: let
|
||||
leanPkgs = lean.packages.${system};
|
||||
project = leanPkgs.buildLeanPackage {
|
||||
name = "Pantograph";
|
||||
roots = [ "Main" "Pantograph" ];
|
||||
src = ./.;
|
||||
};
|
||||
in rec {
|
||||
packages = project // {
|
||||
inherit (leanPkgs) lean;
|
||||
default = packages.executable;
|
||||
};
|
||||
devShells.default = project.devShell;
|
||||
};
|
||||
};
|
||||
}
|
|
@ -1,11 +1,33 @@
|
|||
{"version": 5,
|
||||
{"version": 4,
|
||||
"packagesDir": "lake-packages",
|
||||
"packages":
|
||||
[{"git":
|
||||
{"url": "https://github.com/lurk-lab/LSpec.git",
|
||||
"subDir?": null,
|
||||
"rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
|
||||
"opts": {},
|
||||
"name": "LSpec",
|
||||
"inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
|
||||
"inherited": false}}]}
|
||||
"inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41"}},
|
||||
{"git":
|
||||
{"url": "https://github.com/leanprover-community/mathlib4.git",
|
||||
"subDir?": null,
|
||||
"rev": "8e5a00a8afc8913c0584cb85f37951995275fd87",
|
||||
"name": "mathlib",
|
||||
"inputRev?": "8e5a00a8afc8913c0584cb85f37951995275fd87"}},
|
||||
{"git":
|
||||
{"url": "https://github.com/gebner/quote4",
|
||||
"subDir?": null,
|
||||
"rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
|
||||
"name": "Qq",
|
||||
"inputRev?": "master"}},
|
||||
{"git":
|
||||
{"url": "https://github.com/JLimperg/aesop",
|
||||
"subDir?": null,
|
||||
"rev": "cdc00b640d0179910ebaa9c931e3b733a04b881c",
|
||||
"name": "aesop",
|
||||
"inputRev?": "master"}},
|
||||
{"git":
|
||||
{"url": "https://github.com/leanprover/std4",
|
||||
"subDir?": null,
|
||||
"rev": "6006307d2ceb8743fea7e00ba0036af8654d0347",
|
||||
"name": "std",
|
||||
"inputRev?": "main"}}]}
|
||||
|
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:4.1.0
|
||||
leanprover/lean4:nightly-2023-08-12
|
||||
|
|
Loading…
Reference in New Issue