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(-)

diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index ca2772b904..14de2762a1 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -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