Skip to content

Commit

Permalink
fix lake invocation with -R
Browse files Browse the repository at this point in the history
  • Loading branch information
bollu committed Nov 14, 2023
1 parent e6dd7a4 commit 379e58b
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 7 deletions.
6 changes: 3 additions & 3 deletions docgen.sh
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
set -o xtrace
set -e
lake -Kenv=dev update
lake exe cache get # load mathlib from cache
lake -R -Kenv=dev update
lake -R exe cache get # load mathlib from cache
# make a phony build/doc if doc-gen fails.
lake -Kenv=dev build SSA:docs || mkdir -p build/doc # Alive depends on SSA.
lake -R -Kenv=dev build SSA:docs || mkdir -p build/doc # Alive depends on SSA.
40 changes: 36 additions & 4 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,14 @@
"packagesDir": "lake-packages",
"packages":
[{"git":
{"url": "https://github.com/leanprover-community/mathlib4",
"subDir?": null,
"rev": "3b5350301929a51585dedea497e172a23e4a4485",
"opts": {},
"name": "mathlib",
"inputRev?": "bitvec-ring",
"inherited": false}},
{"git":
{"url": "https://github.com/mhuisi/lean4-cli.git",
"subDir?": null,
"rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
Expand All @@ -18,12 +26,12 @@
"inputRev?": "master",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover-community/mathlib4",
{"url": "https://github.com/leanprover/doc-gen4",
"subDir?": null,
"rev": "3b5350301929a51585dedea497e172a23e4a4485",
"rev": "8bccb92b531248af1b6692d65486e8640c8bcd10",
"opts": {},
"name": "mathlib",
"inputRev?": "bitvec-ring",
"name": "«doc-gen4»",
"inputRev?": "8bccb92b531248af1b6692d65486e8640c8bcd10",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover/std4",
Expand Down Expand Up @@ -56,5 +64,29 @@
"opts": {},
"name": "proofwidgets",
"inputRev?": "v0.0.21",
"inherited": true}},
{"git":
{"url": "https://github.com/xubaiw/CMark.lean",
"subDir?": null,
"rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
"opts": {},
"name": "CMark",
"inputRev?": "main",
"inherited": true}},
{"git":
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
"subDir?": null,
"rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32",
"opts": {},
"name": "«lean4-unicode-basic»",
"inputRev?": "main",
"inherited": true}},
{"git":
{"url": "https://github.com/hargonix/LeanInk",
"subDir?": null,
"rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
"opts": {},
"name": "leanInk",
"inputRev?": "doc-gen",
"inherited": true}}],
"name": "SSA"}

0 comments on commit 379e58b

Please sign in to comment.