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

feat: Condensed interface #85

Merged
aniva merged 27 commits from serial/expr into dev 2024-08-15 22:41:59 -07:00
Conversation 0 Commits 27 Files Changed 13 +11 -16
7 changed files with 11 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit a7fe7cbd7c - Show all commits

2
Pantograph/Compile/Frontend.lean
View File

@ -52,7 +52,7 @@ def processOneCommand: Elab.Frontend.FrontendM (CompilationStep × Bool) := do
let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos
let s' := (← get).commandState let s' := (← get).commandState
let after := s'.env let after := s'.env
let msgs := s'.messages.msgs.drop s.messages.msgs.size let msgs := s'.messages.toList.drop s.messages.toList.length
let trees := s'.infoState.trees.drop s.infoState.trees.size let trees := s'.infoState.trees.drop s.infoState.trees.size
let ⟨_, fileName, fileMap⟩ := (← read).inputCtx let ⟨_, fileName, fileMap⟩ := (← read).inputCtx
return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done) return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)

2
Pantograph/Environment.lean
View File

@ -132,7 +132,7 @@ def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) :
(hints := Lean.mkReducibilityHintsRegularEx 1) (hints := Lean.mkReducibilityHintsRegularEx 1)
(safety := Lean.DefinitionSafety.safe) (safety := Lean.DefinitionSafety.safe)
(all := []) (all := [])
let env' ← match env.addDecl constant with let env' ← match env.addDecl (← getOptions) constant with
| .error e => do | .error e => do
let options ← Lean.MonadOptions.getOptions let options ← Lean.MonadOptions.getOptions
let desc ← (e.toMessageData options).toString let desc ← (e.toMessageData options).toString

9
Pantograph/Goal.lean
View File

@ -7,11 +7,6 @@ import Pantograph.Protocol
import Pantograph.Tactic import Pantograph.Tactic
import Lean import Lean
def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
{
msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false
}
namespace Pantograph namespace Pantograph
open Lean open Lean
@ -186,7 +181,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.
try try
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.toArray
let errors ← (messages.map (·.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
@ -231,7 +226,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
goal.checkNotAssigned `GoalState.assign goal.checkNotAssigned `GoalState.assign
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.toArray
let errors ← (messages.map (·.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

2
Pantograph/Version.lean
View File

@ -1,6 +1,6 @@
namespace Pantograph namespace Pantograph
@[export pantograph_version] @[export pantograph_version]
def version := "0.2.16" def version := "0.2.17"
end Pantograph end Pantograph

8
flake.lock
View File

@ -42,16 +42,16 @@
"nixpkgs-old": "nixpkgs-old" "nixpkgs-old": "nixpkgs-old"
}, },
"locked": { "locked": {
"lastModified": 1714704934, "lastModified": 1719788866,
"narHash": "sha256-q0kLyIahUXolkSrBZSegPF+R99WAH1YC96JfKoFntDE=", "narHash": "sha256-kB2cp1XJKODXiuiKp7J5OK+PFP+sOSBE5gdVNOKWCPI=",
"owner": "leanprover", "owner": "leanprover",
"repo": "lean4", "repo": "lean4",
"rev": "dcccfb73cb247e9478220375ab7de03f7c67e505", "rev": "3b58e0649156610ce3aeed4f7b5c652340c668d4",
"type": "github" "type": "github"
}, },
"original": { "original": {
"owner": "leanprover", "owner": "leanprover",
"ref": "v4.8.0-rc1", "ref": "v4.10.0-rc1",
"repo": "lean4", "repo": "lean4",
"type": "github" "type": "github"
} }

2
flake.nix
View File

@ -6,7 +6,7 @@
flake-parts.url = "github:hercules-ci/flake-parts"; flake-parts.url = "github:hercules-ci/flake-parts";
lean = { lean = {
# 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"; url = "github:leanprover/lean4?ref=v4.10.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:v4.8.0-rc1 leanprover/lean4:v4.10.0-rc1