feat: Output shared library in Nix flake #48

Merged
aniva merged 16 commits from feature/lib into dev 2024-03-16 19:01:04 -07:00
14 changed files with 253 additions and 139 deletions

View File

@ -2,6 +2,7 @@ import Lean.Data.Json
import Lean.Environment import Lean.Environment
import Pantograph.Version import Pantograph.Version
import Pantograph.Library
import Pantograph import Pantograph
-- Main IO functions -- Main IO functions
@ -39,35 +40,6 @@ partial def loop : MainM Unit := do
IO.println str IO.println str
loop loop
namespace Lean
/-- This is better than the default version since it handles `.` and doesn't
crash the program when it fails. -/
def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO Options := do
let ps := (entry.splitOn "=").map String.trim
let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'"
let key := key.toName
let defValue ← getOptionDefaultValue key
match defValue with
| DataValue.ofString _ => pure $ opts.setString key val
| DataValue.ofBool _ =>
match val with
| "true" => pure $ opts.setBool key true
| "false" => pure $ opts.setBool key false
| _ => throw s!"invalid Bool option value '{val}'"
| DataValue.ofName _ => pure $ opts.setName key val.toName
| DataValue.ofNat _ =>
match val.toNat? with
| none => throw s!"invalid Nat option value '{val}'"
| some v => pure $ opts.setNat key v
| DataValue.ofInt _ =>
match val.toInt? with
| none => throw s!"invalid Int option value '{val}'"
| some v => pure $ opts.setInt key v
| DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
end Lean
unsafe def main (args: List String): IO Unit := do unsafe def main (args: List String): IO Unit := do
-- NOTE: A more sophisticated scheme of command line argument handling is needed. -- NOTE: A more sophisticated scheme of command line argument handling is needed.
@ -76,35 +48,19 @@ unsafe def main (args: List String): IO Unit := do
println! s!"{version}" println! s!"{version}"
return return
Lean.enableInitializersExecution initSearch ""
Lean.initSearchPath (← Lean.findSysroot)
let options? ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none) let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
|>.foldlM Lean.setOptionFromString' Lean.Options.empty |>.toArray |> createCoreContext
|>.run
let options ← match options? with
| .ok options => pure options
| .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
let imports:= args.filter (λ s => ¬ (s.startsWith "--")) let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
let coreState ← createCoreState imports.toArray
let env ← Lean.importModules
(imports := imports.toArray.map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
let context: Context := { let context: Context := {
imports imports
} }
let coreContext: Lean.Core.Context := {
currNamespace := Lean.Name.str .anonymous "Aniva"
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] },
options := options
}
try try
let coreM := loop.run context |>.run' {} let coreM := loop.run context |>.run' {}
IO.println "ready." IO.println "ready."
discard <| coreM.toIO coreContext { env := env } discard <| coreM.toIO coreContext coreState
catch ex => catch ex =>
IO.println "Uncaught IO exception" IO.println "Uncaught IO exception"
IO.println ex.toString IO.println ex.toString

View File

@ -1,8 +1,8 @@
LIB := build/lib/Pantograph.olean LIB := ./.lake/build/lib/Pantograph.olean
EXE := build/bin/pantograph EXE := ./.lake/build/bin/pantograph
SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain
TEST_EXE := build/bin/test TEST_EXE := ./.lake/build/bin/test
TEST_SOURCE := $(wildcard Test/*.lean) TEST_SOURCE := $(wildcard Test/*.lean)
$(LIB) $(EXE): $(SOURCE) $(LIB) $(EXE): $(SOURCE)
@ -12,7 +12,7 @@ $(TEST_EXE): $(LIB) $(TEST_SOURCE)
lake build test lake build test
test: $(TEST_EXE) test: $(TEST_EXE)
lake env $(TEST_EXE) $(TEST_EXE)
clean: clean:
lake clean lake clean

View File

@ -2,6 +2,7 @@ import Pantograph.Goal
import Pantograph.Protocol import Pantograph.Protocol
import Pantograph.Serial import Pantograph.Serial
import Pantograph.Environment import Pantograph.Environment
import Pantograph.Library
import Lean.Data.HashMap import Lean.Data.HashMap
namespace Pantograph namespace Pantograph
@ -21,14 +22,6 @@ abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
-- certain monadic features in `MainM` -- certain monadic features in `MainM`
abbrev CR α := Except Protocol.InteractionError α abbrev CR α := Except Protocol.InteractionError α
def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
metaM.run'
def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
termElabM.run' (ctx := {
declName? := .none,
errToSorry := false,
}) |>.run'
def execute (command: Protocol.Command): MainM Lean.Json := do def execute (command: Protocol.Command): MainM Lean.Json := do
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
match Lean.fromJson? command.payload with match Lean.fromJson? command.payload with
@ -56,7 +49,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
errorCommand s!"Unknown command {cmd}" errorCommand s!"Unknown command {cmd}"
return Lean.toJson error return Lean.toJson error
where where
errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
errorCommand := errorI "command" errorCommand := errorI "command"
errorIndex := errorI "index" errorIndex := errorI "index"
-- Command Functions -- Command Functions
@ -70,7 +62,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let nGoals := state.goalStates.size let nGoals := state.goalStates.size
return .ok { nGoals } return .ok { nGoals }
env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
Environment.catalog args let result ← Environment.catalog args
return .ok result
env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
let state ← get let state ← get
Environment.inspect args state.options Environment.inspect args state.options
@ -78,22 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
Environment.addDecl args Environment.addDecl args
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
let state ← get let state ← get
let env ← Lean.MonadEnv.getEnv exprEcho args.expr state.options
let syn ← match syntax_from_str env args.expr with
| .error str => return .error $ errorI "parsing" str
| .ok syn => pure syn
runTermElabM (do
match ← syntax_to_expr syn with
| .error str => return .error $ errorI "elab" str
| .ok expr => do
try
let type ← Lean.Meta.inferType expr
return .ok {
type := (← serialize_expression (options := state.options) type),
expr := (← serialize_expression (options := state.options) expr)
}
catch exception =>
return .error $ errorI "typing" (← exception.toMessageData.toString))
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
let state ← get let state ← get
let options := state.options let options := state.options
@ -115,13 +93,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let state ← get let state ← get
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
| .some expr, .none => | .some expr, .none => do
(match syntax_from_str env expr with let expr ← match ← exprParse expr with
| .error str => return .error <| errorI "parsing" str | .error e => return .error e
| .ok syn => do | .ok expr => pure $ expr
(match ← syntax_to_expr syn with return .ok $ ← GoalState.create expr
| .error str => return .error <| errorI "elab" str
| .ok expr => return .ok (← GoalState.create expr)))
| .none, .some copyFrom => | .none, .some copyFrom =>
(match env.find? <| copyFrom.toName with (match env.find? <| copyFrom.toName with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
@ -144,9 +120,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .some goalState => do | .some goalState => do
let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
| .some tactic, .none => do | .some tactic, .none => do
pure ( Except.ok (← runTermElabM <| GoalState.execute goalState args.goalId tactic)) pure ( Except.ok (← goalTactic goalState args.goalId tactic))
| .none, .some expr => do | .none, .some expr => do
pure ( Except.ok (← runTermElabM <| GoalState.tryAssign goalState args.goalId expr)) pure ( Except.ok (← goalTryAssign goalState args.goalId expr))
| _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied") | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
match nextGoalState? with match nextGoalState? with
| .error error => return .error error | .error error => return .error error
@ -178,8 +154,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .none => return .error $ errorIndex s!"Invalid state index {branchId}" | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
| .some branch => pure $ target.continue branch | .some branch => pure $ target.continue branch
| .none, .some goals => | .none, .some goals =>
let goals := goals.map (λ name => { name := name.toName }) pure $ goalResume target goals
pure $ target.resume goals
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
match nextState? with match nextState? with
| .error error => return .error <| errorI "structure" error | .error error => return .error <| errorI "structure" error
@ -189,7 +164,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
goalStates := state.goalStates.insert nextStateId nextGoalState, goalStates := state.goalStates.insert nextStateId nextGoalState,
nextId := state.nextId + 1 nextId := state.nextId + 1
} }
let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) |>.run' let goals ← goalSerialize nextGoalState (options := state.options)
return .ok { return .ok {
nextStateId, nextStateId,
goals, goals,
@ -204,12 +179,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
match state.goalStates.find? args.stateId with match state.goalStates.find? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => runMetaM <| do | .some goalState => runMetaM <| do
goalState.restoreMetaM return .ok (← goalPrint goalState state.options)
let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
let parent? ← goalState.parentExpr?.mapM (λ expr => serialize_expression state.options expr)
return .ok {
root?,
parent?,
}
end Pantograph end Pantograph

View File

@ -30,14 +30,14 @@ def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :
if is_symbol_unsafe_or_internal n info if is_symbol_unsafe_or_internal n info
then Option.none then Option.none
else Option.some <| to_compact_symbol_name n info else Option.some <| to_compact_symbol_name n info
def catalog (_: Protocol.EnvCatalog): CoreM (Protocol.CR Protocol.EnvCatalogResult) := do def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let names := env.constants.fold (init := #[]) (λ acc name info => let names := env.constants.fold (init := #[]) (λ acc name info =>
match to_filtered_symbol name info with match to_filtered_symbol name info with
| .some x => acc.push x | .some x => acc.push x
| .none => acc) | .none => acc)
return .ok { symbols := names } return { symbols := names }
def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let name := args.name.toName let name := args.name.toName
let info? := env.find? name let info? := env.find? name
@ -66,8 +66,8 @@ def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Prot
| .inductInfo induct => { core with inductInfo? := .some { | .inductInfo induct => { core with inductInfo? := .some {
numParams := induct.numParams, numParams := induct.numParams,
numIndices := induct.numIndices, numIndices := induct.numIndices,
all := induct.all.map (·.toString), all := induct.all.toArray.map (·.toString),
ctors := induct.ctors.map (·.toString), ctors := induct.ctors.toArray.map (·.toString),
isRec := induct.isRec, isRec := induct.isRec,
isReflexive := induct.isReflexive, isReflexive := induct.isReflexive,
isNested := induct.isNested, isNested := induct.isNested,
@ -79,7 +79,7 @@ def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Prot
numFields := ctor.numFields, numFields := ctor.numFields,
} } } }
| .recInfo r => { core with recursorInfo? := .some { | .recInfo r => { core with recursorInfo? := .some {
all := r.all.map (·.toString), all := r.all.toArray.map (·.toString),
numParams := r.numParams, numParams := r.numParams,
numIndices := r.numIndices, numIndices := r.numIndices,
numMotives := r.numMotives, numMotives := r.numMotives,

179
Pantograph/Library.lean Normal file
View File

@ -0,0 +1,179 @@
import Pantograph.Environment
import Pantograph.Goal
import Pantograph.Protocol
import Pantograph.Serial
import Pantograph.Version
import Lean
namespace Lean
/-- This is better than the default version since it handles `.` and doesn't
crash the program when it fails. -/
def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO Options := do
let ps := (entry.splitOn "=").map String.trim
let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'"
let key := key.toName
let defValue ← getOptionDefaultValue key
match defValue with
| DataValue.ofString _ => pure $ opts.setString key val
| DataValue.ofBool _ =>
match val with
| "true" => pure $ opts.setBool key true
| "false" => pure $ opts.setBool key false
| _ => throw s!"invalid Bool option value '{val}'"
| DataValue.ofName _ => pure $ opts.setName key val.toName
| DataValue.ofNat _ =>
match val.toNat? with
| none => throw s!"invalid Nat option value '{val}'"
| some v => pure $ opts.setNat key v
| DataValue.ofInt _ =>
match val.toInt? with
| none => throw s!"invalid Int option value '{val}'"
| some v => pure $ opts.setInt key v
| DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
end Lean
namespace Pantograph
def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
metaM.run'
def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
termElabM.run' (ctx := {
declName? := .none,
errToSorry := false,
}) |>.run'
def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
/-- Adds the given paths to Lean package search path -/
@[export pantograph_init_search]
unsafe def initSearch (sp: String): IO Unit := do
Lean.enableInitializersExecution
Lean.initSearchPath (← Lean.findSysroot) (sp := System.SearchPath.parse sp)
/-- Creates a Core.Context object needed to run all monads -/
@[export pantograph_create_core_context]
def createCoreContext (options: Array String): IO Lean.Core.Context := do
let options? ← options.foldlM Lean.setOptionFromString' Lean.Options.empty |>.run
let options ← match options? with
| .ok options => pure options
| .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
return {
currNamespace := Lean.Name.str .anonymous "Aniva"
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] },
options := options
}
/-- Creates a Core.State object needed to run all monads -/
@[export pantograph_create_core_state]
def createCoreState (imports: Array String): IO Lean.Core.State := do
let env ← Lean.importModules
(imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
return { env := env }
@[export pantograph_env_catalog_m]
def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
Environment.catalog ({}: Protocol.EnvCatalog)
@[export pantograph_mk_options]
def mkOptions
(printJsonPretty: Bool)
(printExprPretty: Bool)
(printExprAST: Bool)
(noRepeat: Bool)
(printAuxDecls: Bool)
(printImplementationDetailHyps: Bool)
: Protocol.Options := {
printJsonPretty,
printExprPretty,
printExprAST,
noRepeat,
printAuxDecls,
printImplementationDetailHyps,
}
@[export pantograph_env_inspect_m]
def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) :=
Environment.inspect ({
name, value? := .some value, dependency?:= .some dependency
}: Protocol.EnvInspect) options
@[export pantograph_env_add_m]
def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
Lean.CoreM (Protocol.CR Protocol.EnvAddResult) :=
Environment.addDecl { name, type, value, isTheorem }
/-- This must be a TermElabM since the parsed expr contains extra information -/
def exprParse (s: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
let env ← Lean.MonadEnv.getEnv
let syn ← match syntax_from_str env s with
| .error str => return .error $ errorI "parsing" str
| .ok syn => pure syn
match ← syntax_to_expr syn with
| .error str => return .error $ errorI "elab" str
| .ok expr => return .ok expr
@[export pantograph_expr_echo_m]
def exprEcho (expr: String) (options: @&Protocol.Options):
Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
let termElabM: Lean.Elab.TermElabM _ := do
let expr ← match ← exprParse expr with
| .error e => return .error e
| .ok expr => pure expr
try
let type ← Lean.Meta.inferType expr
return .ok {
type := (← serialize_expression options type),
expr := (← serialize_expression options expr)
}
catch exception =>
return .error $ errorI "typing" (← exception.toMessageData.toString)
runTermElabM termElabM
@[export pantograph_goal_start_expr_m]
def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
let termElabM: Lean.Elab.TermElabM _ := do
let expr ← match ← exprParse expr with
| .error e => return .error e
| .ok expr => pure $ expr
return .ok $ ← GoalState.create expr
runTermElabM termElabM
@[export pantograph_goal_tactic_m]
def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult :=
runTermElabM <| GoalState.execute state goalId tactic
@[export pantograph_goal_try_assign_m]
def goalTryAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult :=
runTermElabM <| GoalState.tryAssign state goalId expr
@[export pantograph_goal_continue]
def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
target.continue branch
@[export pantograph_goal_resume]
def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
@[export pantograph_goal_serialize_m]
def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
runMetaM <| state.serializeGoals (parent := .none) options
@[export pantograph_goal_print_m]
def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do
let metaM := do
state.restoreMetaM
return {
root? := ← state.rootExpr?.mapM (λ expr => serialize_expression options expr),
parent? := ← state.parentExpr?.mapM (λ expr => serialize_expression options expr),
}
runMetaM metaM
end Pantograph

View File

@ -124,8 +124,8 @@ structure EnvInspect where
structure InductInfo where structure InductInfo where
numParams: Nat numParams: Nat
numIndices: Nat numIndices: Nat
all: List String all: Array String
ctors: List String ctors: Array String
isRec: Bool := false isRec: Bool := false
isReflexive: Bool := false isReflexive: Bool := false
isNested: Bool := false isNested: Bool := false
@ -138,7 +138,7 @@ structure ConstructorInfo where
numFields: Nat numFields: Nat
deriving Lean.ToJson deriving Lean.ToJson
structure RecursorInfo where structure RecursorInfo where
all: List String all: Array String
numParams: Nat numParams: Nat
numIndices: Nat numIndices: Nat
numMotives: Nat numMotives: Nat
@ -163,7 +163,7 @@ structure EnvAdd where
name: String name: String
type: String type: String
value: String value: String
isTheorem?: Bool isTheorem: Bool
deriving Lean.FromJson deriving Lean.FromJson
structure EnvAddResult where structure EnvAddResult where
deriving Lean.ToJson deriving Lean.ToJson
@ -221,7 +221,7 @@ structure GoalContinue where
-- The state which is an ancestor of `target` where goals will be extracted from -- The state which is an ancestor of `target` where goals will be extracted from
branch?: Option Nat := .none branch?: Option Nat := .none
-- Or, the particular goals that should be brought back into scope -- Or, the particular goals that should be brought back into scope
goals?: Option (List String) := .none goals?: Option (Array String) := .none
deriving Lean.FromJson deriving Lean.FromJson
structure GoalContinueResult where structure GoalContinueResult where
nextStateId: Nat nextStateId: Nat
@ -230,6 +230,7 @@ structure GoalContinueResult where
-- Remove goal states -- Remove goal states
structure GoalDelete where structure GoalDelete where
-- This is ok being a List because it doesn't show up in the ABI
stateIds: List Nat stateIds: List Nat
deriving Lean.FromJson deriving Lean.FromJson
structure GoalDeleteResult where structure GoalDeleteResult where

View File

@ -157,7 +157,7 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
| .instImplicit => " :instImplicit" | .instImplicit => " :instImplicit"
of_name (name: Name) := name_to_ast name sanitize of_name (name: Name) := name_to_ast name sanitize
def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.Expression := do def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
let pp := toString (← Meta.ppExpr e) let pp := toString (← Meta.ppExpr e)
let pp?: Option String := match options.printExprPretty with let pp?: Option String := match options.printExprPretty with
| true => .some pp | true => .some pp
@ -172,7 +172,7 @@ def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.E
} }
/-- Adapted from ppGoal -/ /-- Adapted from ppGoal -/
def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
: MetaM Protocol.Goal := do : MetaM Protocol.Goal := do
-- Options for printing; See Meta.ppGoal for details -- Options for printing; See Meta.ppGoal for details
let showLetValues := true let showLetValues := true
@ -242,7 +242,11 @@ def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: Metavar
where where
of_name (n: Name) := name_to_ast n (sanitize := false) of_name (n: Name) := name_to_ast n (sanitize := false)
protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do protected def GoalState.serializeGoals
(state: GoalState)
(parent: Option GoalState := .none)
(options: @&Protocol.Options := {}):
MetaM (Array Protocol.Goal):= do
state.restoreMetaM state.restoreMetaM
let goals := state.goals.toArray let goals := state.goals.toArray
let parentDecl? := parent.bind (λ parentState => let parentDecl? := parent.bind (λ parentState =>

View File

@ -1,5 +1,6 @@
namespace Pantograph namespace Pantograph
def version := "0.2.12-alpha" @[export pantograph_version]
def version := "0.2.13"
end Pantograph end Pantograph

View File

@ -34,8 +34,8 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
("Or", ConstantCat.induct { ("Or", ConstantCat.induct {
numParams := 2, numParams := 2,
numIndices := 0, numIndices := 0,
all := ["Or"], all := #["Or"],
ctors := ["Or.inl", "Or.inr"], ctors := #["Or.inl", "Or.inr"],
}), }),
("Except.ok", ConstantCat.ctor { ("Except.ok", ConstantCat.ctor {
induct := "Except", induct := "Except",
@ -44,7 +44,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
numFields := 1, numFields := 1,
}), }),
("Eq.rec", ConstantCat.recursor { ("Eq.rec", ConstantCat.recursor {
all := ["Eq"], all := #["Eq"],
numParams := 2, numParams := 2,
numIndices := 1, numIndices := 1,
numMotives := 1, numMotives := 1,
@ -52,7 +52,7 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
k := true, k := true,
}), }),
("ForM.rec", ConstantCat.recursor { ("ForM.rec", ConstantCat.recursor {
all := ["ForM"], all := #["ForM"],
numParams := 3, numParams := 3,
numIndices := 0, numIndices := 0,
numMotives := 1, numMotives := 1,

View File

@ -41,16 +41,16 @@
"nixpkgs": "nixpkgs_2" "nixpkgs": "nixpkgs_2"
}, },
"locked": { "locked": {
"lastModified": 1695693562, "lastModified": 1710520221,
"narHash": "sha256-6qbCafG0bL5KxQt2gL6hV4PFDsEMM0UXfldeOOqxsaE=", "narHash": "sha256-8Fm4bj9sqqsUHFZweSdGMM5GdUX3jkGK/ggGq27CeQc=",
"owner": "leanprover", "owner": "leanprover",
"repo": "lean4", "repo": "lean4",
"rev": "a832f398b80a5ebb820d27b9e55ec949759043ff", "rev": "f70895ede54501adf0db77474f452a7fef40d0b3",
"type": "github" "type": "github"
}, },
"original": { "original": {
"owner": "leanprover", "owner": "leanprover",
"ref": "v4.1.0", "ref": "f70895ede54501adf0db77474f452a7fef40d0b3",
"repo": "lean4", "repo": "lean4",
"type": "github" "type": "github"
} }

View File

@ -4,7 +4,7 @@
inputs = { inputs = {
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
flake-parts.url = "github:hercules-ci/flake-parts"; flake-parts.url = "github:hercules-ci/flake-parts";
lean.url = "github:leanprover/lean4?ref=v4.1.0"; lean.url = "github:leanprover/lean4?ref=f70895ede54501adf0db77474f452a7fef40d0b3";
}; };
outputs = inputs @ { outputs = inputs @ {
@ -28,9 +28,10 @@
src = ./.; src = ./.;
}; };
in rec { in rec {
packages = project // { packages = {
inherit leanPkgs; inherit (leanPkgs) lean lean-all;
default = packages.executable; inherit (project) sharedLib executable;
default = project.executable;
}; };
devShells.default = project.devShell; devShells.default = project.devShell;
}; };

View File

@ -1,12 +1,14 @@
{"version": 6, {"version": 7,
"packagesDir": "lake-packages", "packagesDir": ".lake/packages",
"packages": "packages":
[{"git": [{"url": "https://github.com/lurk-lab/LSpec.git",
{"url": "https://github.com/lurk-lab/LSpec.git", "type": "git",
"subDir?": null, "subDir": null,
"rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41", "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
"opts": {}, "name": "LSpec",
"name": "LSpec", "manifestFile": "lake-manifest.json",
"inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41", "inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
"inherited": false}}], "inherited": false,
"name": "pantograph"} "configFile": "lakefile.lean"}],
"name": "pantograph",
"lakeDir": ".lake"}

View File

@ -4,6 +4,7 @@ open Lake DSL
package pantograph package pantograph
lean_lib Pantograph { lean_lib Pantograph {
defaultFacets := #[LeanLib.sharedFacet]
} }
@[default_target] @[default_target]
@ -14,7 +15,7 @@ lean_exe pantograph {
} }
require LSpec from git require LSpec from git
"https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41" "https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
lean_lib Test { lean_lib Test {
} }
lean_exe test { lean_exe test {

View File

@ -1 +1 @@
leanprover/lean4:4.1.0 leanprover/lean4:4.7.0-rc2