doc: README.md fix #73
|
@ -81,6 +81,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
|
||||
printExprPretty := args.printExprPretty?.getD options.printExprPretty,
|
||||
printExprAST := args.printExprAST?.getD options.printExprAST,
|
||||
printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars,
|
||||
noRepeat := args.noRepeat?.getD options.noRepeat,
|
||||
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
|
||||
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
|
||||
|
|
|
@ -90,7 +90,7 @@ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax
|
|||
Elab.Tactic.evalTactic stx
|
||||
if (← getThe Core.State).messages.hasErrors then
|
||||
let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
|
||||
let errors ← (messages.map Message.data).mapM fun md => md.toString
|
||||
let errors ← (messages.map (·.data)).mapM fun md => md.toString
|
||||
return .error errors
|
||||
else
|
||||
return .ok (← MonadBacktrack.saveState)
|
||||
|
@ -161,7 +161,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
|
|||
goal.assign expr
|
||||
if (← getThe Core.State).messages.hasErrors then
|
||||
let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
|
||||
let errors ← (messages.map Message.data).mapM fun md => md.toString
|
||||
let errors ← (messages.map (·.data)).mapM fun md => md.toString
|
||||
return .failure errors
|
||||
let prevMCtx := state.savedState.term.meta.meta.mctx
|
||||
let nextMCtx ← getMCtx
|
||||
|
|
|
@ -82,23 +82,6 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
|
|||
def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
|
||||
Environment.catalog ({}: Protocol.EnvCatalog)
|
||||
|
||||
@[export pantograph_mk_options]
|
||||
def mkOptions
|
||||
(printJsonPretty: Bool)
|
||||
(printExprPretty: Bool)
|
||||
(printExprAST: Bool)
|
||||
(noRepeat: Bool)
|
||||
(printAuxDecls: Bool)
|
||||
(printImplementationDetailHyps: Bool)
|
||||
: Protocol.Options := {
|
||||
printJsonPretty,
|
||||
printExprPretty,
|
||||
printExprAST,
|
||||
noRepeat,
|
||||
printAuxDecls,
|
||||
printImplementationDetailHyps,
|
||||
}
|
||||
|
||||
@[export pantograph_env_inspect_m]
|
||||
def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
|
||||
Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) :=
|
||||
|
|
|
@ -42,16 +42,16 @@
|
|||
"nixpkgs-old": "nixpkgs-old"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1711508550,
|
||||
"narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=",
|
||||
"lastModified": 1714704934,
|
||||
"narHash": "sha256-q0kLyIahUXolkSrBZSegPF+R99WAH1YC96JfKoFntDE=",
|
||||
"owner": "leanprover",
|
||||
"repo": "lean4",
|
||||
"rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
|
||||
"rev": "dcccfb73cb247e9478220375ab7de03f7c67e505",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "leanprover",
|
||||
"ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
|
||||
"ref": "v4.8.0-rc1",
|
||||
"repo": "lean4",
|
||||
"type": "github"
|
||||
}
|
||||
|
|
|
@ -5,8 +5,8 @@
|
|||
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
|
||||
flake-parts.url = "github:hercules-ci/flake-parts";
|
||||
lean = {
|
||||
url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
|
||||
# Do not follow input's nixpkgs since it could cause build failures
|
||||
url = "github:leanprover/lean4?ref=v4.8.0-rc1";
|
||||
};
|
||||
lspec = {
|
||||
url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
|
||||
|
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:nightly-2024-03-27
|
||||
leanprover/lean4:v4.8.0-rc1
|
||||
|
|
Loading…
Reference in New Issue