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

Merge pull request 'chore: Update Lean to v4.12.0' (#108) from misc/version into dev 

Reviewed-on: #108
This commit is contained in:
Leni Aniva 2024-10-08 09:49:08 -07:00
parent 9119f47a8f 2e1276c21c
commit 1f4f2d7d6d
8 changed files with 68 additions and 129 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Pantograph/Expr.lean
View File

@ -1,4 +1,5 @@
import Lean import Lean
import Std.Data.HashMap
open Lean open Lean
@ -144,10 +145,10 @@ def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := d
assert! args.size ≥ decl.fvars.size assert! args.size ≥ decl.fvars.size
assert! !(← mvarIdPending.isAssigned) assert! !(← mvarIdPending.isAssigned)
assert! !(← mvarIdPending.isDelayedAssigned) assert! !(← mvarIdPending.isDelayedAssigned)
let fvarArgMap: HashMap FVarId Expr := HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList let fvarArgMap: Std.HashMap FVarId Expr := Std.HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
let fvarId := localDecl.fvarId let fvarId := localDecl.fvarId
let a := fvarArgMap.find? fvarId let a := fvarArgMap[fvarId]?
return acc ++ [(fvarId, a)] return acc ++ [(fvarId, a)]
assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome) assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)

13
Pantograph/Frontend/MetaTranslate.lean
View File

@ -1,4 +1,5 @@
import Lean.Meta import Lean.Meta
import Std.Data.HashMap
open Lean open Lean
@ -10,12 +11,12 @@ structure Context where
sourceMCtx : MetavarContext := {} sourceMCtx : MetavarContext := {}
sourceLCtx : LocalContext := {} sourceLCtx : LocalContext := {}
abbrev FVarMap := HashMap FVarId FVarId abbrev FVarMap := Std.HashMap FVarId FVarId
structure State where structure State where
-- Stores mapping from old to new mvar/fvars -- Stores mapping from old to new mvar/fvars
mvarMap: HashMap MVarId MVarId := {} mvarMap: Std.HashMap MVarId MVarId := {}
fvarMap: HashMap FVarId FVarId := {} fvarMap: Std.HashMap FVarId FVarId := {}
/- /-
Monadic state for translating a frozen meta state. The underlying `MetaM` Monadic state for translating a frozen meta state. The underlying `MetaM`
@ -46,13 +47,13 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
let state ← get let state ← get
match e with match e with
| .fvar fvarId => | .fvar fvarId =>
let .some fvarId' := state.fvarMap.find? fvarId | panic! s!"FVar id not registered: {fvarId.name}" let .some fvarId' := state.fvarMap[fvarId]? | panic! s!"FVar id not registered: {fvarId.name}"
assert! (← getLCtx).contains fvarId' assert! (← getLCtx).contains fvarId'
return .done $ .fvar fvarId' return .done $ .fvar fvarId'
| .mvar mvarId => do | .mvar mvarId => do
assert! !(sourceMCtx.dAssignment.contains mvarId) assert! !(sourceMCtx.dAssignment.contains mvarId)
assert! !(sourceMCtx.eAssignment.contains mvarId) assert! !(sourceMCtx.eAssignment.contains mvarId)
match state.mvarMap.find? mvarId with match state.mvarMap[mvarId]? with
| .some mvarId' => do | .some mvarId' => do
return .done $ .mvar mvarId' return .done $ .mvar mvarId'
| .none => do | .none => do
@ -92,7 +93,7 @@ partial def translateLCtx : MetaTranslateM LocalContext := do
) lctx ) lctx
partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
if let .some mvarId' := (← get).mvarMap.find? srcMVarId then if let .some mvarId' := (← get).mvarMap[srcMVarId]? then
return mvarId' return mvarId'
let mvar ← Meta.withLCtx .empty #[] do let mvar ← Meta.withLCtx .empty #[] do
let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get! let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!

25
Repl.lean
View File

@ -1,4 +1,4 @@
import Lean.Data.HashMap import Std.Data.HashMap
import Pantograph import Pantograph
namespace Pantograph.Repl namespace Pantograph.Repl
@ -10,7 +10,7 @@ structure Context where
structure State where structure State where
options: Protocol.Options := {} options: Protocol.Options := {}
nextId: Nat := 0 nextId: Nat := 0
goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty
/-- Main state monad for executing commands -/ /-- Main state monad for executing commands -/
abbrev MainM := ReaderT Context (StateT State Lean.CoreM) abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
@ -66,7 +66,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
let state ← get let state ← get
let nGoals := state.goalStates.size let nGoals := state.goalStates.size
set { state with nextId := 0, goalStates := Lean.HashMap.empty } set { state with nextId := 0, goalStates := .empty }
return .ok { nGoals } return .ok { nGoals }
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
let state ← get let state ← get
@ -119,7 +119,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
return .ok { stateId, root := goalState.root.name.toString } return .ok { stateId, root := goalState.root.name.toString }
goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
let state ← get let state ← get
let .some goalState := state.goalStates.find? args.stateId | let .some goalState := state.goalStates[args.stateId]? |
return .error $ errorIndex s!"Invalid state index {args.stateId}" return .error $ errorIndex s!"Invalid state index {args.stateId}"
let .some goal := goalState.goals.get? args.goalId | let .some goal := goalState.goals.get? args.goalId |
return .error $ errorIndex s!"Invalid goal index {args.goalId}" return .error $ errorIndex s!"Invalid goal index {args.goalId}"
@ -146,12 +146,15 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .ok (.success nextGoalState) => do | .ok (.success nextGoalState) => do
let nextGoalState ← match state.options.automaticMode, args.conv? with let nextGoalState ← match state.options.automaticMode, args.conv? with
| true, .none => do | true, .none => do
let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) | throwError "Resuming known goals" let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
throwError "Resuming known goals"
pure result pure result
| true, .some true => pure nextGoalState | true, .some true => pure nextGoalState
| true, .some false => do | true, .some false => do
let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail" let .some (_, _, dormantGoals) := goalState.convMVar? |
let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) | throwError "Resuming known goals" throwError "If conv exit succeeded this should not fail"
let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) |
throwError "Resuming known goals"
pure result pure result
| false, _ => pure nextGoalState | false, _ => pure nextGoalState
let nextStateId ← newGoalState nextGoalState let nextStateId ← newGoalState nextGoalState
@ -168,10 +171,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
return .ok { tacticErrors? := .some messages } return .ok { tacticErrors? := .some messages }
goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
let state ← get let state ← get
let .some target := state.goalStates.find? args.target | return .error $ errorIndex s!"Invalid state index {args.target}" let .some target := state.goalStates[args.target]? |
return .error $ errorIndex s!"Invalid state index {args.target}"
let nextState? ← match args.branch?, args.goals? with let nextState? ← match args.branch?, args.goals? with
| .some branchId, .none => do | .some branchId, .none => do
match state.goalStates.find? branchId with match state.goalStates[branchId]? with
| .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 =>
@ -197,7 +201,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
return .ok {} return .ok {}
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
let state ← get let state ← get
let .some goalState := state.goalStates.find? args.stateId | return .error $ errorIndex s!"Invalid state index {args.stateId}" let .some goalState := state.goalStates[args.stateId]? |
return .error $ errorIndex s!"Invalid state index {args.stateId}"
let result ← runMetaInMainM <| goalPrint goalState state.options let result ← runMetaInMainM <| goalPrint goalState state.options
return .ok result return .ok result
frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do

135
flake.lock
View File

@ -36,111 +36,74 @@
"lean": { "lean": {
"inputs": { "inputs": {
"flake-utils": "flake-utils", "flake-utils": "flake-utils",
"lean4-mode": "lean4-mode", "nixpkgs": "nixpkgs",
"nix": "nix", "nixpkgs-cadical": "nixpkgs-cadical",
"nixpkgs": "nixpkgs_2",
"nixpkgs-old": "nixpkgs-old" "nixpkgs-old": "nixpkgs-old"
}, },
"locked": { "locked": {
"lastModified": 1719788866, "lastModified": 1727749878,
"narHash": "sha256-kB2cp1XJKODXiuiKp7J5OK+PFP+sOSBE5gdVNOKWCPI=", "narHash": "sha256-O2Egyh2D0TfQWzQKfHUeAh7qAjMfeLVwXwGUw5QqcvE=",
"owner": "leanprover", "owner": "leanprover",
"repo": "lean4", "repo": "lean4",
"rev": "3b58e0649156610ce3aeed4f7b5c652340c668d4", "rev": "dc2533473114eb8656439ff2b9335209784aa640",
"type": "github" "type": "github"
}, },
"original": { "original": {
"owner": "leanprover", "owner": "leanprover",
"ref": "v4.10.0-rc1", "ref": "v4.12.0",
"repo": "lean4", "repo": "lean4",
"type": "github" "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"
}
},
"lspec": { "lspec": {
"flake": false, "flake": false,
"locked": { "locked": {
"lastModified": 1722857503, "lastModified": 1728279187,
"narHash": "sha256-F9uaymiw1wTCLrJm4n1Bpk3J8jW6poedQzvnnQlZ6Kw=", "narHash": "sha256-ZMqbvCqR/gHXRuIkuo7b0Yp9N1vOQR7xnrcy/SeIBoQ=",
"owner": "lurk-lab", "owner": "argumentcomputer",
"repo": "LSpec", "repo": "LSpec",
"rev": "8a51034d049c6a229d88dd62f490778a377eec06", "rev": "504a8cecf8da601b9466ac727aebb6b511aae4ab",
"type": "github" "type": "github"
}, },
"original": { "original": {
"owner": "lurk-lab", "owner": "argumentcomputer",
"ref": "8a51034d049c6a229d88dd62f490778a377eec06", "ref": "504a8cecf8da601b9466ac727aebb6b511aae4ab",
"repo": "LSpec", "repo": "LSpec",
"type": "github" "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": { "nixpkgs": {
"locked": { "locked": {
"lastModified": 1653988320, "lastModified": 1686089707,
"narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=", "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
"owner": "NixOS", "owner": "NixOS",
"repo": "nixpkgs", "repo": "nixpkgs",
"rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1", "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
"type": "github" "type": "github"
}, },
"original": { "original": {
"owner": "NixOS", "owner": "NixOS",
"ref": "nixos-22.05-small", "ref": "nixpkgs-unstable",
"repo": "nixpkgs", "repo": "nixpkgs",
"type": "github" "type": "github"
} }
}, },
"nixpkgs-cadical": {
"locked": {
"lastModified": 1722221733,
"narHash": "sha256-sga9SrrPb+pQJxG1ttJfMPheZvDOxApFfwXCFO0H9xw=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "12bf09802d77264e441f48e25459c10c93eada2e",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "12bf09802d77264e441f48e25459c10c93eada2e",
"type": "github"
}
},
"nixpkgs-lib": { "nixpkgs-lib": {
"locked": { "locked": {
"dir": "lib", "dir": "lib",
@ -176,39 +139,7 @@
"type": "github" "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": { "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": { "locked": {
"lastModified": 1711703276, "lastModified": 1711703276,
"narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=", "narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=",
@ -229,7 +160,7 @@
"flake-parts": "flake-parts", "flake-parts": "flake-parts",
"lean": "lean", "lean": "lean",
"lspec": "lspec", "lspec": "lspec",
"nixpkgs": "nixpkgs_3" "nixpkgs": "nixpkgs_2"
} }
} }
}, },

6
flake.nix
View File

@ -6,10 +6,10 @@
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.10.0-rc1"; url = "github:leanprover/lean4?ref=v4.12.0";
}; };
lspec = { lspec = {
url = "github:lurk-lab/LSpec?ref=8a51034d049c6a229d88dd62f490778a377eec06"; url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
flake = false; flake = false;
}; };
}; };
@ -29,7 +29,7 @@
"x86_64-darwin" "x86_64-darwin"
]; ];
perSystem = { system, pkgs, ... }: let perSystem = { system, pkgs, ... }: let
leanPkgs = lean.packages.${system}; leanPkgs = lean.packages.${system}.deprecated;
lspecLib = leanPkgs.buildLeanPackage { lspecLib = leanPkgs.buildLeanPackage {
name = "LSpec"; name = "LSpec";
roots = [ "Main" "LSpec" ]; roots = [ "Main" "LSpec" ];

9
lake-manifest.json
View File

@ -1,13 +1,14 @@
{"version": 7, {"version": "1.1.0",
"packagesDir": ".lake/packages", "packagesDir": ".lake/packages",
"packages": "packages":
[{"url": "https://github.com/lurk-lab/LSpec.git", [{"url": "https://github.com/lenianiva/LSpec.git",
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114", "scope": "",
"rev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
"name": "LSpec", "name": "LSpec",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114", "inputRev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
"inherited": false, "inherited": false,
"configFile": "lakefile.lean"}], "configFile": "lakefile.lean"}],
"name": "pantograph", "name": "pantograph",

2
lakefile.lean
View File

@ -18,7 +18,7 @@ lean_exe repl {
} }
require LSpec from git require LSpec from git
"https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114" "https://github.com/lenianiva/LSpec.git" @ "c492cecd0bc473e2f9c8b94d545d02cc0056034f"
lean_lib Test { lean_lib Test {
} }
@[test_driver] @[test_driver]

2
lean-toolchain
View File

@ -1 +1 @@
leanprover/lean4:v4.10.0-rc1 leanprover/lean4:v4.12.0