blob: 5282de13e398f4c347259b7f37db136b2e8f1c7d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
{
lib,
mkDerivation,
fetchFromGitHub,
unstableGitUpdater,
}:
mkDerivation {
pname = "1lab";
version = "0-unstable-2025-07-01";
src = fetchFromGitHub {
owner = "the1lab";
repo = "1lab";
rev = "e9c2ad2b3ba9cefad36e72cb9d732117c68ac862";
hash = "sha256-wKh77+xCdfMtnq9jMlpdnEptGO+/WVNlQFa1TDbdUGs=";
};
postPatch = ''
# We don't need anything in support; avoid installing LICENSE.agda
rm -rf support
# Remove verbosity options as they make Agda take longer and use more memory.
shopt -s globstar extglob
files=(src/**/*.@(agda|lagda.md))
sed -Ei '/OPTIONS/s/ -v ?[^ #]+//g' "''${files[@]}"
'';
passthru.updateScript = unstableGitUpdater { };
meta = {
description = "Formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory ";
homepage = "https://github.com/the1lab/1lab";
license = lib.licenses.agpl3Only;
platforms = lib.platforms.unix;
maintainers = with lib.maintainers; [ ncfavier ];
};
}
|
