diff options
| author | Josselin Poiret <dev@jpoiret.xyz> | 2023-04-30 12:12:33 +0200 |
|---|---|---|
| committer | Josselin Poiret <dev@jpoiret.xyz> | 2023-06-04 10:59:36 +0200 |
| commit | 067e75e17a7f2c278eb6273824e33454d8e00566 (patch) | |
| tree | d6be56456862b1f0834b5a5e7d6e686be8deb56f /gnu/packages | |
| parent | cf2c3f797003a67c9a8d3c1400a480c617f89eda (diff) | |
| download | guix-067e75e17a7f2c278eb6273824e33454d8e00566.tar.gz guix-067e75e17a7f2c278eb6273824e33454d8e00566.zip | |
gnu: Add agda-1lab.
* gnu/packages/agda.scm: New variable agda-1lab.
Diffstat (limited to 'gnu/packages')
| -rw-r--r-- | gnu/packages/agda.scm | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 240a51de1a..bd7fe29f1e 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -295,3 +295,32 @@ try agda-prelude instead.") agda-stdlib but using cubical methods.") (home-page "https://github.com/agda/cubical") (license license:expat)))) + +(define-public agda-1lab + ;; Upstream doesn't do releases (yet). Use a commit that builds with 2.6.3, + ;; since they use Agda HEAD. + (let* ((revision "1") + (commit "47ca1d23640a6f49a3abe3c2fe27738bcc10c9c6")) + (package + (name "agda-1lab") + (version (git-version "0.0" revision commit)) + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/plt-amy/1lab.git") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "0j7mp6c0xd0849skdxzncklkxynxnyfrbpcjv4qp5p1xfn0dnfqx")))) + (build-system agda-build-system) + (arguments + (list #:plan '(("src/index\\.lagda\\.md$")))) + (synopsis "Reference resource for mathematics done in Homotopy Type Theory") + (description "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.") + (home-page "https://1lab.dev") + (license license:agpl3)))) |