From e75c008a471a29793ef323cd15ac1ae6258085df Mon Sep 17 00:00:00 2001 From: Sean McLaughlin Date: Fri, 15 Aug 2025 16:11:28 -0400 Subject: [PATCH] chore: remove spurious dependency --- lake-manifest.json | 14 ++------------ lakefile.lean | 3 --- 2 files changed, 2 insertions(+), 15 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 0188d99..071527d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,17 +1,7 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/import-graph.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "eb164a46de87078f27640ee71e6c3841defc2484", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", - "inherited": false, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli.git", + [{"url": "https://github.com/leanprover/lean4-cli.git", "type": "git", "subDir": null, "scope": "", @@ -44,7 +34,7 @@ {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "scope": "leanprover-community", + "scope": "", "rev": "e96b5eca4fcfe2e0e96a1511a6cd5747515aba82", "name": "batteries", "manifestFile": "lake-manifest.json", diff --git a/lakefile.lean b/lakefile.lean index 8a845f3..e3d9fbf 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -35,6 +35,3 @@ require plausible from git require Cli from git "https://github.com/leanprover/lean4-cli.git" @ "v4.22.0" - -require importGraph from git - "https://github.com/leanprover-community/import-graph.git" @ "v4.22.0"