aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

feat: Elementarized tactics with motives, congruence, and absurdity #72

Merged
aniva merged 41 commits from goal/mapply into dev 2024-06-12 13:52:46 -07:00
Conversation 6 Commits 41 Files Changed 22 +10 -11
7 changed files with 10 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 4cff6677d2 - Show all commits

2
Pantograph.lean
View File

@ -87,7 +87,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
} }
} }
return .ok { } return .ok { }
options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.OptionsPrintResult) := do options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
return .ok (← get).options return .ok (← get).options
goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
let state ← get let state ← get

4
Pantograph/Goal.lean
View File

@ -169,7 +169,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.
let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
if (← getThe Core.State).messages.hasErrors then if (← getThe Core.State).messages.hasErrors then
let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray 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 return .failure errors
let nextElabState ← MonadBacktrack.saveState let nextElabState ← MonadBacktrack.saveState
let nextMCtx := nextElabState.meta.meta.mctx let nextMCtx := nextElabState.meta.meta.mctx
@ -214,7 +214,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
goal.assign expr goal.assign expr
if (← getThe Core.State).messages.hasErrors then if (← getThe Core.State).messages.hasErrors then
let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray 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 return .failure errors
let prevMCtx := state.savedState.term.meta.meta.mctx let prevMCtx := state.savedState.term.meta.meta.mctx
let nextMCtx ← getMCtx let nextMCtx ← getMCtx

1
Pantograph/Protocol.lean
View File

@ -193,7 +193,6 @@ structure OptionsSetResult where
deriving Lean.ToJson deriving Lean.ToJson
structure OptionsPrint where structure OptionsPrint where
deriving Lean.FromJson deriving Lean.FromJson
abbrev OptionsPrintResult := Options
structure GoalStart where structure GoalStart where
-- Only one of the fields below may be populated. -- Only one of the fields below may be populated.

2
Test/Integration.lean
View File

@ -65,7 +65,7 @@ def test_option_modify : IO LSpec.TestSeq :=
subroutine_step "options.print" subroutine_step "options.print"
[] []
(Lean.toJson ({ options with printExprAST := true }: (Lean.toJson ({ options with printExprAST := true }:
Protocol.OptionsPrintResult)) Protocol.Options))
] ]
def test_malformed_command : IO LSpec.TestSeq := def test_malformed_command : IO LSpec.TestSeq :=
let invalid := "invalid" let invalid := "invalid"

8
flake.lock
View File

@ -42,16 +42,16 @@
"nixpkgs-old": "nixpkgs-old" "nixpkgs-old": "nixpkgs-old"
}, },
"locked": { "locked": {
"lastModified": 1711508550, "lastModified": 1714704934,
"narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=", "narHash": "sha256-q0kLyIahUXolkSrBZSegPF+R99WAH1YC96JfKoFntDE=",
"owner": "leanprover", "owner": "leanprover",
"repo": "lean4", "repo": "lean4",
"rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2", "rev": "dcccfb73cb247e9478220375ab7de03f7c67e505",
"type": "github" "type": "github"
}, },
"original": { "original": {
"owner": "leanprover", "owner": "leanprover",
"ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2", "ref": "v4.8.0-rc1",
"repo": "lean4", "repo": "lean4",
"type": "github" "type": "github"
} }

2
flake.nix
View File

@ -5,8 +5,8 @@
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 = { lean = {
url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
# Do not follow input's nixpkgs since it could cause build failures # Do not follow input's nixpkgs since it could cause build failures
url = "github:leanprover/lean4?ref=v4.8.0-rc1";
}; };
lspec = { lspec = {
url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114"; url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";

2
lean-toolchain
View File

@ -1 +1 @@
leanprover/lean4:nightly-2024-03-27 leanprover/lean4:v4.8.0-rc1