pkgs/development/libraries/agda/1lab/default.nix

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