Compare commits
5 Commits
dev
...
bug/incorr
Author | SHA1 | Date |
---|---|---|
Leni Aniva | 80f9aa3269 | |
Leni Aniva | 5a05e9e8d4 | |
Leni Aniva | 48b924fae2 | |
Leni Aniva | fb3d36584f | |
Leni Aniva | 13dd11e995 |
|
@ -67,7 +67,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
|
||||||
let s := (← get).commandState
|
let s := (← get).commandState
|
||||||
let before := s.env
|
let before := s.env
|
||||||
let done ← Elab.Frontend.processCommand
|
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 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
|
||||||
|
|
|
@ -80,10 +80,10 @@ def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
|
||||||
|
|
||||||
@[export pantograph_frontend_collect_tactics_from_compilation_step_m]
|
@[export pantograph_frontend_collect_tactics_from_compilation_step_m]
|
||||||
def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
|
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
|
| info@(.ofTacticInfo _) => info.isOriginal
|
||||||
| _ => false
|
| _ => false
|
||||||
let tactics := tacticInfoTrees.bind collectTactics
|
let tactics := tacticInfoTrees.flatMap collectTactics
|
||||||
tactics.mapM λ invocation => do
|
tactics.mapM λ invocation => do
|
||||||
let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
|
let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
|
||||||
let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
|
let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
|
||||||
|
@ -106,7 +106,7 @@ structure InfoWithContext where
|
||||||
|
|
||||||
private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
|
private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
|
||||||
let infos ← t.findAllInfoM none fun i ctx? => match i with
|
let infos ← t.findAllInfoM none fun i ctx? => match i with
|
||||||
| .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do
|
| .ofTermInfo { expectedType?, expr, stx, lctx, isBinder := false, .. } => do
|
||||||
let .some ctx := ctx? | return (false, true)
|
let .some ctx := ctx? | return (false, true)
|
||||||
if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
|
if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
|
||||||
if expectedType?.isNone then
|
if expectedType?.isNone then
|
||||||
|
@ -131,7 +131,7 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
|
||||||
-- NOTE: Plural deliberately not spelled "sorries"
|
-- NOTE: Plural deliberately not spelled "sorries"
|
||||||
@[export pantograph_frontend_collect_sorrys_m]
|
@[export pantograph_frontend_collect_sorrys_m]
|
||||||
def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
|
def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
|
||||||
return (← step.trees.mapM collectSorrysInTree).join
|
return (← step.trees.mapM collectSorrysInTree).flatten
|
||||||
|
|
||||||
structure AnnotatedGoalState where
|
structure AnnotatedGoalState where
|
||||||
state : GoalState
|
state : GoalState
|
||||||
|
@ -155,7 +155,7 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState
|
||||||
let range := stxByteRange tacticInfo.stx
|
let range := stxByteRange tacticInfo.stx
|
||||||
return mvarIds.map (·, range)
|
return mvarIds.map (·, range)
|
||||||
| _ => panic! "Invalid info"
|
| _ => panic! "Invalid info"
|
||||||
let annotatedGoals := List.join (← goalsM.run {} |>.run' {})
|
let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
|
||||||
let goals := annotatedGoals.map Prod.fst
|
let goals := annotatedGoals.map Prod.fst
|
||||||
let srcBoundaries := annotatedGoals.map Prod.snd
|
let srcBoundaries := annotatedGoals.map Prod.snd
|
||||||
let root := match goals with
|
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)
|
| .context ctx tree => tree.filter p m |>.map (.context ctx)
|
||||||
| .node info children =>
|
| .node info children =>
|
||||||
if p info then
|
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
|
else
|
||||||
(children.toList.map (filter p m)).join
|
(children.toList.map (filter p m)).flatten
|
||||||
| .hole mvar => if m mvar then [.hole mvar] else []
|
| .hole mvar => if m mvar then [.hole mvar] else []
|
||||||
|
|
||||||
/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
|
/-- 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
|
| .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred
|
||||||
| .node i children =>
|
| .node i children =>
|
||||||
let head := if pred i then [(i, context?, children)] else []
|
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
|
head ++ tail
|
||||||
| _ => []
|
| _ => []
|
||||||
|
|
||||||
|
@ -119,7 +119,7 @@ partial def InfoTree.findAllInfoM [Monad m]
|
||||||
let (flagCollect, flagRecurse) ← pred i context?
|
let (flagCollect, flagRecurse) ← pred i context?
|
||||||
let head := if flagCollect then [(i, context?, children)] else []
|
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)
|
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 []
|
| _ => return []
|
||||||
|
|
||||||
@[export pantograph_infotree_to_string_m]
|
@[export pantograph_infotree_to_string_m]
|
||||||
|
|
|
@ -193,6 +193,15 @@ def mystery (k: Nat) : Nat := true
|
||||||
}
|
}
|
||||||
]
|
]
|
||||||
|
|
||||||
|
def test_capture_type_mismatch_in_binder : TestT MetaM Unit := do
|
||||||
|
let input := "
|
||||||
|
example (p: Prop) (h: (∀ (x: Prop), Nat) → p): p := h (λ (y: Nat) => 5)
|
||||||
|
"
|
||||||
|
let goalStates ← (collectSorrysFromSource input).run' {}
|
||||||
|
let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
|
||||||
|
checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[
|
||||||
|
]
|
||||||
|
|
||||||
def collectNewConstants (source: String) : MetaM (List (List Name)) := do
|
def collectNewConstants (source: String) : MetaM (List (List Name)) := do
|
||||||
let filename := "<anonymous>"
|
let filename := "<anonymous>"
|
||||||
let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
|
let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
|
||||||
|
@ -227,6 +236,7 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
|
||||||
("sorry_in_coupled", test_sorry_in_coupled),
|
("sorry_in_coupled", test_sorry_in_coupled),
|
||||||
("environment_capture", test_environment_capture),
|
("environment_capture", test_environment_capture),
|
||||||
("capture_type_mismatch", test_capture_type_mismatch),
|
("capture_type_mismatch", test_capture_type_mismatch),
|
||||||
|
("capture_type_mismatch_in_binder", test_capture_type_mismatch_in_binder),
|
||||||
("collect_one_constant", test_collect_one_constant),
|
("collect_one_constant", test_collect_one_constant),
|
||||||
("collect_one_theorem", test_collect_one_theorem),
|
("collect_one_theorem", test_collect_one_theorem),
|
||||||
]
|
]
|
||||||
|
|
|
@ -73,7 +73,7 @@ def test_tactic : Test :=
|
||||||
step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
|
step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
|
||||||
({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
|
({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
|
||||||
step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)]
|
step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)]
|
||||||
({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult),
|
({ parent? := .some { pp? := .some "fun x => ?m.11 x" }, }: Protocol.GoalPrintResult),
|
||||||
step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
|
step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
|
||||||
({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
|
({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
|
||||||
]
|
]
|
||||||
|
|
|
@ -561,10 +561,10 @@ def test_nat_zero_add: TestM Unit := do
|
||||||
return ()
|
return ()
|
||||||
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
|
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 "_uniq.68" [("n", "Nat")] "Nat",
|
buildNamedGoal "_uniq.72" [("n", "Nat")] "Nat",
|
||||||
buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
|
buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
|
||||||
buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
|
buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit")
|
||||||
])
|
])
|
||||||
|
|
||||||
let tactic := "exact n"
|
let tactic := "exact n"
|
||||||
|
@ -647,13 +647,13 @@ def test_nat_zero_add_alt: TestM Unit := do
|
||||||
| other => do
|
| other => do
|
||||||
addTest $ assertUnreachable $ other.toString
|
addTest $ assertUnreachable $ other.toString
|
||||||
return ()
|
return ()
|
||||||
let major := "_uniq.68"
|
let major := "_uniq.72"
|
||||||
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
|
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 major [("n", "Nat")] "Nat",
|
||||||
buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
|
buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
|
||||||
buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
|
buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit")
|
||||||
])
|
])
|
||||||
|
|
||||||
let tactic := "intro x"
|
let tactic := "intro x"
|
||||||
|
@ -670,7 +670,7 @@ def test_nat_zero_add_alt: TestM Unit := do
|
||||||
| other => do
|
| other => do
|
||||||
addTest $ assertUnreachable $ other.toString
|
addTest $ assertUnreachable $ other.toString
|
||||||
return ()
|
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]
|
addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
|
||||||
let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
|
let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
|
||||||
let state2b ← match state3m2.resume [conduit] with
|
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 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 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 conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
|
||||||
let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
|
let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
|
||||||
addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
|
addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
|
||||||
#[
|
#[
|
||||||
{
|
{
|
||||||
name := "_uniq.70",
|
name := "_uniq.74",
|
||||||
userName? := .some "conduit",
|
userName? := .some "conduit",
|
||||||
target := {
|
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})",
|
sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
|
||||||
},
|
},
|
||||||
vars := #[{
|
vars := #[{
|
||||||
|
|
|
@ -40,7 +40,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
|
||||||
"Nat → Prop",
|
"Nat → Prop",
|
||||||
"Nat",
|
"Nat",
|
||||||
"∀ (t : Nat), Nat.below t → ?motive t",
|
"∀ (t : Nat), Nat.below t → ?motive t",
|
||||||
"?motive ?m.67 = (n + 0 = n)",
|
"?motive ?m.71 = (n + 0 = n)",
|
||||||
])
|
])
|
||||||
addTest test
|
addTest test
|
||||||
|
|
||||||
|
@ -83,7 +83,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
|
||||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||||
let tactic := Tactic.evalMotivatedApply recursor
|
let tactic := Tactic.evalMotivatedApply recursor
|
||||||
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
||||||
let majorId := 67
|
let majorId := 71
|
||||||
addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
||||||
[
|
[
|
||||||
"Nat → Prop",
|
"Nat → Prop",
|
||||||
|
@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
|
||||||
|
|
||||||
addTest $ ← conduit.withContext do
|
addTest $ ← conduit.withContext do
|
||||||
let t := toString (← Meta.ppExpr $ ← conduit.getType)
|
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) :=
|
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||||
[
|
[
|
||||||
|
|
|
@ -42,15 +42,16 @@
|
||||||
"nixpkgs": "nixpkgs"
|
"nixpkgs": "nixpkgs"
|
||||||
},
|
},
|
||||||
"locked": {
|
"locked": {
|
||||||
"lastModified": 1731711316,
|
"lastModified": 1733351931,
|
||||||
"narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
|
"narHash": "sha256-ngMjY/ci6490G2gofaS9CODtpnmFoYzfaI13U14TkFM=",
|
||||||
"owner": "lenianiva",
|
"owner": "lenianiva",
|
||||||
"repo": "lean4-nix",
|
"repo": "lean4-nix",
|
||||||
"rev": "136fc6057c48de970579e960b62421e9c295b67d",
|
"rev": "157c85903f668fadeb79f330961b7bbe5ee596de",
|
||||||
"type": "github"
|
"type": "github"
|
||||||
},
|
},
|
||||||
"original": {
|
"original": {
|
||||||
"owner": "lenianiva",
|
"owner": "lenianiva",
|
||||||
|
"ref": "157c85903f668fadeb79f330961b7bbe5ee596de",
|
||||||
"repo": "lean4-nix",
|
"repo": "lean4-nix",
|
||||||
"type": "github"
|
"type": "github"
|
||||||
}
|
}
|
||||||
|
|
25
flake.nix
25
flake.nix
|
@ -4,7 +4,7 @@
|
||||||
inputs = {
|
inputs = {
|
||||||
nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
|
nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
|
||||||
flake-parts.url = "github:hercules-ci/flake-parts";
|
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 = {
|
lspec = {
|
||||||
url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
|
url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
|
||||||
flake = false;
|
flake = false;
|
||||||
|
@ -18,7 +18,8 @@
|
||||||
lean4-nix,
|
lean4-nix,
|
||||||
lspec,
|
lspec,
|
||||||
...
|
...
|
||||||
} : flake-parts.lib.mkFlake { inherit inputs; } {
|
}:
|
||||||
|
flake-parts.lib.mkFlake {inherit inputs;} {
|
||||||
flake = {
|
flake = {
|
||||||
};
|
};
|
||||||
systems = [
|
systems = [
|
||||||
|
@ -27,7 +28,11 @@
|
||||||
"x86_64-linux"
|
"x86_64-linux"
|
||||||
"x86_64-darwin"
|
"x86_64-darwin"
|
||||||
];
|
];
|
||||||
perSystem = { system, pkgs, ... }: let
|
perSystem = {
|
||||||
|
system,
|
||||||
|
pkgs,
|
||||||
|
...
|
||||||
|
}: let
|
||||||
pkgs = import nixpkgs {
|
pkgs = import nixpkgs {
|
||||||
inherit system;
|
inherit system;
|
||||||
overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
|
overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
|
||||||
|
@ -43,9 +48,9 @@
|
||||||
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
|
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
|
||||||
src = ./.;
|
src = ./.;
|
||||||
filter = path: type:
|
filter = path: type:
|
||||||
!(pkgs.lib.hasInfix "/Test/" path) &&
|
!(pkgs.lib.hasInfix "/Test/" path)
|
||||||
!(pkgs.lib.hasSuffix ".md" path) &&
|
&& !(pkgs.lib.hasSuffix ".md" path)
|
||||||
!(pkgs.lib.hasSuffix "Repl.lean" path);
|
&& !(pkgs.lib.hasSuffix "Repl.lean" path);
|
||||||
});
|
});
|
||||||
};
|
};
|
||||||
repl = pkgs.lean.buildLeanPackage {
|
repl = pkgs.lean.buildLeanPackage {
|
||||||
|
@ -55,8 +60,8 @@
|
||||||
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
|
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
|
||||||
src = ./.;
|
src = ./.;
|
||||||
filter = path: type:
|
filter = path: type:
|
||||||
!(pkgs.lib.hasInfix "/Test/" path) &&
|
!(pkgs.lib.hasInfix "/Test/" path)
|
||||||
!(pkgs.lib.hasSuffix ".md" path);
|
&& !(pkgs.lib.hasSuffix ".md" path);
|
||||||
});
|
});
|
||||||
};
|
};
|
||||||
test = pkgs.lean.buildLeanPackage {
|
test = pkgs.lean.buildLeanPackage {
|
||||||
|
@ -79,12 +84,14 @@
|
||||||
inherit (repl) executable;
|
inherit (repl) executable;
|
||||||
default = repl.executable;
|
default = repl.executable;
|
||||||
};
|
};
|
||||||
|
formatter = pkgs.alejandra;
|
||||||
legacyPackages = {
|
legacyPackages = {
|
||||||
inherit project;
|
inherit project;
|
||||||
leanPkgs = pkgs.lean;
|
leanPkgs = pkgs.lean;
|
||||||
};
|
};
|
||||||
checks = {
|
checks = {
|
||||||
test = pkgs.runCommand "test" {
|
test =
|
||||||
|
pkgs.runCommand "test" {
|
||||||
buildInputs = [test.executable pkgs.lean.lean-all];
|
buildInputs = [test.executable pkgs.lean.lean-all];
|
||||||
} ''
|
} ''
|
||||||
#export LEAN_SRC_PATH="${./.}"
|
#export LEAN_SRC_PATH="${./.}"
|
||||||
|
|
|
@ -1 +1 @@
|
||||||
leanprover/lean4:v4.12.0
|
leanprover/lean4:v4.14.0
|
||||||
|
|
Loading…
Reference in New Issue