diff mbox series

[bug#46124] Idris 2

Message ID 20210426172240.683c4c2b@riseup.net
State New
Headers show
Series [bug#46124] Idris 2 | expand

Checks

Context Check Description
cbaines/submitting builds success
cbaines/comparison success View comparision
cbaines/git branch success View Git branch
cbaines/applying patch fail View Laminar job
cbaines/issue success View issue

Commit Message

raingloom April 26, 2021, 3:22 p.m. UTC
On Thu, 22 Apr 2021 10:39:53 +0200
Xinglu Chen <public@yoctocell.xyz> wrote:

> I think you forgot the attach the patch. ;)
> 

Ah heck. That might have been the case.
Here it is.

There hasn't been a tagged release since then, so I'm sending my
original patch, but I should note that in my channel I've been tracking
the latest commit, which does seem to work, although it's been a while
since I used Idris for anything complicated.

Comments

Maxime Devos April 26, 2021, 9:27 p.m. UTC | #1
raingloom schreef op ma 26-04-2021 om 17:22 [+0200]:
> There hasn't been a tagged release since then, so I'm sending my
> original patch, but I should note that in my channel I've been tracking
> the latest commit, which does seem to work, although it's been a while
> since I used Idris for anything complicated.
> 
> +                     ;; TODO detect toolchain
> +                     "CC=gcc")))

Unless idris has a compiler built in that uses gcc for compiling
idris to machine code, this should likely be
,(string-append "CC=" (cc-for-target)) instead, such that the
cross-compiler is used when cross-compiling.

Teaching (cc-for-target) to detect which toolchain should be used
is a separate matter.  Maybe it could be a macro that looks at
(package-native-inputs this-package) or something.

Greetings,
Maxime.
diff mbox series

Patch

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