From 7554e53ad682e5baa40fee0776ab88cffc1a7772 Mon Sep 17 00:00:00 2001
From: raingloom <raingloom@riseup.net>
Date: Wed, 27 Jan 2021 06:21:01 +0100
Subject: [PATCH] gnu: Added Idris 2.
* gnu/packages/idris.scm (idris2): New variable.
---
gnu/packages/idris.scm | 80 +++++++++++++++++++++++++++++++++++++++++-
1 file changed, 79 insertions(+), 1 deletion(-)
@@ -21,6 +21,8 @@
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages bash)
+ #:use-module (gnu packages chez)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
@@ -28,12 +30,15 @@
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ncurses)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages python)
+ #:use-module (gnu packages sphinx)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
#:use-module (guix download)
#:use-module (guix git-download)
#:use-module ((guix licenses) #:prefix license:)
- #:use-module (guix packages))
+ #:use-module (guix packages)
+ #:use-module (ice-9 regex))
(define-public idris
(package
@@ -150,6 +155,79 @@ can be specified precisely in the type. The language is closely related to
Epigram and Agda.")
(license license:bsd-3)))
+(define-public idris2
+ (package
+ (name "idris2")
+ (version "0.3.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/idris-lang/Idris2")
+ (commit (string-append "v" version))))
+ (sha256
+ (base32
+ "0sa2lpb7n6xqfknwld9rzm4bnb6qcd0ja1n63cnc5v8wdzr8q7kh"))))
+ (build-system gnu-build-system)
+ (arguments
+ `(#:tests? #f ;; they are run as part of other targets
+ #:phases
+ (modify-phases
+ %standard-phases
+ (add-after 'unpack 'patch-paths
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (substitute* "config.mk"
+ ((,(regexp-quote "PREFIX ?= $(HOME)/.idris2"))
+ (string-append "PREFIX = "
+ (assoc-ref outputs "out"))))
+ (for-each
+ (lambda (f)
+ (substitute* f
+ ((,(regexp-quote "#!/bin/sh"))
+ (string-append "#!" (assoc-ref inputs "sh")
+ "/bin/sh"))))
+ (list "src/Compiler/Scheme/Chez.idr"
+ "src/Compiler/Scheme/Racket.idr"
+ "bootstrap/idris2_app/idris2.rkt"
+ "bootstrap/idris2_app/idris2.ss"))))
+ ;; this is not the kind of bootstrap we want to run
+ (delete 'bootstrap)
+ (delete 'configure)
+ (replace 'build
+ (lambda _
+ (invoke "make" "bootstrap"
+ "SCHEME=scheme"
+ ;; TODO detect toolchain
+ "CC=gcc")))
+ (add-after 'build 'build-doc
+ (lambda _
+ (with-directory-excursion
+ "docs"
+ (invoke "make" "html"))))
+ (add-after 'install 'install-doc
+ (lambda* (#:key outputs #:allow-other-keys)
+ (copy-recursively
+ "docs/build/html"
+ (string-append
+ (assoc-ref outputs "out")
+ "/share/doc/"
+ ,name "-" ,version)))))))
+ (inputs
+ `(("sh" ,bash-minimal)
+ ("chez-scheme" ,chez-scheme)))
+ (native-inputs
+ `(("python-sphinx" ,python-sphinx)
+ ("python-sphinx-rtd-theme" ,python-sphinx-rtd-theme)
+ ("python" ,python)))
+ (home-page "https://idris-lang.org/")
+ (synopsis "A dependently typed programming language, a successor to Idris")
+ (description
+ "Idris 2 is a general purpose language with dependent linear types.
+It is compiled, with eager evaluation. Dependent types allow types to
+be predicated on values, meaning that some aspects of a program's behaviour
+can be specified precisely in the type. It can use multiple languages as code
+generation backends.")
+ (license license:bsd-3)))
+
;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set.
(define (idris-default-arguments name)
`(#:modules ((guix build gnu-build-system)
--
2.31.1