tjh.dev
1{
2 lib,
3 mkDerivation,
4 fetchFromGitHub,
5}:
6
7mkDerivation rec {
8 pname = "1lab";
9 version = "unstable-2024-08-05";
10
11 src = fetchFromGitHub {
12 owner = "the1lab";
13 repo = pname;
14 rev = "7cc9bf7bbe90be5491e0d64da90a36afa29a540b";
15 hash = "sha256-hOyf6ZzejDAFDRj6liFZsBc9bKdxV5bzTPP4kGXIhW0=";
16 };
17
18 postPatch = ''
19 # We don't need anything in support; avoid installing LICENSE.agda
20 rm -rf support
21
22 # Remove verbosity options as they make Agda take longer and use more memory.
23 shopt -s globstar extglob
24 files=(src/**/*.@(agda|lagda.md))
25 sed -Ei '/OPTIONS/s/ -v ?[^ #]+//g' "''${files[@]}"
26
27 # Generate all-pages manually instead of building the build script.
28 mkdir -p _build
29 for f in "''${files[@]}"; do
30 f=''${f#src/} f=''${f%%.*} f=''${f//\//.}
31 echo "open import $f"
32 done > _build/all-pages.agda
33 '';
34
35 libraryName = "1lab";
36 libraryFile = "1lab.agda-lib";
37 everythingFile = "_build/all-pages.agda";
38
39 meta = with lib; {
40 description = "Formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory ";
41 homepage = src.meta.homepage;
42 license = licenses.agpl3Only;
43 platforms = platforms.unix;
44 maintainers = with maintainers; [ ncfavier ];
45 };
46}