diff --git a/lake-manifest.json b/lake-manifest.json index 8121241..f5dda02 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -10,17 +10,7 @@ "manifestFile": "lake-manifest.json", "inputRev": "v4.28.0", "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/batteries.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0", - "inherited": false, - "configFile": "lakefile.toml"}], + "configFile": "lakefile.lean"}], "name": "raylean", "lakeDir": ".lake", "fixedToolchain": false} diff --git a/lakefile.lean b/lakefile.lean index 2df8865..63b2b75 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,8 +5,6 @@ def optionUseBundle : Bool := get_config? bundle == some "on" def optionDisableResvg : Bool := get_config? resvg == some "disable" -require batteries from git "https://github.com/leanprover-community/batteries.git" @ "v4.28.0" - require «lens-demo» from git "https://github.com/funexists/lens-demo.git" @ "v4.28.0" package raylean where