chore: Update Lean to v4.14.0 #134
|
@ -67,7 +67,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
|
|||
let s := (← get).commandState
|
||||
let before := s.env
|
||||
let done ← Elab.Frontend.processCommand
|
||||
let stx := (← get).commands.back
|
||||
let stx := (← get).commands.back!
|
||||
let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos
|
||||
let s' := (← get).commandState
|
||||
let after := s'.env
|
||||
|
|
|
@ -80,10 +80,10 @@ def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
|
|||
|
||||
@[export pantograph_frontend_collect_tactics_from_compilation_step_m]
|
||||
def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
|
||||
let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ
|
||||
let tacticInfoTrees := step.trees.flatMap λ tree => tree.filter λ
|
||||
| info@(.ofTacticInfo _) => info.isOriginal
|
||||
| _ => false
|
||||
let tactics := tacticInfoTrees.bind collectTactics
|
||||
let tactics := tacticInfoTrees.flatMap collectTactics
|
||||
tactics.mapM λ invocation => do
|
||||
let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
|
||||
let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
|
||||
|
@ -131,7 +131,7 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
|
|||
-- NOTE: Plural deliberately not spelled "sorries"
|
||||
@[export pantograph_frontend_collect_sorrys_m]
|
||||
def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
|
||||
return (← step.trees.mapM collectSorrysInTree).join
|
||||
return (← step.trees.mapM collectSorrysInTree).flatten
|
||||
|
||||
structure AnnotatedGoalState where
|
||||
state : GoalState
|
||||
|
@ -155,7 +155,7 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState
|
|||
let range := stxByteRange tacticInfo.stx
|
||||
return mvarIds.map (·, range)
|
||||
| _ => panic! "Invalid info"
|
||||
let annotatedGoals := List.join (← goalsM.run {} |>.run' {})
|
||||
let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
|
||||
let goals := annotatedGoals.map Prod.fst
|
||||
let srcBoundaries := annotatedGoals.map Prod.snd
|
||||
let root := match goals with
|
||||
|
|
|
@ -87,9 +87,9 @@ partial def InfoTree.filter (p : Info → Bool) (m : MVarId → Bool := fun _ =>
|
|||
| .context ctx tree => tree.filter p m |>.map (.context ctx)
|
||||
| .node info children =>
|
||||
if p info then
|
||||
[.node info (children.toList.map (filter p m)).join.toPArray']
|
||||
[.node info (children.toList.map (filter p m)).flatten.toPArray']
|
||||
else
|
||||
(children.toList.map (filter p m)).join
|
||||
(children.toList.map (filter p m)).flatten
|
||||
| .hole mvar => if m mvar then [.hole mvar] else []
|
||||
|
||||
/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
|
||||
|
@ -103,7 +103,7 @@ partial def InfoTree.findAllInfo
|
|||
| .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred
|
||||
| .node i children =>
|
||||
let head := if pred i then [(i, context?, children)] else []
|
||||
let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred)
|
||||
let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.flatMap (fun t => findAllInfo t context? haltOnMatch pred)
|
||||
head ++ tail
|
||||
| _ => []
|
||||
|
||||
|
@ -119,7 +119,7 @@ partial def InfoTree.findAllInfoM [Monad m]
|
|||
let (flagCollect, flagRecurse) ← pred i context?
|
||||
let head := if flagCollect then [(i, context?, children)] else []
|
||||
let tail := if ¬ flagRecurse then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? pred)
|
||||
return head ++ (← tail).join
|
||||
return head ++ (← tail).flatten
|
||||
| _ => return []
|
||||
|
||||
@[export pantograph_infotree_to_string_m]
|
||||
|
|
|
@ -561,10 +561,10 @@ def test_nat_zero_add: TestM Unit := do
|
|||
return ()
|
||||
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
|
||||
#[
|
||||
buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
|
||||
buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
|
||||
buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
|
||||
buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
|
||||
buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"),
|
||||
buildNamedGoal "_uniq.72" [("n", "Nat")] "Nat",
|
||||
buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
|
||||
buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit")
|
||||
])
|
||||
|
||||
let tactic := "exact n"
|
||||
|
@ -647,13 +647,13 @@ def test_nat_zero_add_alt: TestM Unit := do
|
|||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let major := "_uniq.68"
|
||||
let major := "_uniq.72"
|
||||
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
|
||||
#[
|
||||
buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
|
||||
buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"),
|
||||
buildNamedGoal major [("n", "Nat")] "Nat",
|
||||
buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
|
||||
buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
|
||||
buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
|
||||
buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit")
|
||||
])
|
||||
|
||||
let tactic := "intro x"
|
||||
|
@ -670,7 +670,7 @@ def test_nat_zero_add_alt: TestM Unit := do
|
|||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
|
||||
let (eqL, eqR, eqT) := ("_uniq.92", "_uniq.93", "_uniq.91")
|
||||
addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
|
||||
let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
|
||||
let state2b ← match state3m2.resume [conduit] with
|
||||
|
@ -681,16 +681,16 @@ def test_nat_zero_add_alt: TestM Unit := do
|
|||
|
||||
let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
|
||||
let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
|
||||
let fvN := "_uniq.63"
|
||||
let fvN := "_uniq.67"
|
||||
let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
|
||||
let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
|
||||
addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
|
||||
#[
|
||||
{
|
||||
name := "_uniq.70",
|
||||
name := "_uniq.74",
|
||||
userName? := .some "conduit",
|
||||
target := {
|
||||
pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)",
|
||||
pp? := .some "(?m.96 ?m.72 = ?m.98 ?m.72) = (n + 0 = n)",
|
||||
sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
|
||||
},
|
||||
vars := #[{
|
||||
|
|
|
@ -40,7 +40,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
|
|||
"Nat → Prop",
|
||||
"Nat",
|
||||
"∀ (t : Nat), Nat.below t → ?motive t",
|
||||
"?motive ?m.67 = (n + 0 = n)",
|
||||
"?motive ?m.71 = (n + 0 = n)",
|
||||
])
|
||||
addTest test
|
||||
|
||||
|
@ -83,7 +83,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
|
|||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let tactic := Tactic.evalMotivatedApply recursor
|
||||
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
||||
let majorId := 67
|
||||
let majorId := 71
|
||||
addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
||||
[
|
||||
"Nat → Prop",
|
||||
|
@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
|
|||
|
||||
addTest $ ← conduit.withContext do
|
||||
let t := toString (← Meta.ppExpr $ ← conduit.getType)
|
||||
return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")
|
||||
return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.146 ?m.{majorId}) = (n + 0 = n)")
|
||||
|
||||
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||
[
|
||||
|
|
|
@ -42,15 +42,16 @@
|
|||
"nixpkgs": "nixpkgs"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1731711316,
|
||||
"narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
|
||||
"lastModified": 1733351931,
|
||||
"narHash": "sha256-ngMjY/ci6490G2gofaS9CODtpnmFoYzfaI13U14TkFM=",
|
||||
"owner": "lenianiva",
|
||||
"repo": "lean4-nix",
|
||||
"rev": "136fc6057c48de970579e960b62421e9c295b67d",
|
||||
"rev": "157c85903f668fadeb79f330961b7bbe5ee596de",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "lenianiva",
|
||||
"ref": "157c85903f668fadeb79f330961b7bbe5ee596de",
|
||||
"repo": "lean4-nix",
|
||||
"type": "github"
|
||||
}
|
||||
|
|
31
flake.nix
31
flake.nix
|
@ -4,7 +4,7 @@
|
|||
inputs = {
|
||||
nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
|
||||
flake-parts.url = "github:hercules-ci/flake-parts";
|
||||
lean4-nix.url = "github:lenianiva/lean4-nix";
|
||||
lean4-nix.url = "github:lenianiva/lean4-nix?ref=157c85903f668fadeb79f330961b7bbe5ee596de";
|
||||
lspec = {
|
||||
url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
|
||||
flake = false;
|
||||
|
@ -28,6 +28,21 @@
|
|||
"x86_64-darwin"
|
||||
];
|
||||
perSystem = { system, pkgs, ... }: let
|
||||
pkgs = import nixpkgs {
|
||||
inherit system;
|
||||
overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
|
||||
};
|
||||
systems = [
|
||||
"aarch64-linux"
|
||||
"aarch64-darwin"
|
||||
"x86_64-linux"
|
||||
"x86_64-darwin"
|
||||
];
|
||||
perSystem = {
|
||||
system,
|
||||
pkgs,
|
||||
...
|
||||
}: let
|
||||
pkgs = import nixpkgs {
|
||||
inherit system;
|
||||
overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
|
||||
|
@ -43,9 +58,9 @@
|
|||
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
|
||||
src = ./.;
|
||||
filter = path: type:
|
||||
!(pkgs.lib.hasInfix "/Test/" path) &&
|
||||
!(pkgs.lib.hasSuffix ".md" path) &&
|
||||
!(pkgs.lib.hasSuffix "Repl.lean" path);
|
||||
!(pkgs.lib.hasInfix "/Test/" path)
|
||||
&& !(pkgs.lib.hasSuffix ".md" path)
|
||||
&& !(pkgs.lib.hasSuffix "Repl.lean" path);
|
||||
});
|
||||
};
|
||||
repl = pkgs.lean.buildLeanPackage {
|
||||
|
@ -55,8 +70,8 @@
|
|||
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
|
||||
src = ./.;
|
||||
filter = path: type:
|
||||
!(pkgs.lib.hasInfix "/Test/" path) &&
|
||||
!(pkgs.lib.hasSuffix ".md" path);
|
||||
!(pkgs.lib.hasInfix "/Test/" path)
|
||||
&& !(pkgs.lib.hasSuffix ".md" path);
|
||||
});
|
||||
};
|
||||
test = pkgs.lean.buildLeanPackage {
|
||||
|
@ -79,12 +94,14 @@
|
|||
inherit (repl) executable;
|
||||
default = repl.executable;
|
||||
};
|
||||
formatter = pkgs.alejandra;
|
||||
legacyPackages = {
|
||||
inherit project;
|
||||
leanPkgs = pkgs.lean;
|
||||
};
|
||||
checks = {
|
||||
test = pkgs.runCommand "test" {
|
||||
test =
|
||||
pkgs.runCommand "test" {
|
||||
buildInputs = [test.executable pkgs.lean.lean-all];
|
||||
} ''
|
||||
#export LEAN_SRC_PATH="${./.}"
|
||||
|
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:v4.12.0
|
||||
leanprover/lean4:v4.14.0
|
||||
|
|
Loading…
Reference in New Issue