Skip to content

Commit dc50f42

Browse files
committed
Fixed LSpec dependency
1 parent 694b3a9 commit dc50f42

File tree

2 files changed

+7
-5
lines changed

2 files changed

+7
-5
lines changed

analysis/markov/lake-manifest.json

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -21,20 +21,20 @@
2121
"inputRev": "26d5ce4d60195a869b1fdb100b442794ea63e1ad",
2222
"inherited": false,
2323
"configFile": "lakefile.toml"},
24-
{"url": "https://github.com/argumentcomputer/LSpec.git",
24+
{"url": "https://github.com/argumentcomputer/LSpec",
2525
"type": "git",
2626
"subDir": null,
2727
"scope": "",
28-
"rev": "d2bbbfa61a82ac199a5e852aa375acffd9a3b3f1",
28+
"rev": "24cceb69c20fadca0fd3acabe39fa9270dfb47e6",
2929
"name": "LSpec",
3030
"manifestFile": "lake-manifest.json",
31-
"inputRev": null,
31+
"inputRev": "24cceb69c20fadca0fd3acabe39fa9270dfb47e6",
3232
"inherited": false,
3333
"configFile": "lakefile.toml"},
3434
{"url": "https://github.com/leanprover-community/mathlib4",
3535
"type": "git",
3636
"subDir": null,
37-
"scope": "leanprover-community",
37+
"scope": "",
3838
"rev": "c211948581bde9846a99e32d97a03f0d5307c31e",
3939
"name": "mathlib",
4040
"manifestFile": "lake-manifest.json",

analysis/markov/lakefile.lean

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,8 @@ package «linleios» where
1010
`pp.unicode.fun, true⟩,
1111
-- disables automatic implicit arguments
1212
`autoImplicit, false⟩,
13+
-- suppresses the checkBinderAnnotations error/warning
14+
`checkBinderAnnotations, false⟩,
1315
]
1416
moreServerOptions := #[
1517
`trace.debug, true⟩,
@@ -32,7 +34,7 @@ require mathlib from git
3234
"https://github.com/leanprover-community/mathlib4" @ "v4.20.0"
3335

3436
require LSpec from git
35-
"https://github.com/argumentcomputer/LSpec.git"
37+
"https://github.com/argumentcomputer/LSpec" @ "24cceb69c20fadca0fd3acabe39fa9270dfb47e6"
3638

3739
require Parser from git
3840
"https://github.com/fgdorais/lean4-parser" @ "26d5ce4d60195a869b1fdb100b442794ea63e1ad"

0 commit comments

Comments
 (0)