From 8853b17fee59728700760eefbe1c1b8b079eb650 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 6 Mar 2024 15:14:08 -0800 Subject: [PATCH 1/4] test: More diagnostics for tests --- Pantograph/Goal.lean | 4 ++++ Pantograph/Protocol.lean | 2 +- Test/Integration.lean | 6 ++++++ 3 files changed, 11 insertions(+), 1 deletion(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 630637d..b56c893 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -225,6 +225,10 @@ protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do let expr := goalState.mctx.eAssignment.find! parent let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) return expr +protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do + let expr ← goalState.mctx.eAssignment.find? mvar + let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) + return expr end Pantograph diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 84e0cc2..a4983d9 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -242,7 +242,7 @@ structure GoalPrintResult where -- The root expression root?: Option Expression := .none -- The filling expression of the parent goal - parent?: Option Expression := .none + parent?: Option Expression deriving Lean.ToJson -- Diagnostic Options, not available in REPL diff --git a/Test/Integration.lean b/Test/Integration.lean index 0a6c210..8f3f217 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -103,6 +103,12 @@ def test_tactic : IO LSpec.TestSeq := goals? := #[goal1], }: Protocol.GoalTacticResult)), + subroutine_step "goal.print" + [("stateId", .num 1)] + (Lean.toJson ({ + parent? := .some { pp? := .some "fun x => ?m.11 x" }, + }: + Protocol.GoalPrintResult)), subroutine_step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")] (Lean.toJson ({ From 5c970bfeed203e3c747aaf159a987ff40be9e382 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 29 Mar 2024 23:50:30 -0700 Subject: [PATCH 2/4] fix: Lean build failure on macOS --- flake.lock | 22 ++++++++++++++++++---- flake.nix | 1 - 2 files changed, 18 insertions(+), 5 deletions(-) diff --git a/flake.lock b/flake.lock index f7f3012..61e8969 100644 --- a/flake.lock +++ b/flake.lock @@ -38,9 +38,7 @@ "flake-utils": "flake-utils", "lean4-mode": "lean4-mode", "nix": "nix", - "nixpkgs": [ - "nixpkgs" - ], + "nixpkgs": "nixpkgs_2", "nixpkgs-old": "nixpkgs-old" }, "locked": { @@ -195,6 +193,22 @@ } }, "nixpkgs_2": { + "locked": { + "lastModified": 1711715736, + "narHash": "sha256-9slQ609YqT9bT/MNX9+5k5jltL9zgpn36DpFB7TkttM=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "807c549feabce7eddbf259dbdcec9e0600a0660d", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixpkgs-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_3": { "locked": { "lastModified": 1697456312, "narHash": "sha256-roiSnrqb5r+ehnKCauPLugoU8S36KgmWraHgRqVYndo=", @@ -215,7 +229,7 @@ "flake-parts": "flake-parts", "lean": "lean", "lspec": "lspec", - "nixpkgs": "nixpkgs_2" + "nixpkgs": "nixpkgs_3" } } }, diff --git a/flake.nix b/flake.nix index fdb3f6b..583b1a8 100644 --- a/flake.nix +++ b/flake.nix @@ -6,7 +6,6 @@ flake-parts.url = "github:hercules-ci/flake-parts"; lean = { url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2"; - inputs.nixpkgs.follows = "nixpkgs"; }; lspec = { url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114"; From 08874d433f00e5914d701c2b8dcf4a48acb758b3 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 29 Mar 2024 23:59:14 -0700 Subject: [PATCH 3/4] fix: Update flake so lean builds on Darwin --- flake.lock | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/flake.lock b/flake.lock index 61e8969..39888a8 100644 --- a/flake.lock +++ b/flake.lock @@ -5,11 +5,11 @@ "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1696343447, - "narHash": "sha256-B2xAZKLkkeRFG5XcHHSXXcP7To9Xzr59KXeZiRf4vdQ=", + "lastModified": 1709336216, + "narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "c9afaba3dfa4085dbd2ccb38dfade5141e33d9d4", + "rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2", "type": "github" }, "original": { @@ -144,11 +144,11 @@ "nixpkgs-lib": { "locked": { "dir": "lib", - "lastModified": 1696019113, - "narHash": "sha256-X3+DKYWJm93DRSdC5M6K5hLqzSya9BjibtBsuARoPco=", + "lastModified": 1709237383, + "narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "f5892ddac112a1e9b3612c39af1b72987ee5783a", + "rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8", "type": "github" }, "original": { @@ -194,11 +194,11 @@ }, "nixpkgs_2": { "locked": { - "lastModified": 1711715736, - "narHash": "sha256-9slQ609YqT9bT/MNX9+5k5jltL9zgpn36DpFB7TkttM=", + "lastModified": 1686089707, + "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "807c549feabce7eddbf259dbdcec9e0600a0660d", + "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397", "type": "github" }, "original": { @@ -210,11 +210,11 @@ }, "nixpkgs_3": { "locked": { - "lastModified": 1697456312, - "narHash": "sha256-roiSnrqb5r+ehnKCauPLugoU8S36KgmWraHgRqVYndo=", + "lastModified": 1711703276, + "narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=", "owner": "nixos", "repo": "nixpkgs", - "rev": "ca012a02bf8327be9e488546faecae5e05d7d749", + "rev": "d8fe5e6c92d0d190646fb9f1056741a229980089", "type": "github" }, "original": { From 431bdab2361bdb295e8905eab60c53c5e5e6017f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 30 Mar 2024 00:03:37 -0700 Subject: [PATCH 4/4] doc: Reason why not to follow nixpkgs --- flake.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/flake.nix b/flake.nix index 583b1a8..2458805 100644 --- a/flake.nix +++ b/flake.nix @@ -6,6 +6,7 @@ flake-parts.url = "github:hercules-ci/flake-parts"; lean = { url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2"; + # Do not follow input's nixpkgs since it could cause build failures }; lspec = { url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";