Repository files navigation

A formalised, cross-linked reference resource for mathematics done inHomotopy Type Theory. Unlike the HoTT book, the 1lab is not a “linear”resource: Concepts are presented as a directed graph, with linksindicating dependencies.

Building the 1Lab is a rather complicated task, which has led to a lotof homebrew infrastructure being developed for it. We build against aspecific build of Agda (see therev field insupport/nix/dep/Agda/github.json), and there are also quite a fewexternal dependencies (e.g. pdftocairo, katex). The recommended way ofbuilding the 1Lab is using Nix.

As a quick point of reference,nix-build will type-check and compilethe entire thing, and copy the necessary assets (TeX Gyre Pagella andKaTeX's CSS and fonts) to the right locations. The result will be linkedas./result, which can then be used to serve a website:

$ nix-build$ python -m http.server --directory result

Note that using Nix to build the website takes around ~20-30 minutes,since it will type-check the entire codebase from scratch every time.For interactive development,nix-shell will give you a shell witheverything you need to hack on the 1Lab, including Agda and thepre-built Shakefile as1lab-shake:

$ 1lab-shake all -j

Sincenix-shell will load the derivation steps as environmentvariables, you can use something like this to copy the static assetsinto place:

$eval"${installPhase}"$ python -m http.server --directory _build/site

To hack on a file continuously, you can use "watch mode", which willattempt to only check and build the changed file.

$ 1lab-shake all -w

Additionally, since the validity of the Agda code is generally upheld byagda-mode, you can use--skip-agda to only build the prose. Notethat this will disable checking the integrity of link targets, thetranslation of`ref`{.Agda} spans, and the code blocks will beright ugly.

Our build tools are routinely built for x86_64-linux and uploaded toCachix. If you have the Cachix CLI installed, simply runcachix use 1lab. Otherwise, add the following to your Nix configuration:

substituters = https://1lab.cachix.orgtrusted-public-keys = 1lab.cachix.org-1:eYjd9F9RfibulS4OSFBYeaTMxWojPYLyMqgJHDvG1fs=

If you're feeling brave, you can try to replicate one of the buildenvironments above. You will need:

• Thecabal-install package manager. Usingstack is no longer supported.

• A working LaTeX installation (TeXLive, etc) with the packagestikz-cd (depends onpgf),mathpazo,xcolor,preview, andstandalone (depends onvarwidth andxkeyval);

• Poppler (forpdftocairo);

• libsass (forsassc);

• Node + required Node modules. Runnpm ci to install those.

You can then use cabal-install to build and run our specific version ofAgda and our Shakefile:

$ cabal install Agda# This will take quite a while!$ cabal v2-run shake -- -j --skip-agda# the double dash separates cabal-install's arguments from our# shakefile's.