fix: lake changed the build directory
Henrik Böving
parent
ca82b428ed
commit
b85fd6cbeb
|
|
@ -1,3 +1,3 @@
|
|||
/build
|
||||
/.lake/*
|
||||
/lake-packages/*
|
||||
lakefile.olean
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ namespace DocGen4.Output
|
|||
open scoped DocGen4.Jsx
|
||||
open Lean System Widget Elab Process
|
||||
|
||||
def basePath := FilePath.mk "." / "build" / "doc"
|
||||
def basePath := FilePath.mk "." / ".lake" / "build" / "doc"
|
||||
def srcBasePath := basePath / "src"
|
||||
def declarationsBasePath := basePath / "declarations"
|
||||
|
||||
|
|
|
|||
14
README.md
14
README.md
|
|
@ -27,11 +27,16 @@ lake -R -Kenv=dev build Test:docs Foo:docs
|
|||
Note that `doc-gen4` currently always generates documentation for `Lean`, `Init`
|
||||
and `Lake` in addition to the provided targets.
|
||||
|
||||
The root of the built docs will be `.lake/build/docs/index.html`. However, due to the "Same Origin Policy", the
|
||||
generated website will be partially broken if you just open the generated html files in your browser. You
|
||||
need to serve them from a proper http server for it to work. An easy way to do that is to run
|
||||
`python3 -m http.server` from the `.lake/build/docs` directory.
|
||||
|
||||
## Assumptions that `doc-gen4` makes
|
||||
The only requirement for the `lake -Kenv=dev build Test:docs` to work is that your
|
||||
target library builds, that is `lake build Test` exits without an error. If this requirement
|
||||
is not fulfilled, the documentation generation will fail and you will end up with
|
||||
partial build artefacts in `build/doc`. Note that `doc-gen4` is perfectly capable of
|
||||
partial build artefacts in `.lake/build/doc`. Note that `doc-gen4` is perfectly capable of
|
||||
generating documentation for Lean code that contains `sorry`, just not for code
|
||||
that doesn't compile.
|
||||
|
||||
|
|
@ -62,12 +67,7 @@ meta if get_config? env = some "dev" then -- dev is so not everyone has to build
|
|||
require «doc-gen4» from "../doc-gen4"
|
||||
```
|
||||
|
||||
The root of the built docs will be `build/docs/index.html`. However, due to the "Same Origin Policy", the
|
||||
generated website will be partially broken if you just open the generated html files in your browser. You
|
||||
need to serve them from a proper http server for it to work. An easy way to do that is to run
|
||||
`python3 -m http.server` from the `build/docs` directory.
|
||||
|
||||
Note that if you modify the `.js` or `.css` files in `doc-gen4`, they won't necessarily be copied over when
|
||||
you rebuild the documentation. You can manually copy the changes to the `build/docs` directory to make
|
||||
you rebuild the documentation. You can manually copy the changes to the `.lake/build/docs` directory to make
|
||||
sure the changes appear, or just do a full recompilation (`lake clean` and `lake build` inside the `doc-gen4`
|
||||
directory.)
|
||||
|
|
|
|||
|
|
@ -1,36 +1,41 @@
|
|||
{"version": 6,
|
||||
"packagesDir": "lake-packages",
|
||||
{"version": 7,
|
||||
"packagesDir": ".lake/packages",
|
||||
"packages":
|
||||
[{"git":
|
||||
{"url": "https://github.com/xubaiw/CMark.lean",
|
||||
"subDir?": null,
|
||||
"rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
|
||||
"opts": {},
|
||||
"name": "CMark",
|
||||
"inputRev?": "main",
|
||||
"inherited": false}},
|
||||
{"git":
|
||||
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
|
||||
"subDir?": null,
|
||||
"rev": "4ecf4f1f98d14d03a9e84fa1c082630fa69df88b",
|
||||
"opts": {},
|
||||
"name": "UnicodeBasic",
|
||||
"inputRev?": "main",
|
||||
"inherited": false}},
|
||||
{"git":
|
||||
{"url": "https://github.com/mhuisi/lean4-cli",
|
||||
"subDir?": null,
|
||||
"rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
|
||||
"opts": {},
|
||||
"name": "Cli",
|
||||
"inputRev?": "nightly",
|
||||
"inherited": false}},
|
||||
{"git":
|
||||
{"url": "https://github.com/hargonix/LeanInk",
|
||||
"subDir?": null,
|
||||
"rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
|
||||
"opts": {},
|
||||
"name": "leanInk",
|
||||
"inputRev?": "doc-gen",
|
||||
"inherited": false}}],
|
||||
"name": "«doc-gen4»"}
|
||||
[{"url": "https://github.com/xubaiw/CMark.lean",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
|
||||
"name": "CMark",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71",
|
||||
"name": "UnicodeBasic",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/mhuisi/lean4-cli",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
|
||||
"name": "Cli",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "nightly",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/hargonix/LeanInk",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
|
||||
"name": "leanInk",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "doc-gen",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"}],
|
||||
"name": "«doc-gen4»",
|
||||
"lakeDir": ".lake"}
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:v4.2.0-rc4
|
||||
leanprover/lean4:v4.3.0-rc2
|
||||
|
|
|
|||
Loading…
Reference in New Issue