feat: Nix: mdbook

.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

.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

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
+```

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"

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;