Skip to content

Commit 8535dda

Browse files
author
Huub Vromen
committed
Switch to official Mathlib repository for reproducibility
1 parent 7a916d3 commit 8535dda

File tree

2 files changed

+3
-4
lines changed

2 files changed

+3
-4
lines changed

lake-manifest.json

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,11 @@
11
{"version": "1.1.0",
22
"packagesDir": ".lake/packages",
33
"packages":
4-
[{"url":
5-
"file:///Users/huubvromen/nextcloud/Leanprojects/SharedMathlib/mathlib4",
4+
[{"url": "https://github.com/leanprover-community/mathlib4.git",
65
"type": "git",
76
"subDir": null,
87
"scope": "",
9-
"rev": "5f59d4ede9239e86ab55064fd38b381cddc5a6d5",
8+
"rev": "4eb9bc7aa8fa0750e90c05d945d0d78b6d7e7d1f",
109
"name": "mathlib",
1110
"manifestFile": "lake-manifest.json",
1211
"inputRev": null,

lakefile.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ open Lake DSL
44
package Lewis
55

66
require mathlib from git
7-
"file:///Users/huubvromen/nextcloud/Leanprojects/SharedMathlib/mathlib4"
7+
"https://github.com/leanprover-community/mathlib4.git"
88

99
@[default_target]
1010
lean_lib Lewis

0 commit comments

Comments
 (0)