Build system gardening 🪴

.github/workflows/build.yml

@@ -53,7 +53,7 @@ jobs:
 
       - name: Typecheck 👩‍🏫
         run: |
-          nix-shell --arg interactive false --run "$build_command"
+          nix-shell --run "$build_command"
         # Run Agda as a separate stage so it doesn't have to be subject to
         # the absolutely spartan GC tuning parameters we run the build in
         # CI with
@@ -67,7 +67,7 @@ jobs:
       - name: Build 🛠️
         run: |
           echo "$mailmap" > .mailmap
-          nix-shell --arg interactive false --run "$build_command"
+          nix-shell --run "$build_command"
 
         # Shake is a bit of a pig, what with our abuses of caches, and
         # the default 2× heap overhead GHC uses means that a clean build

.gitignore

@@ -14,13 +14,14 @@ wip/
 .ghci
 hie.yaml
 /*.sh
+cabal.project.*
 
 # Build output
 /html
-/_build
+/_build*
 /result*
 /node_modules
-/dist-newstyle
+/dist-*
 /stack.yaml.lock
 /.stack-work
 .shake
@@ -30,6 +31,7 @@ hie.yaml
 *.hi-boot
 *.o-boot
 /rubtmp*
+.sass-cache
 
 ## Build system performance stuff
 *.eventlog*

README.md

@@ -18,9 +18,9 @@ external dependencies (e.g. pdftocairo, katex). The recommended way of
 building the 1Lab is using Nix.
 
 As a quick point of reference, `nix-build` will type-check and compile
-the entire thing, and copy the necessary assets (TeX Gyre Pagella and
-KaTeX's CSS and fonts) to the right locations. The result will be linked
-as `./result`, which can then be used to serve a website:
+the entire thing, and copy the necessary assets to the right locations.
+The result will be linked as `./result`, which can then be used to serve
+a website:
 
 ```bash
 $ nix-build
@@ -42,7 +42,7 @@ variables, you can use something like this to copy the static assets
 into place:
 
 ```bash
-$ eval "${installPhase}"
+$ eval "$installPhase"
 $ python -m http.server --directory _build/site
 ```
 
@@ -68,6 +68,11 @@ substituters = https://1lab.cachix.org
 trusted-public-keys = 1lab.cachix.org-1:eYjd9F9RfibulS4OSFBYeaTMxWojPYLyMqgJHDvG1fs=
 ```
 
+If you ever need to work on the Shakefile itself, `nix-shell -A shakefile`
+will give you a shell with all the required Haskell dependencies and a
+working Haskell Language Server installation. You can then use
+`cabal run 1lab-shake -- all -j` to build the Shakefile and the 1Lab.
+
 ## Directly
 
 If you're feeling brave, you can try to replicate one of the build
@@ -76,25 +81,24 @@ environments above. You will need:
 - The `cabal-install` package manager. Using `stack` is no longer supported.
 
 - A working LaTeX installation (TeXLive, etc) with the packages
-`tikz-cd` (depends on `pgf`), `mathpazo`, `xcolor`, `preview`, and
-`standalone` (depends on `varwidth` and `xkeyval`);
-
-- [Poppler] (for `pdftocairo`);
-- [`libsass`] (for `sassc`);
-- [Node] + required Node modules. Run `npm ci` to install those.
+  listed in `default.nix` (see `our-texlive`).
 
-[Poppler]: https://poppler.freedesktop.org/
-[Node]: https://nodejs.org/en/
-[`libsass`]: https://github.com/sass/sassc
+- [Poppler](https://poppler.freedesktop.org/) (for `pdftocairo`);
+- [Dart Sass](https://github.com/sass/dart-sass) (for `sass`);
+- [Node](https://nodejs.org/en/) + required Node modules. Run `npm ci` to install those.
 
 You can then use cabal-install to build and run our specific version of
-Agda and our Shakefile:
+Agda and our Shakefile. Follow the instructions in `cabal.project` to
+pin Agda to the appropriate version, then run:
 
 ```bash
 $ cabal install Agda -foptimise-heavily
 # This will take quite a while!
 
-$ cabal v2-run shake -- -j --skip-agda
+$ cabal run 1lab-shake -- -j --skip-agda all
 # the double dash separates cabal-install's arguments from our
 # shakefile's.
 ```
+
+To finish building the website, you will also need to manually install
+the required assets: see the `installPhase` in `default.nix`.

cabal.project

@@ -1,6 +1,12 @@
 packages: support/shake/1lab-shake.cabal
 
-source-repository-package
-  type: git
-  location: https://github.com/agda/agda.git
-  tag: 632954bf442192276ca9c84ca95991d1ffc7a410
+-- To build outside of the Nix shell, uncomment the following stanza
+-- and replace `master` with the `rev` field from `support/nix/dep/Agda/github.json`.
+--
+-- If you want to avoid polluting your Git tree, you can move this to
+-- `cabal.project.local`, which is ignored by Git.
+
+-- source-repository-package
+--   type: git
+--   location: https://github.com/agda/agda.git
+--   tag: master

default.nix

@@ -1,19 +1,10 @@
-{ # Is this a nix-shell invocation?
-  inNixShell ? false
-  # Do we want the full Agda package for interactive use? Set to false in CI
-, interactive ? true
-, system ? builtins.currentSystem
+{ system ? builtins.currentSystem
 }:
 let
   pkgs = import ./support/nix/nixpkgs.nix { inherit system; };
   inherit (pkgs) lib;
 
-  our-ghc = pkgs.labHaskellPackages.ghcWithPackages (ps: with ps; ([
-    shake directory tagsoup
-    text containers uri-encode
-    process aeson Agda pandoc SHA
-    fsnotify
-  ] ++ (if interactive then [ haskell-language-server ] else [])));
+  shakefile = pkgs.callPackage ./support/nix/build-shake.nix { };
 
   our-texlive = pkgs.texlive.combine {
     inherit (pkgs.texlive)
@@ -26,12 +17,6 @@ let
       varwidth xkeyval standalone;
   };
 
-  shakefile = pkgs.callPackage ./support/nix/build-shake.nix {
-    inherit our-ghc;
-    name = "1lab-shake";
-    main = "Main.hs";
-  };
-
   sort-imports = let
     script = builtins.readFile support/sort-imports.hs;
     # Extract the list of dependencies from the stack shebang comment.
@@ -43,32 +28,52 @@ let
     libraries = lib.attrVals deps pkgs.labHaskellPackages;
   } script;
 
-  deps = with pkgs; [
-    # For driving the compilation:
-    shakefile our-ghc
+  nodeModules = pkgs.importNpmLock.buildNodeModules {
+    npmRoot = ./.;
+    inherit (pkgs) nodejs;
+
+    derivationArgs = let
+      forbiddenRefs = [
+        pkgs.python3
+      ];
+    in {
+      nativeBuildInputs = [ pkgs.removeReferencesTo ];
+      postInstall = ''
+        find "$out" -exec remove-references-to ${lib.concatMapStringsSep " " (x: "-t ${lib.escapeShellArg x}") forbiddenRefs} '{}' +
+      '';
+      disallowedRequisites = forbiddenRefs;
+    };
+  };
 
+  setupNodePath = pkgs.makeSetupHook {
+    name = "setup-node-path";
+  } (pkgs.writeScript "setup-node-path.sh" ''
+    addToSearchPath NODE_PATH ${nodeModules}/node_modules
+  '');
+
+  # Dependencies for building the 1Lab itself, excluding the shakefile.
+  # These are also included in the shell for the shakefile itself so
+  # that `cabal run 1lab-shake` works as expected.
+  deps = with pkgs; [
     # For building the text and maths:
-    gitMinimal nodePackages.sass nodejs
+    gitMinimal dart-sass nodejs setupNodePath
 
     # For building diagrams:
     poppler-utils our-texlive
-  ] ++ (if interactive then [
-    sort-imports
-  ] else [
-    labHaskellPackages.pandoc.data
-  ]);
+  ];
 in
   pkgs.stdenv.mkDerivation rec {
     name = "1lab";
 
-    src = if inNixShell then null else
-      with pkgs.nix-gitignore; gitignoreFilterSourcePure (_: _: true) [
-        # Keep .git around for extracting page authors
-        (compileRecursiveGitignore ./.)
-        ".github"
-      ] ./.;
+    src = with pkgs.nix-gitignore; gitignoreFilterSourcePure (_: _: true) [
+      # Keep .git around for extracting page authors
+      (compileRecursiveGitignore ./.)
+      ".github"
+    ] ./.;
 
-    nativeBuildInputs = deps;
+    nativeBuildInputs = deps ++ [
+      shakefile
+    ];
 
     shellHook = ''
       export out=_build/site
@@ -92,8 +97,7 @@ in
     '';
 
     passthru = {
-      inherit deps shakefile sort-imports;
+      inherit pkgs shakefile deps sort-imports nodeModules;
       texlive = our-texlive;
-      ghc = our-ghc;
     };
   }

shell.nix

@@ -0,0 +1,27 @@
+{ system ? builtins.currentSystem
+}:
+let
+  the1lab = import ./. { inherit system; };
+  inherit (the1lab) pkgs shakefile deps sort-imports;
+  inherit (pkgs) lib;
+in
+# Note that mkShell destroys the installPhase.
+the1lab.overrideAttrs (old: {
+  src = null; # Don't copy anything to the store.
+
+  nativeBuildInputs = old.nativeBuildInputs or [] ++ [
+    (lib.getBin pkgs.labHaskellPackages.Agda)
+    sort-imports
+  ];
+
+  passthru = old.passthru // {
+    shakefile =
+      (shakefile.envFunc { withHoogle = false; }).overrideAttrs (old: {
+        nativeBuildInputs = old.nativeBuildInputs ++ deps ++ [
+          pkgs.cabal-install
+          pkgs.labHaskellPackages.haskell-language-server
+          sort-imports
+        ];
+      });
+  };
+})