fix

leanprover · Aug 1, 2024 · ff1befa · ff1befa
1 parent b4f0e27
commit ff1befa
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 16 deletions.
diff --git a/.github/workflows/nix-ci.yml b/.github/workflows/nix-ci.yml
@@ -103,7 +103,7 @@ jobs:
         continue-on-error: true
       - name: Build manual
         run: |
-          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc
+          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,inked} -o push-doc
           nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc
           # https://github.com/netlify/cli/issues/1809
           cp -r --dereference ./result ./dist

diff --git a/doc/flake.nix b/doc/flake.nix
@@ -44,21 +44,6 @@
           mdbook build -d $out
         '';
       };
-      # We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache
-      test = stdenv.mkDerivation {
-        name ="lean-doc-test";
-        src = doc-src;
-        buildInputs = [ lean-mdbook stage1.Lean.lean-package strace ];
-        patchPhase = ''
-          cd doc
-          patchShebangs test
-        '';
-        buildPhase = ''
-          mdbook test
-          touch $out
-        '';
-        dontInstall = true;
-      };
       leanInk = (buildLeanPackage {
         name = "Main";
         src = inputs.leanInk;