From a5ad46f7becef9976152fdd50ac250ea53f96314 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 23 Nov 2020 18:42:24 +0100 Subject: [PATCH] feat: Nix: mdbook --- .github/workflows/ci.yml | 22 -------------------- .github/workflows/nix-ci.yml | 13 ++++++++++++ doc/mdbook.md | 9 ++++++-- flake.lock | 17 +++++++++++++++ flake.nix | 40 +++++++++++++++++++++++++++++++++++- 5 files changed, 76 insertions(+), 25 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8a9c155512..7c8b3b4e60 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -122,27 +122,5 @@ jobs: cd build make update-stage0 && make -j4 if: matrix.name == 'Linux' - - name: Install cargo - uses: actions-rs/toolchain@v1 - with: - toolchain: stable - profile: minimal - if: matrix.name == 'Linux release' - - name: Build manual - run: | - cargo install --git https://github.com/leanprover/mdBook mdbook - export PATH=~/.cargo/bin:$PWD/build/stage1/bin:$PATH - cd doc - git clean -fx . # clean up test artifacts in doc/example - mdbook build - mdbook test - if: matrix.name == 'Linux release' - - name: Publish manual - uses: peaceiris/actions-gh-pages@v3 - with: - github_token: ${{ secrets.GITHUB_TOKEN }} - publish_dir: ./doc/out - destination_dir: ./doc - if: matrix.name == 'Linux release' && github.ref == 'refs/heads/master' && github.event_name == 'push' - name: CCache stats run: ccache -s diff --git a/.github/workflows/nix-ci.yml b/.github/workflows/nix-ci.yml index 4d48ca2898..73f0f37a9e 100644 --- a/.github/workflows/nix-ci.yml +++ b/.github/workflows/nix-ci.yml @@ -81,5 +81,18 @@ jobs: run: | nix build -v --print-build-logs .#test cachix push -j4 lean4 ./result + - name: Build manual + run: | + nix build .#mdbook .#doc-test + cachix push -j4 lean4 ./result* + nix build .#doc + if: matrix.name == 'Linux' + - name: Publish manual + uses: peaceiris/actions-gh-pages@v3 + with: + github_token: ${{ secrets.GITHUB_TOKEN }} + publish_dir: ./result + destination_dir: ./doc + if: matrix.name == 'Linux' && github.ref == 'refs/heads/master' && github.event_name == 'push' - name: CCache stats run: CCACHE_DIR=/nix/var/cache/ccache nix run .#nixpkgs.ccache -- -s diff --git a/doc/mdbook.md b/doc/mdbook.md index 5334a53142..a80975cca6 100644 --- a/doc/mdbook.md +++ b/doc/mdbook.md @@ -5,13 +5,18 @@ This manual is generated by [mdBook](https://github.com/rust-lang/mdBook). We ar * Replace calling `rustdoc --test` from `mdbook test` with `./test` To build this manual, first install the fork via -``` +```bash cargo install --git https://github.com/leanprover/mdBook mdbook ``` Then use e.g. [`mdbook watch`](https://rust-lang.github.io/mdBook/cli/watch.html) in the `doc/` folder: -``` +```bash cd doc mdbook watch --open # opens the output in `out/` in your default browser ``` Run `mdbook test` to test all `lean` code blocks. + +Using the [Nix setup](make/nix.md), you can instead open a shell with the mdBook fork downloaded from our binary cache: +```bash +nix develop .#doc +``` diff --git a/flake.lock b/flake.lock index a38dfabf8f..f844c63ad1 100644 --- a/flake.lock +++ b/flake.lock @@ -31,6 +31,22 @@ "type": "github" } }, + "mdBook": { + "flake": false, + "locked": { + "lastModified": 1604075551, + "narHash": "sha256-+8jZBoGd8Rts0U1gNgN2tngRbf+amgLyJG5pSniGpZk=", + "owner": "leanprover", + "repo": "mdBook", + "rev": "2320d15253555b971166c500d6414bb2e5fed072", + "type": "github" + }, + "original": { + "owner": "leanprover", + "repo": "mdBook", + "type": "github" + } + }, "nix": { "inputs": { "lowdown-src": "lowdown-src", @@ -84,6 +100,7 @@ "root": { "inputs": { "flake-utils": "flake-utils", + "mdBook": "mdBook", "nix": "nix", "nixpkgs": "nixpkgs_2", "temci": "temci" diff --git a/flake.nix b/flake.nix index 43d80d79c8..1f384665e2 100644 --- a/flake.nix +++ b/flake.nix @@ -8,8 +8,12 @@ flake = false; }; inputs.nix.url = github:NixOS/nix; + inputs.mdBook = { + url = github:leanprover/mdBook; + flake = false; + }; - outputs = { self, nixpkgs, flake-utils, temci, nix }: flake-utils.lib.eachDefaultSystem (system: + outputs = { self, nixpkgs, flake-utils, temci, nix, mdBook }: flake-utils.lib.eachDefaultSystem (system: with nixpkgs.legacyPackages.${system}; let nix-pinned = writeShellScriptBin "nix" '' @@ -49,6 +53,38 @@ }; lean-emacs = emacsWithPackages (epkgs: with epkgs; [ dash dash-functional f flycheck s ] ++ [ lean4-mode ]); + lean-mdbook = mdbook.overrideAttrs (drv: rec { + name = "lean-${mdbook.name}"; + src = mdBook; + cargoDeps = drv.cargoDeps.overrideAttrs (_: { + inherit src; + outputHash = "sha256-BTm76YxY/tI4Pg53UbR+7KiQydb9L0FGYNZ0UKGyacw="; + }); + doCheck = false; + }); + doc = stdenv.mkDerivation { + name ="lean-doc"; + src = ./doc; + buildInputs = [ lean-mdbook ]; + buildCommand = '' + mdbook build -d $out $src + ''; + }; + # We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache + doc-test = stdenv.mkDerivation { + name ="lean-doc-test"; + src = ./doc; + buildInputs = [ lean-mdbook lean.stage1 strace ]; + patchPhase = '' + patchShebangs test + ''; + buildPhase = '' + ./test + mdbook test + touch $out + ''; + dontInstall = true; + }; in rec { packages = { inherit cc lean4-mode buildLeanPackage; @@ -63,6 +99,8 @@ # prefix lines with cumulative and individual execution time "$@" |& ts -i "(%.S)]" | ts -s "[%M:%S" ''; + mdbook = lean-mdbook; + inherit doc doc-test; }; defaultPackage = packages.lean;