A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory. Unlike the HoTT book, the 1lab is not a “linear” resource: Concepts are presented as a directed graph, with links indicating dependencies.
Here's how you can build --- and work on --- the web parts of the 1lab.
An Arch Linux-based Docker container is provided which contains all the dependencies necessary for building the 1lab, including the font files required for a complete deployment. Since this container is on the registry, we can do a one-line build of the 1Lab as follows:
% docker run -it -v $PWD:/workspace docker.io/pltamy/1lab:latest /bin/sh -i
$ 1lab-shake all -j # build everything
$ sh support/make-site.sh # copy everything into place
After this, the directory _build/site
will have everything in place
for use as the HTTP root of a static site to serve the 1Lab, for example
using the Python distribution that the container ships with:
$ python -m http.server --directory _build/site
If you run NixOS, or have the Nix package manager installed, you can use
the provided default.nix
file to build a complete, reproducible
deployment of the 1Lab. This has the benefit of also providing
nix-shell
support for immediately setting up an environment for
development which supports compilation of the HTML and SVG files, in
addition to the Agda.
You can then use Nix to compile the project as usual. 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 css/fonts) to
the right locations. The result will be linked as ./result
, which can
then be used to serve a website:
$ nix build
$ python -m http.server --directory result
For interactive development, keep in mind that the buildInputs
to
default.nix
don't include Stack or ghc
. However, just like the
Docker container, a pre-built version of the Shakefile is included as
1lab-shake
:
$ 1lab-shake all -j
Since nix-shell
will load the derivation steps as environment
variables, you can use something like this to copy the static assets
into place:
$ export out=_build/site
$ echo "${installPhase}" | bash
If you're feeling brave, you can try to replicate one of the build environments above. You will need:
-
A Haskell package manager (either cabal or stack);
-
A working LaTeX installation (TeXLive, etc) with the packages
tikz-cd
(depends onpgf
),mathpazo
,xcolor
,preview
, andstandalone
(depends onvarwidth
andxkeyval
); -
Rubber (for
rubber
); -
Poppler (for
pdftocairo
); -
libsass
(forsassc
); -
The KaTeX executable
katex
in your$PATH
; -
The tools agda-fold-equations and agda-reference-filter, which are Cabal packages and can be installed however you prefer
-
If you're using Stack, that's all. If using cabal-install, you're going to need the following Haskell packages:
- Agda
- pandoc
- shake
- tagsoup
- uri-encode
If everything is set up properly, the following command should work to
produce the compiled HTML, SVG and CSS files in _build/html
. You can
then follow either the support/make-site.sh
script or the
installPhase
in default.nix
to work out how to acquire & set up the
rest of the static assets.
$ ./Shakefile.hs all -j # (using stack)
$ runghc ./Shakefile.hs all -j # (using cabal-install)