aboutsummaryrefslogtreecommitdiff
path: root/gnu/packages/agda.scm
diff options
context:
space:
mode:
Diffstat (limited to 'gnu/packages/agda.scm')
-rw-r--r--gnu/packages/agda.scm29
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))))
generated by cgit
s98pgrqsj77k91")))) (build-system gnu-build-system) (inputs `(("gettext" ,gettext-minimal) ("perl" ,perl) ("python" ,python-wrapper))) (home-page "https://salsa.debian.org/iso-codes-team/iso-codes") (synopsis "Various ISO standards") (description "This package provides lists of various ISO standards (e.g. country, language, language scripts, and currency names) in one place, rather than repeated in many programs throughout the system. Currently there are lists of languages and countries embedded in several different programs, which leads to dozens of lists of 200 languages, translated into more than 30 languages... not very efficient. With this package, we create a single \"gettext domain\" for every supported ISO standard which contains the translations of that domain. It is easy for a programmer to re-use those translations instead of maintaining their own translation infrastructure. Moreover, the programmer does not need to follow changes in the ISO standard and will not work with outdated information.") (license license:gpl2+))) ; some bits use the lgpl2 (define-public python-iso639 (package (name "python-iso639") (version "0.4.5") (source (origin (method url-fetch) (uri (pypi-uri "iso-639" version)) (sha256 (base32 "0jffmh4m20q8j27xb2fqbnlghjj0cx8pgsbzqisdg65qh2wd976w")))) (build-system python-build-system) (home-page "https://github.com/noumar/iso639") (synopsis "Python library for ISO 639 standard") (description "This package provides a Python library for ISO 639 standard that is concerned with representation of names for languages and language groups.") (license license:agpl3+))) (define-public python2-iso639 (package-with-python2 python-iso639)) (define-public python-iso3166 (package (name "python-iso3166") (version "0.9") (source (origin (method url-fetch) (uri (pypi-uri "iso3166" version)) (sha256 (base32 "0hm0xm30sprk1jssmn4cqks0x3nx5fp8r5ypvahcysmmayzrsnjl")))) (build-system python-build-system) (home-page "https://github.com/deactivated/python-iso3166") (synopsis "Self-contained ISO 3166-1 country definitions") (description "This package provides the ISO 3166-1 country definitions.") (license license:expat))) (define-public python2-iso3166 (package-with-python2 python-iso3166))
generated by cgit