* [bug#49607] [PATCH] gnu: Add Idris 2.
@ 2021-07-17 15:42 Xinglu Chen
2021-10-05 16:37 ` [bug#49607] [PATCH 1/3] gnu: ghc-cheapskate: Update to 0.1.1.2 Attila Lendvai
` (6 more replies)
0 siblings, 7 replies; 17+ messages in thread
From: Xinglu Chen @ 2021-07-17 15:42 UTC (permalink / raw)
To: 49607; +Cc: raingloom
From: raingloom <raingloom@riseup.net>
* gnu/packages/idris.scm (idris2): New variable.
Co-authored-by: Xinglu Chen <public@yoctocell.xyz>
---
Based a previous patch by raingloom[1].
Some changes I made:
* Tests are enabled, but only the Chez backend is enabled since that’s
the only backend we have for now.
* Some environment have been set, which should make it possible to
import third-party packages.
* The bin/idris2_app directory has been removed, see the comment in the
code below.
* The executable is wrapped so some environment variables can be set.
* I also changed the synopsis to the one on their GitHub page, and added
a copyright line for raingloom.
[1]: https://issues.guix.gnu.org/46124#1
gnu/packages/idris.scm | 120 ++++++++++++++++++++++++++++++++++++++++-
1 file changed, 119 insertions(+), 1 deletion(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index ca2772b904..64cb4f37f5 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -3,6 +3,8 @@
;;; Copyright © 2016, 2017 David Craven <david@craven.ch>
;;; Copyright © 2018 Alex ter Weele <alex.ter.weele@gmail.com>
;;; Copyright © 2019, 2021 Eric Bavier <bavier@posteo.net>
+;;; Copyrignt © 2021 raingloom <raingloom@riseup.net>
+;;; Copyright © 2021 Xinglu Chen <public@yoctocell.xyz>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -21,6 +23,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 +32,16 @@
#: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 (guix utils)
+ #:use-module (ice-9 regex))
(define-public idris
(package
@@ -150,6 +158,116 @@ can be specified precisely in the type. The language is closely related to
Epigram and Agda.")
(license license:bsd-3)))
+;; TODO: Add other backends?
+(define-public idris2
+ (package
+ (name "idris2")
+ (version "0.4.0")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/idris-lang/Idris2")
+ (commit (string-append "v" version))))
+ (sha256
+ (base32
+ "105jybjf5s0k6003qzfxchzsfcpsxip180bh3mdmi74d464d0h8g"))))
+ (build-system gnu-build-system)
+ (arguments
+ `(#:test-target "bootstrap-test"
+ #: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"))))
+ (substitute* '("src/Compiler/Scheme/Chez.idr"
+ "src/Compiler/Scheme/Racket.idr"
+ "bootstrap/idris2_app/idris2.rkt"
+ "bootstrap/idris2_app/idris2.ss")
+ ((,(regexp-quote "#!/bin/sh"))
+ (string-append "#!" (assoc-ref inputs "bash")
+ "/bin/sh")))))
+ ;; This is not the kind of bootstrap we want to run
+ (delete 'bootstrap)
+ (delete 'configure) ; no configure script
+ (replace 'build
+ (lambda _
+ (invoke "make" "bootstrap"
+ "SCHEME=scheme"
+ ;; TODO: detect toolchain.
+ (string-append "CC=" ,(cc-for-target)))))
+ (add-after 'build 'build-doc
+ (lambda _
+ (with-directory-excursion
+ "docs"
+ (invoke "make" "html"))))
+ (add-before 'check 'set-cc
+ (lambda _
+ (setenv "CC" ,(cc-for-target))))
+ (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))))
+ (add-after 'install-doc 'fix-ld-library-path
+ (lambda* (#:key outputs #:allow-other-keys)
+ ;; The bin/idris2 calls bin/idris2_app/idris2.so which is
+ ;; the real executable, but it sets LD_LIBRARY_PATH
+ ;; incorrectly. Remove bin/idris2 and replace it with
+ ;; bin/idris2_app/idris2.so instead.
+ (let ((out (assoc-ref outputs "out")))
+ (delete-file (string-append out "/bin/idris2"))
+ (copy-file (string-append out "/bin/idris2_app/idris2.so")
+ (string-append out "/bin/idris2"))
+ (delete-file-recursively (string-append out "/bin/idris2_app")))))
+ (add-after 'fix-ld-library-path 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((chez (string-append (assoc-ref inputs "chez-scheme")
+ "/bin/scheme"))
+ (out (assoc-ref outputs "out"))
+ (idris2 (string-append out "/bin/idris2"))
+ (version ,version))
+ (wrap-program idris2
+ `("LD_LIBRARY_PATH" ":" prefix
+ (,(string-append out "/idris2-" version "/lib")))
+ `("CHEZ" ":" = (,chez)))))))))
+ (inputs
+ `(("bash" ,bash-minimal)
+ ("chez-scheme" ,chez-scheme)
+ ("gmp" ,gmp)))
+ (native-inputs
+ ;; For building docs.
+ `(("python-sphinx" ,python-sphinx)
+ ("python-sphinx-rtd-theme" ,python-sphinx-rtd-theme)
+ ("python" ,python) ))
+ (native-search-paths
+ (list (search-path-specification
+ (variable "IDRIS2_PACKAGE_PATH")
+ (files (list (string-append "idris2-" version))))
+ (search-path-specification
+ (variable "IDRIS2_LIBS")
+ (files (list (string-append "idris2-" version "/lib")))
+ (file-type 'directory))
+ (search-path-specification
+ (variable "IDRIS2_DATA")
+ (files (list (string-append "idris2-" version "/support")))
+ (file-type 'directory))))
+ (home-page "https://idris-lang.org/")
+ (synopsis "Purely functional programming language with first class types")
+ (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)
base-commit: 9cb35c02164d929fcb8929e7f454df215df8cf25
--
2.32.0
^ permalink raw reply related [flat|nested] 17+ messages in thread
* [bug#49607] [PATCH 1/3] gnu: ghc-cheapskate: Update to 0.1.1.2
2021-07-17 15:42 [bug#49607] [PATCH] gnu: Add Idris 2 Xinglu Chen
@ 2021-10-05 16:37 ` Attila Lendvai
2021-10-05 16:37 ` [bug#49607] [PATCH 2/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
2021-10-05 16:37 ` [bug#49607] [PATCH 3/3] gnu: idris: Add idris2 0.5.1, and 1.3.3-1.5545986 Attila Lendvai
2022-04-14 12:16 ` [bug#49607] [PATCH v2 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
` (5 subsequent siblings)
6 siblings, 2 replies; 17+ messages in thread
From: Attila Lendvai @ 2021-10-05 16:37 UTC (permalink / raw)
To: 49607; +Cc: Attila Lendvai
* gnu/packages/haskell-xyz.scm (ghc-cheapskate): Update to 0.1.1.2
* gnu/packages/idris.scm (idris-1.3.3): Delete now unnecessary substitute
---
i have many plans for further changes, but i thought i'll
send this meanwhile, so that everyone can have a fresh
idris on their guix.
this doesn't build/install the docs. may add it later.
gnu/packages/haskell-xyz.scm | 4 ++--
gnu/packages/idris.scm | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/gnu/packages/haskell-xyz.scm b/gnu/packages/haskell-xyz.scm
index f421458e15..87ebe4f3b6 100644
--- a/gnu/packages/haskell-xyz.scm
+++ b/gnu/packages/haskell-xyz.scm
@@ -1966,7 +1966,7 @@ Partial and Infinite Values\"}.")
(define-public ghc-cheapskate
(package
(name "ghc-cheapskate")
- (version "0.1.1.1")
+ (version "0.1.1.2")
(source
(origin
(method url-fetch)
@@ -1976,7 +1976,7 @@ Partial and Infinite Values\"}.")
".tar.gz"))
(sha256
(base32
- "0qnyd8bni2rby6b02ff4bvfdhm1hwc8vzpmnms84jgrlg1lly3fm"))))
+ "17n6laihqrjn62l8qw4565nf77zkvrl68bjmc3vzr4ckqfblhdzd"))))
(build-system haskell-build-system)
(inputs
`(("ghc-blaze-html" ,ghc-blaze-html)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index ca2772b904..058d679c1f 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -100,8 +100,8 @@
(add-after 'unpack 'update-constraints
(lambda _
(substitute* "idris.cabal"
- (("ansi-terminal < 0\\.9") "ansi-terminal < 0.10")
- (("cheapskate >= 0\\.1\\.1\\.2 && < 0\\.2") "cheapskate >= 0.1.1.1 && < 0.2"))
+ ;; This is only needed for v1.3.3, later it got relaxed upstream
+ (("ansi-terminal < 0\\.9") "ansi-terminal < 0.10"))
#t))
(add-before 'configure 'set-cc-command
(lambda _
--
2.33.0
^ permalink raw reply related [flat|nested] 17+ messages in thread
* [bug#49607] [PATCH 2/3] gnu: idris: Use wrap-program to define IDRIS_CC
2021-10-05 16:37 ` [bug#49607] [PATCH 1/3] gnu: ghc-cheapskate: Update to 0.1.1.2 Attila Lendvai
@ 2021-10-05 16:37 ` Attila Lendvai
2021-10-05 16:37 ` [bug#49607] [PATCH 3/3] gnu: idris: Add idris2 0.5.1, and 1.3.3-1.5545986 Attila Lendvai
1 sibling, 0 replies; 17+ messages in thread
From: Attila Lendvai @ 2021-10-05 16:37 UTC (permalink / raw)
To: 49607; +Cc: Attila Lendvai
Idris requires a C compiler at runtime to generate executables.
* gnu/packages/idris.scm (idris): Rename the scheme variable to idris-1.3.3 to
prepare for adding different versions later on.
[inputs]: Add Clang, and bash-minimal (for wrap-program).
[phases]: use (cc-for-target).
---
gnu/packages/idris.scm | 31 +++++++++++++++++++++++--------
1 file changed, 23 insertions(+), 8 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 058d679c1f..1f6e984a90 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -21,10 +21,12 @@
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages bash)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
#:use-module (gnu packages libffi)
+ #:use-module (gnu packages llvm)
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ncurses)
#:use-module (gnu packages perl)
@@ -33,9 +35,10 @@
#: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 (guix utils))
-(define-public idris
+(define-public idris-1.3.3
(package
(name "idris")
(version "1.3.3")
@@ -51,12 +54,15 @@
(build-system haskell-build-system)
(native-inputs ;For tests
`(("perl" ,perl)
+ ("clang" ,clang) ; the tests want to generate exeutables
("ghc-cheapskate" ,ghc-cheapskate)
("ghc-tasty" ,ghc-tasty)
("ghc-tasty-golden" ,ghc-tasty-golden)
("ghc-tasty-rerun" ,ghc-tasty-rerun)))
(inputs
- `(("gmp" ,gmp)
+ `(("bash" ,bash-minimal)
+ ("clang" ,clang) ; FIXME clang compiles faster than gcc, but (cc-for-target) ignores it
+ ("gmp" ,gmp)
("ncurses" ,ncurses)
("ghc-aeson" ,ghc-aeson)
("ghc-annotated-wl-pprint" ,ghc-annotated-wl-pprint)
@@ -105,7 +111,7 @@
#t))
(add-before 'configure 'set-cc-command
(lambda _
- (setenv "CC" "gcc")
+ (setenv "CC" ,(cc-for-target))
#t))
(add-after 'install 'fix-libs-install-location
(lambda* (#:key outputs #:allow-other-keys)
@@ -116,14 +122,14 @@
(lambda (module)
(symlink (string-append modules "/" module)
(string-append lib "/" module)))
- '("prelude" "base" "contrib" "effects" "pruviloj")))))
+ '("prelude" "base" "contrib" "effects" "pruviloj")))
+ #t))
(delete 'check) ;Run check later
(add-after 'install 'check
(lambda* (#:key outputs #:allow-other-keys #:rest args)
(let ((out (assoc-ref outputs "out")))
(chmod "test/scripts/timeout" #o755) ;must be executable
(setenv "TASTY_NUM_THREADS" (number->string (parallel-job-count)))
- (setenv "IDRIS_CC" "gcc") ;Needed for creating executables
(setenv "PATH" (string-append out "/bin:" (getenv "PATH")))
(apply (assoc-ref %standard-phases 'check) args))))
(add-before 'check 'restore-libidris_rts
@@ -135,8 +141,15 @@
(static (assoc-ref outputs "static"))
(filename "/lib/idris/rts/libidris_rts.a"))
(rename-file (string-append static filename)
- (string-append out filename))
- #t))))))
+ (string-append out filename)))
+ #t))
+ (add-before 'check 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (exe (string-append out "/bin/idris")))
+ (wrap-program exe
+ `("IDRIS_CC" = (,',(cc-for-target)))))
+ #true)))))
(native-search-paths
(list (search-path-specification
(variable "IDRIS_LIBRARY_PATH")
@@ -150,6 +163,8 @@ can be specified precisely in the type. The language is closely related to
Epigram and Agda.")
(license license:bsd-3)))
+(define-public idris idris-1.3.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.33.0
^ permalink raw reply related [flat|nested] 17+ messages in thread
* [bug#49607] [PATCH 3/3] gnu: idris: Add idris2 0.5.1, and 1.3.3-1.5545986.
2021-10-05 16:37 ` [bug#49607] [PATCH 1/3] gnu: ghc-cheapskate: Update to 0.1.1.2 Attila Lendvai
2021-10-05 16:37 ` [bug#49607] [PATCH 2/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
@ 2021-10-05 16:37 ` Attila Lendvai
1 sibling, 0 replies; 17+ messages in thread
From: Attila Lendvai @ 2021-10-05 16:37 UTC (permalink / raw)
To: 49607; +Cc: Attila Lendvai
This generality is there because with this it is possible to bootstrap Idris
HEAD all the way down from GHC. It requires patching past releases, which
requires importing them into separate git branches. This has not been merged
into upstream yet, therefore this commit only contains a single use of
MAKE-IDRIS-PACKAGE, but that will change in the future.
Add a symlink to a versioned binary; e.g. add a `bin/idris-1.3.3`.
* gnu/packages/idris.scm (idris-1.3.3-1): New variable, the latest git commit
from the v1.x line of Idris.
(make-idris-package): New function to instantiate a package of Idris2.
(idris2-0.5.1): New variable.
---
gnu/packages/idris.scm | 182 ++++++++++++++++++++++++++++++++++++++++-
1 file changed, 179 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 1f6e984a90..4ef18c6da4 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -19,9 +19,22 @@
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
+;;; TODO
+;;;
+;;; - Idris has multiple backends, but we only register Chez as an
+;;; input. Decide how to make backends optional, and/or which ones to package
+;;; by default.
+;;;
+;;; - Set RUNPATH instead of using LD_LIBRARY_PATH. See
+;;; http://blog.tremily.us/posts/rpath/ This needs patching Idris so that it
+;;; stops using a wrapper script and finds its libidris_support.so
+;;; e.g. relative to the executable.
+
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages base)
#: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)
@@ -29,14 +42,21 @@
#:use-module (gnu packages llvm)
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ncurses)
+ #:use-module (gnu packages node)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages racket)
+ #:use-module (gnu packages version-control)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
#:use-module (guix download)
+ #:use-module (guix git)
#:use-module (guix git-download)
#:use-module ((guix licenses) #:prefix license:)
#:use-module (guix packages)
- #:use-module (guix utils))
+ #:use-module (guix utils)
+ #:use-module (ice-9 match)
+ #:use-module (ice-9 regex)
+ #:export (make-idris-package))
(define-public idris-1.3.3
(package
@@ -148,8 +168,10 @@
(let* ((out (assoc-ref outputs "out"))
(exe (string-append out "/bin/idris")))
(wrap-program exe
- `("IDRIS_CC" = (,',(cc-for-target)))))
- #true)))))
+ `("IDRIS_CC" = (,',(cc-for-target))))
+ (with-directory-excursion (string-append out "/bin/")
+ (symlink ,name (string-append ,name "-" ,version))))
+ #t)))))
(native-search-paths
(list (search-path-specification
(variable "IDRIS_LIBRARY_PATH")
@@ -165,6 +187,160 @@ Epigram and Agda.")
(define-public idris idris-1.3.3)
+(define-public idris-1.3.3-1
+ ;; This is the current latest from the v1.x branch.
+ (let ((commit "55459867fc3f1ac34527a5dd998c37e72b15d488")
+ (revision "1"))
+ (package
+ (inherit idris-1.3.3)
+ (version (git-version "1.3.3" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/attila-lendvai/Idris2")
+ (commit commit)))
+ (sha256
+ (base32
+ "0qsn1953jy74pgppwkax8yrlswb3v46x541ahbl95rshf666nsj6"))
+ (file-name (git-file-name "idris" version))))
+ (inputs
+ (append (package-inputs idris-1.3.3)
+ `(("ghc-haskeline-0.8" ,ghc-haskeline-0.8)))))))
+
+(define* (make-idris-package source version
+ #:key bootstrap-idris
+ (ignore-test-failures? #false)
+ (unwrap? #true)
+ (tests? #true)
+ (files-to-patch-for-shell
+ '("src/Compiler/Scheme/Chez.idr"
+ "src/Compiler/Scheme/Racket.idr"
+ "src/Compiler/Scheme/Gambit.idr"
+ "src/Compiler/ES/Node.idr"
+ "bootstrap/idris2_app/idris2.rkt"
+ "bootstrap/idris2_app/idris2.ss"))
+ (with-bootstrap-shortcut? #true))
+ (package
+ (name "idris2")
+ (version version)
+ (source (match source
+ ((commit hash . url)
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url (if (null? url)
+ "https://github.com/idris-lang/Idris2.git"
+ (car url)))
+ (commit commit)))
+ (sha256 (base32 hash))
+ (file-name (git-file-name name version))))
+ ((? git-checkout?)
+ source)))
+ (build-system gnu-build-system)
+ (native-inputs
+ `(,@(if with-bootstrap-shortcut?
+ `(("chez-scheme" ,chez-scheme))
+ `(("bootstrap-idris" ,bootstrap-idris)))
+ ("cc" ,clang-toolchain-12) ; clang or older clang-toolchain's don't have a bin/cc
+ ("coreutils" ,coreutils)
+ ("git" ,git)
+ ("node" ,node) ; only for the tests
+ ("racket" ,racket) ; only for the tests
+ ("sed" ,sed)))
+ (inputs
+ `(("bash" ,bash-minimal)
+ ("chez-scheme" ,chez-scheme)
+ ("gmp" ,gmp)))
+ (arguments
+ `(#:tests? ,tests?
+ #:make-flags
+ (list (string-append "CC=" ,(cc-for-target))
+ ,@(if with-bootstrap-shortcut?
+ '((string-append "SCHEME="
+ (assoc-ref %build-inputs "chez-scheme")
+ "/bin/scheme"))
+ `((string-append "BOOTSTRAP_IDRIS="
+ (assoc-ref %build-inputs "bootstrap-idris")
+ "/bin/" ,(package-name bootstrap-idris))))
+ (string-append "PREFIX=" (assoc-ref %outputs "out"))
+ "-j1")
+ #:phases
+ (modify-phases %standard-phases
+ (delete 'bootstrap)
+ (delete 'configure)
+ (delete 'check) ; check must happen after install and wrap-program
+ (add-after 'unpack 'patch-paths
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* ',files-to-patch-for-shell
+ ((,(regexp-quote "#!/bin/sh"))
+ (string-append "#!" (assoc-ref inputs "bash") "/bin/sh"))
+ (("/usr/bin/env")
+ (string-append (assoc-ref inputs "coreutils") "/bin/env")))
+ #true))
+ ,@(if unwrap?
+ `((add-after 'install 'unwrap
+ (lambda* (#:key outputs #:allow-other-keys)
+ ;; The bin/idris2 calls bin/idris2_app/idris2.so which is
+ ;; the real executable, but it sets LD_LIBRARY_PATH
+ ;; incorrectly. Remove bin/idris2 and replace it with
+ ;; bin/idris2_app/idris2.so instead.
+ (let ((out (assoc-ref outputs "out")))
+ (delete-file (string-append out "/bin/idris2"))
+ (rename-file (string-append out "/bin/idris2_app/idris2.so")
+ (string-append out "/bin/idris2"))
+ (delete-file-recursively (string-append out "/bin/idris2_app"))
+ (delete-file-recursively (string-append out "/lib")))
+ #true)))
+ '())
+ ,@(if with-bootstrap-shortcut?
+ `((replace 'build
+ (lambda* (#:key make-flags #:allow-other-keys)
+ ;; i.e. do not build it using the previous version of
+ ;; Idris, but rather compile the comitted compiler
+ ;; output.
+ (apply invoke "make" "bootstrap" make-flags))))
+ '())
+ (add-after 'unwrap 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((chez (string-append (assoc-ref inputs "chez-scheme")
+ "/bin/scheme"))
+ (out (assoc-ref outputs "out"))
+ (exe (string-append out "/bin/" ,name))
+ (version ,version))
+ (wrap-program exe
+ `("IDRIS2_PREFIX" = (,out))
+ `("LD_LIBRARY_PATH" prefix (,(string-append out "/idris2-" version "/lib")))
+ `("CC" = (,',(cc-for-target)))
+ `("CHEZ" = (,chez)))
+ (with-directory-excursion (string-append out "/bin/")
+ (symlink ,name (string-append ,name "-" ,version))))
+ #true))
+ (add-after 'wrap-program 'check
+ (lambda* (#:key outputs make-flags #:allow-other-keys)
+ (,(if ignore-test-failures?
+ 'false-if-exception
+ 'begin)
+ (apply invoke "make"
+ "INTERACTIVE="
+ (string-append "IDRIS2="
+ (assoc-ref outputs "out")
+ "/bin/" ,name)
+ "test" make-flags))
+ #true)))))
+ (home-page "https://www.idris-lang.org")
+ (synopsis "General purpose language with full dependent types")
+ (description "Idris is a general purpose language with full dependent
+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. The language is closely related to
+Epigram and Agda.")
+ (license license:bsd-3)))
+
+(define-public idris2-0.5.1
+ (make-idris-package '("v0.5.1"
+ "09k5fxnplp6fv3877ynz1lwq9zapxcxbvfvkn6g68yb0ivrff978")
+ "0.5.1"))
+
;; 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.33.0
^ permalink raw reply related [flat|nested] 17+ messages in thread
* [bug#49607] [PATCH v2 1/3] gnu: idris: Use wrap-program to define IDRIS_CC
2021-07-17 15:42 [bug#49607] [PATCH] gnu: Add Idris 2 Xinglu Chen
2021-10-05 16:37 ` [bug#49607] [PATCH 1/3] gnu: ghc-cheapskate: Update to 0.1.1.2 Attila Lendvai
@ 2022-04-14 12:16 ` Attila Lendvai
2022-04-14 12:16 ` [bug#49607] [PATCH 2/3] gnu: idris: Add idris2 0.5.1, and update idris to 1.3.4 Attila Lendvai
2022-04-14 12:16 ` [bug#49607] [PATCH 3/3] gnu: idris: Add doc output and build the html documentation Attila Lendvai
2022-04-14 15:53 ` [bug#49607] a note Attila Lendvai
` (4 subsequent siblings)
6 siblings, 2 replies; 17+ messages in thread
From: Attila Lendvai @ 2022-04-14 12:16 UTC (permalink / raw)
To: 49607; +Cc: Attila Lendvai
Idris requires a C compiler at runtime to generate executables.
* gnu/packages/idris.scm (idris): Rename the scheme variable to idris-1.3.3 to
prepare for adding different versions later on.
[inputs]: Add Clang, and bash-minimal (for wrap-program).
[phases]: use (cc-for-target).
---
i think v2 is ready for inclusion. it can bootstrap idris all the way
from GHC, but it also enables a/the bootstrap shortcut for the latest
version, and disables substitution for the so called historical
versions by default.
a bootstrap shortcut is when the makefile builds a checked in build
output, which is a scheme file, using Chez Scheme.
this way the build farm is not loaded unnecessarily with building a
full chain of bootstrap, but at the same time users can trigger/install
any of the old versions manually.
gnu/packages/idris.scm | 28 ++++++++++++++++++----------
1 file changed, 18 insertions(+), 10 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index cdf76244fb..f84431cab9 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -21,10 +21,12 @@
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages bash)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
#:use-module (gnu packages libffi)
+ #:use-module (gnu packages llvm)
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ncurses)
#:use-module (gnu packages perl)
@@ -33,9 +35,10 @@ (define-module (gnu packages idris)
#: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 (guix utils))
-(define-public idris
+(define-public idris-1.3.3
(package
(name "idris")
(version "1.3.3")
@@ -56,7 +59,8 @@ (define-public idris
(list perl ghc-cheapskate ghc-tasty ghc-tasty-golden
ghc-tasty-rerun))
(inputs
- (list gmp
+ (list bash-minimal
+ gmp
ncurses
ghc-aeson
ghc-annotated-wl-pprint
@@ -95,8 +99,7 @@ (define-public idris
;; This allows us to call the 'idris' binary before installing.
(add-after 'unpack 'set-ld-library-path
(lambda _
- (setenv "LD_LIBRARY_PATH" (string-append (getcwd) "/dist/build"))
- #t))
+ (setenv "LD_LIBRARY_PATH" (string-append (getcwd) "/dist/build"))))
(add-before 'configure 'update-constraints
(lambda _
(substitute* "idris.cabal"
@@ -104,8 +107,7 @@ (define-public idris
dep))))
(add-before 'configure 'set-cc-command
(lambda _
- (setenv "CC" "gcc")
- #t))
+ (setenv "CC" ,(cc-for-target))))
(add-after 'install 'fix-libs-install-location
(lambda* (#:key outputs #:allow-other-keys)
(let* ((out (assoc-ref outputs "out"))
@@ -122,7 +124,6 @@ (define-public idris
(let ((out (assoc-ref outputs "out")))
(chmod "test/scripts/timeout" #o755) ;must be executable
(setenv "TASTY_NUM_THREADS" (number->string (parallel-job-count)))
- (setenv "IDRIS_CC" "gcc") ;Needed for creating executables
(setenv "PATH" (string-append out "/bin:" (getenv "PATH")))
(apply (assoc-ref %standard-phases 'check) args))))
(add-before 'check 'restore-libidris_rts
@@ -134,8 +135,13 @@ (define-public idris
(static (assoc-ref outputs "static"))
(filename "/lib/idris/rts/libidris_rts.a"))
(rename-file (string-append static filename)
- (string-append out filename))
- #t))))))
+ (string-append out filename)))))
+ (add-before 'check 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (exe (string-append out "/bin/idris")))
+ (wrap-program exe
+ `("IDRIS_CC" = (,',(cc-for-target))))))))))
(native-search-paths
(list (search-path-specification
(variable "IDRIS_LIBRARY_PATH")
@@ -149,6 +155,8 @@ (define-public idris
Epigram and Agda.")
(license license:bsd-3)))
+(define-public idris idris-1.3.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.35.1
^ permalink raw reply related [flat|nested] 17+ messages in thread
* [bug#49607] [PATCH 2/3] gnu: idris: Add idris2 0.5.1, and update idris to 1.3.4.
2022-04-14 12:16 ` [bug#49607] [PATCH v2 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
@ 2022-04-14 12:16 ` Attila Lendvai
2022-04-20 13:50 ` Eric Bavier
2022-04-14 12:16 ` [bug#49607] [PATCH 3/3] gnu: idris: Add doc output and build the html documentation Attila Lendvai
1 sibling, 1 reply; 17+ messages in thread
From: Attila Lendvai @ 2022-04-14 12:16 UTC (permalink / raw)
To: 49607; +Cc: Attila Lendvai
The extra generality is added so that it is possible to bootstrap Idris HEAD
all the way down from GHC. It requires patching past releases, which requires
importing them into separate git branches. This work has not been merged into
upstream yet, therefore the historical versions in this commit temprorarily
point to my own fork, as noted in the comments.
The historical versions are marked #:substitutable #false (but they are not
hidden), so that they don't load the substitute servers. Idris can bootstrap
itself from the checked in Scheme files of the ChezScheme or Racket
backends (it can take a so called 'bootstrap shortcut'), therefore the
historical versions are not necessary for compiling the latest version.
They are only needed when one wants to run the bootstrap of Idris all the
way down from Haskell (Idris 1 is written in Haskell).
Add a symlink to a versioned binary; e.g. rename the upstream's binary to
`bin/idris-1.3.4` and symlink it to `bin/idris`. This helps when multiple
versions are installed.
* gnu/packages/idris.scm (idris-1.3.4): New variable, the latest from the v1.x
line of Idris at the time of writing.
(make-idris-package): New function to instantiate a package of Idris2.
(idris2-0.5.1): New variable.
* gnu/packages/patches/idris-build-with-haskeline-0.8.patch: Deleted.
* gnu/packages/patches/idris-build-with-megaparsec-9.patch: Deleted.
* gnu/packages/patches/idris-disable-test.patch: Deleted.
---
gnu/local.mk | 3 -
gnu/packages/idris.scm | 307 +++++++++++++++++-
.../idris-build-with-haskeline-0.8.patch | 85 -----
.../idris-build-with-megaparsec-9.patch | 27 --
gnu/packages/patches/idris-disable-test.patch | 19 --
5 files changed, 293 insertions(+), 148 deletions(-)
delete mode 100644 gnu/packages/patches/idris-build-with-haskeline-0.8.patch
delete mode 100644 gnu/packages/patches/idris-build-with-megaparsec-9.patch
delete mode 100644 gnu/packages/patches/idris-disable-test.patch
diff --git a/gnu/local.mk b/gnu/local.mk
index 70133e6502..4e46b47ad9 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1283,9 +1283,6 @@ dist_patch_DATA = \
%D%/packages/patches/icedtea-7-hotspot-aarch64-use-c++98.patch\
%D%/packages/patches/id3lib-CVE-2007-4460.patch \
%D%/packages/patches/id3lib-UTF16-writing-bug.patch \
- %D%/packages/patches/idris-disable-test.patch \
- %D%/packages/patches/idris-build-with-haskeline-0.8.patch \
- %D%/packages/patches/idris-build-with-megaparsec-9.patch \
%D%/packages/patches/idris-test-ffi008.patch \
%D%/packages/patches/ilmbase-fix-tests.patch \
%D%/packages/patches/imagemagick-CVE-2020-27829.patch \
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index f84431cab9..28e918a486 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -19,9 +19,28 @@
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
+;;; TODO:
+;;;
+;;; - Idris has multiple backends, but we only register Chez as an
+;;; input. Decide how to make backends optional, and/or which ones to package
+;;; by default.
+;;;
+;;; - Set RUNPATH instead of using LD_LIBRARY_PATH. See
+;;; http://blog.tremily.us/posts/rpath/ This probably needs patching Idris
+;;; because it uses its FFI infrastrucutre to open libidris_support.so, which
+;;; is based on dlopen.
+;;;
+;;; - The reason some of the historical packages point to
+;;; github.com/attila-lendvai-patches is that these versions need some
+;;; patches to make them buildable today, and these branches haven't been
+;;; incorporated into the official repo yet. Once/if that happens, these
+;;; URL's can be changed to point to the official repo.
+
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages base)
#: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)
@@ -29,31 +48,40 @@ (define-module (gnu packages idris)
#:use-module (gnu packages llvm)
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ncurses)
+ #:use-module (gnu packages node)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages racket)
+ #:use-module (gnu packages version-control)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
#:use-module (guix download)
+ #:use-module (guix git)
#:use-module (guix git-download)
#:use-module ((guix licenses) #:prefix license:)
+ #:use-module (guix gexp)
#:use-module (guix packages)
- #:use-module (guix utils))
+ #:use-module (guix utils)
+ #:use-module (ice-9 match)
+ #:use-module (ice-9 regex)
+ #:export (make-idris-package))
-(define-public idris-1.3.3
+;;;
+;;; Idris 1
+;;;
+(define-public idris-1.3.4
(package
(name "idris")
- (version "1.3.3")
+ (version "1.3.4")
(source (origin
- (method url-fetch)
- (uri (string-append
- "https://hackage.haskell.org/package/"
- "idris-" version "/idris-" version ".tar.gz"))
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/idris-lang/Idris-dev.git")
+ (commit (string-append "v" version))))
(sha256
(base32
- "1pachwc6msw3n1mz2z1r1w6h518w9gbhdvbaa5vi1qp3cn3wm6q4"))
- (patches (search-patches "idris-disable-test.patch"
- "idris-build-with-haskeline-0.8.patch"
- "idris-build-with-megaparsec-9.patch"
- "idris-test-ffi008.patch"))))
+ "0cd2a92323hb9a6wy8sc0cqwnisf4pv8y9y2rxvxcbyv8cs1q8g2"))
+ (patches (search-patches "idris-test-ffi008.patch"))
+ (file-name (git-file-name "idris" version))))
(build-system haskell-build-system)
(native-inputs ;For tests
(list perl ghc-cheapskate ghc-tasty ghc-tasty-golden
@@ -141,7 +169,11 @@ (define-public idris-1.3.3
(let* ((out (assoc-ref outputs "out"))
(exe (string-append out "/bin/idris")))
(wrap-program exe
- `("IDRIS_CC" = (,',(cc-for-target))))))))))
+ `("IDRIS_CC" = (,',(cc-for-target))))
+ (with-directory-excursion (string-append out "/bin/")
+ (let ((versioned-name ,(string-append name "-" version)))
+ (rename-file ,name versioned-name)
+ (symlink versioned-name ,name)))))))))
(native-search-paths
(list (search-path-specification
(variable "IDRIS_LIBRARY_PATH")
@@ -155,7 +187,254 @@ (define-public idris-1.3.3
Epigram and Agda.")
(license license:bsd-3)))
-(define-public idris idris-1.3.3)
+(define-public idris idris-1.3.4)
+
+;;;
+;;; Idris 2
+;;;
+(define* (make-idris-package source idris-version
+ #:key bootstrap-idris
+ (idris-version-tag #false)
+ (guix-version (string-append
+ idris-version
+ (if idris-version-tag
+ (string-append
+ "-" idris-version-tag)
+ "")))
+ (ignore-test-failures? #false)
+ (unwrap? #true)
+ (tests? #true)
+ (historical? #false)
+ (hidden? #false) ; or (hidden? historical?)
+ (substitutable? (not historical?))
+ (files-to-patch-for-shell
+ '("src/Compiler/Scheme/Chez.idr"
+ "src/Compiler/Scheme/Racket.idr"
+ "src/Compiler/Scheme/Gambit.idr"
+ "src/Compiler/ES/Node.idr"
+ "bootstrap/idris2_app/idris2.rkt"
+ "bootstrap/idris2_app/idris2.ss"
+ "build/stage1/idris2_app/idris2.ss"
+ "build/stage1/idris2_app/idris2.rkt"
+ ))
+ (with-bootstrap-shortcut? (not historical?)))
+ "HISTORICAL? means that it's only interesting for historical reasons, e.g. to be
+used as a bootsrapping stage.
+
+WITH-BOOTSTRAP-SHORTCUT? controls whether to use a previous version of Idris to
+build us (which is potentially recursive), or use the captured compiler output
+(Scheme code)."
+ (package
+ (name "idris2")
+ (version guix-version)
+ (source (match source
+ ((commit hash . url)
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url (if (null? url)
+ "https://github.com/idris-lang/Idris2.git"
+ (car url)))
+ (commit commit)))
+ (sha256 (base32 hash))
+ (file-name (git-file-name name version))))
+ ((or (? git-checkout?)
+ (? local-file?))
+ source)))
+ (build-system gnu-build-system)
+ (native-inputs
+ (list (if with-bootstrap-shortcut?
+ chez-scheme
+ bootstrap-idris)
+ clang-toolchain-12 ; older clang-toolchain versions don't have a bin/cc
+ coreutils which git
+ node ; only for the tests
+ racket ; only for the tests
+ sed))
+ (inputs
+ (list bash-minimal chez-scheme gmp))
+ (arguments
+ (list
+ #:tests? tests?
+ #:substitutable? substitutable?
+ #:make-flags
+ #~(list (string-append "CC=" #$(cc-for-target))
+ #$(string-append "IDRIS_VERSION=" idris-version)
+ #$(string-append "IDRIS_VERSION_TAG=" (or idris-version-tag ""))
+ #$(if with-bootstrap-shortcut?
+ #~(string-append "SCHEME="
+ #$(this-package-input "chez-scheme")
+ "/bin/scheme")
+ #~(string-append "BOOTSTRAP_IDRIS="
+ #$bootstrap-idris
+ "/bin/" #$(package-name bootstrap-idris)))
+ (string-append "PREFIX=" (assoc-ref %outputs "out"))
+ "-j1")
+ #:phases
+ `(modify-phases %standard-phases
+ (delete 'bootstrap)
+ (delete 'configure)
+ (delete 'check) ; check must happen after install and wrap-program
+ (add-after 'unpack 'patch-paths
+ (lambda* (#:key inputs #:allow-other-keys)
+ (let ((files-to-patch (filter file-exists?
+ ',files-to-patch-for-shell)))
+ (substitute* files-to-patch
+ ((,(regexp-quote "#!/bin/sh"))
+ (string-append "#!" (assoc-ref inputs "bash") "/bin/sh"))
+ (("/usr/bin/env")
+ (string-append (assoc-ref inputs "coreutils") "/bin/env"))))))
+ ,@(if unwrap?
+ `((add-after 'install 'unwrap
+ (lambda* (#:key outputs #:allow-other-keys)
+ ;; The bin/idris2 calls bin/idris2_app/idris2.so which is
+ ;; the real executable, but it sets LD_LIBRARY_PATH
+ ;; incorrectly. Remove bin/idris2 and replace it with
+ ;; bin/idris2_app/idris2.so instead.
+ (let* ((out (assoc-ref outputs "out"))
+ (image-base (string-append
+ out "/bin/idris2_app/idris2"))
+ (image (if (file-exists? image-base)
+ image-base
+ ;; For v0.5.1 and older.
+ (string-append image-base ".so"))))
+ (delete-file (string-append out "/bin/idris2"))
+ (rename-file image (string-append out "/bin/idris2"))
+ (delete-file-recursively (string-append out "/bin/idris2_app"))
+ (delete-file-recursively (string-append out "/lib"))))))
+ '())
+ ,@(if with-bootstrap-shortcut?
+ `((replace 'build
+ (lambda* (#:key make-flags #:allow-other-keys)
+ ;; i.e. do not build it using the previous version of
+ ;; Idris, but rather compile the comitted compiler
+ ;; output.
+ (apply invoke "make" "bootstrap" make-flags))))
+ '())
+ (add-after 'unwrap 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((chez (string-append (assoc-ref inputs "chez-scheme")
+ "/bin/scheme"))
+ (out (assoc-ref outputs "out"))
+ (exe (string-append out "/bin/" ,name))
+ (version ,idris-version))
+ (wrap-program exe
+ `("IDRIS2_PREFIX" = (,out))
+ `("LD_LIBRARY_PATH" prefix (,(string-append
+ out "/idris2-" version "/lib")))
+ `("CC" = (,',(cc-for-target)))
+ `("CHEZ" = (,chez)))
+ (with-directory-excursion (string-append out "/bin/")
+ (let ((versioned-name ,(string-append name "-" version)))
+ (rename-file ,name versioned-name)
+ (symlink versioned-name ,name))))))
+ (add-after 'wrap-program 'check
+ (lambda* (#:key outputs make-flags #:allow-other-keys)
+ (let ((invoke-make
+ (lambda (target)
+ (apply invoke "make"
+ "INTERACTIVE="
+ ;; "THREADS=1" ; for reproducible test output
+ (string-append "IDRIS2="
+ (assoc-ref outputs "out")
+ "/bin/" ,name)
+ target make-flags))))
+ ;; TODO This is something like how it should be handled, but
+ ;; the Makefile unconditionally invokes the `testenv` target,
+ ;; and thus overwrites the `runtest` script when `make test` is
+ ;; invoked. For now this situation is resolved in the Idris
+ ;; Makefile, by explicitly invoking the Idris `runtest` wrapper
+ ;; script with an sh prefix.
+ ;;
+ ;;(invoke-make "testenv")
+ ;;(patch-shebang "build/stage2/runtests")
+ (,(if ignore-test-failures?
+ 'false-if-exception
+ 'begin)
+ (invoke-make "test"))))))))
+ (properties `((hidden? . ,hidden?)))
+ (home-page "https://www.idris-lang.org")
+ (synopsis "General purpose language with full dependent types")
+ (description "Idris is a general purpose language with full dependent
+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. The language is closely related to
+Epigram and Agda.")
+ (license license:bsd-3)))
+
+(define-public idris2-0.1.1
+ ;; branch idris.2
+ ;; This is the first (untagged) Idris2 version that bootstraps off of the
+ ;; Idris1 line. Originally it was in the repo called Idris2-boot.
+ (make-idris-package '("3c2335ee6bc00b7f417ac672a4ab7b73599abeb3"
+ "10w10ggyvlw7m1pazbfxr4sj3wpb6z1ap6rg3lxc0z6f2s3x53cb")
+ "0.1.1"
+ #:bootstrap-idris idris-1.3.4
+ #:historical? #true
+ #:unwrap? #false
+ ;; TODO `make bootstrap` needs to be backported into the
+ ;; Makefile in this branch. Force the bootstrap
+ ;; shortcut to be turned off.
+ #:with-bootstrap-shortcut? #false))
+
+(define-public idris2-0.2.1
+ ;; branch idris.3
+ (make-idris-package '("257bbc27498808e8cd4155cc06ea3f6a07541537"
+ "0idxplcmd6p13i2n0g49bc2snddny4kdr4wvd8854snzsiwqn7p1"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.2.1"
+ #:bootstrap-idris idris2-0.1.1
+ #:historical? #true))
+
+(define-public idris2-0.2.2
+ ;; branch idris.4
+ (make-idris-package '("9bc8e6e9834cbc7b52dc6ca2d80d7e96afeb47d1"
+ "0xzl1mb5yxgp6v36rngy00i59cfy67niyiblcpaksllrgmg639p4"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.2.2"
+ #:bootstrap-idris idris2-0.2.1
+ #:historical? #true))
+
+(define-public idris2-0.3.0
+ ;; branch idris.5
+ (make-idris-package '("025b5cd25b76eae28283a10bd155c384e46fbd82"
+ "00a83paib571ahknipmgw7g9pbym105isk3bz0c1ng41s4kjpsxh"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.3.0"
+ #:bootstrap-idris idris2-0.2.2
+ #:historical? #true))
+
+(define-public idris2-0.4.0
+ ;; branch idris.6
+ (make-idris-package '("v0.4.0"
+ "105jybjf5s0k6003qzfxchzsfcpsxip180bh3mdmi74d464d0h8g")
+ "0.4.0"
+ #:bootstrap-idris idris2-0.3.0
+ #:ignore-test-failures? #true ; TODO investigate
+ #:historical? #true))
+
+(define-public idris2-0.5.1
+ (make-idris-package '("v0.5.1"
+ "09k5fxnplp6fv3877ynz1lwq9zapxcxbvfvkn6g68yb0ivrff978")
+ "0.5.1"))
+
+;; TODO re build failure: in the build sandbox some parts of the test output
+;; is missing. I cannot reproduce it in a guix shell. My assumption is that
+;; it's an Idris bug that only manifests in certain circumstances. There are
+;; some other issues left with the use of #!/bin/sh, too.
+(define-public idris2-dev
+ (make-idris-package '("4bb12225424d76c7874b176e2bfb8b5550c112eb"
+ "0kb800cgfm0afa83pbyi3x9bpswcl8jz4pr68zy092fs50km3bj7"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.5.1"
+ #:ignore-test-failures? #true
+ #:idris-version-tag "dev"))
+
+(define-public idris2 idris2-0.5.1)
+
+;;;
+;;; Idris apps
+;;;
;; Idris modules use the gnu-build-system so that the IDRIS_LIBRARY_PATH is set.
(define (idris-default-arguments name)
diff --git a/gnu/packages/patches/idris-build-with-haskeline-0.8.patch b/gnu/packages/patches/idris-build-with-haskeline-0.8.patch
deleted file mode 100644
index 5d1fec2409..0000000000
--- a/gnu/packages/patches/idris-build-with-haskeline-0.8.patch
+++ /dev/null
@@ -1,85 +0,0 @@
-From 89a87cf666eb8b27190c779e72d0d76eadc1bc14 Mon Sep 17 00:00:00 2001
-From: Niklas Larsson <niklas@mm.st>
-Date: Sat, 6 Jun 2020 15:29:45 +0200
-Subject: [PATCH] Fix to unblock haskeline-0.8
-
----
-Taken from <https://github.com/idris-lang/Idris-dev/pull/4871>
-
- idris.cabal | 2 +-
- src/Idris/Output.hs | 8 --------
- src/Idris/REPL.hs | 12 +++++-------
- 3 files changed, 6 insertions(+), 16 deletions(-)
-
-diff --git a/idris.cabal b/idris.cabal
-index 38359019a9..bc9e265023 100644
---- a/idris.cabal
-+++ b/idris.cabal
-@@ -336,7 +336,7 @@ Library
- , directory >= 1.2.2.0 && < 1.2.3.0 || > 1.2.3.0
- , filepath < 1.5
- , fingertree >= 0.1.4.1 && < 0.2
-- , haskeline >= 0.7 && < 0.8
-+ , haskeline >= 0.8 && < 0.9
- , ieee754 >= 0.7 && < 0.9
- , megaparsec >= 7.0.4 && < 9
- , mtl >= 2.1 && < 2.3
-diff --git a/src/Idris/Output.hs b/src/Idris/Output.hs
-index 70b4d48a30..6b5d59948c 100644
---- a/src/Idris/Output.hs
-+++ b/src/Idris/Output.hs
-@@ -37,21 +37,13 @@ import Prelude hiding ((<$>))
- #endif
-
- import Control.Arrow (first)
--import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)
- import Data.List (intersperse, nub)
- import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe)
- import qualified Data.Set as S
--import System.Console.Haskeline.MonadException (MonadException(controlIO),
-- RunIO(RunIO))
- import System.FilePath (replaceExtension)
- import System.IO (Handle, hPutStr, hPutStrLn)
- import System.IO.Error (tryIOError)
-
--instance MonadException m => MonadException (ExceptT Err m) where
-- controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
-- run' = RunIO (fmap ExceptT . run . runExceptT)
-- in fmap runExceptT $ f run'
--
- pshow :: IState -> Err -> String
- pshow ist err = displayDecorated (consoleDecorate ist) .
- renderPretty 1.0 80 .
-diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
-index 05587d9672..5e0dc21089 100644
---- a/src/Idris/REPL.hs
-+++ b/src/Idris/REPL.hs
-@@ -122,23 +122,21 @@ repl orig mods efile
- (if colour && not isWindows
- then colourisePrompt theme str
- else str) ++ " "
-- x <- H.catch (H.withInterrupt $ getInputLine prompt)
-- (ctrlC (return $ Just ""))
-+ x <- H.handleInterrupt (ctrlC (return $ Just "")) (H.withInterrupt $ getInputLine prompt)
- case x of
- Nothing -> do lift $ when (not quiet) (iputStrLn "Bye bye")
- return ()
- Just input -> -- H.catch
-- do ms <- H.catch (H.withInterrupt $ lift $ processInput input orig mods efile)
-- (ctrlC (return (Just mods)))
-+ do ms <- H.handleInterrupt (ctrlC (return (Just mods))) (H.withInterrupt $ lift $ processInput input orig mods efile)
- case ms of
- Just mods -> let efile' = fromMaybe efile (listToMaybe mods)
- in repl orig mods efile'
- Nothing -> return ()
- -- ctrlC)
- -- ctrlC
-- where ctrlC :: InputT Idris a -> SomeException -> InputT Idris a
-- ctrlC act e = do lift $ iputStrLn (show e)
-- act -- repl orig mods
-+ where ctrlC :: InputT Idris a -> InputT Idris a
-+ ctrlC act = do lift $ iputStrLn "Interrupted"
-+ act -- repl orig mods
-
- showMVs c thm [] = ""
- showMVs c thm ms = "Holes: " ++
diff --git a/gnu/packages/patches/idris-build-with-megaparsec-9.patch b/gnu/packages/patches/idris-build-with-megaparsec-9.patch
deleted file mode 100644
index 6d7ff1d713..0000000000
--- a/gnu/packages/patches/idris-build-with-megaparsec-9.patch
+++ /dev/null
@@ -1,27 +0,0 @@
-From 6ea9bc913877d765048d7cdb7fc5aec60b196fac Mon Sep 17 00:00:00 2001
-From: Felix Yan <felixonmars@archlinux.org>
-Date: Wed, 16 Dec 2020 21:48:32 +0800
-Subject: [PATCH] Fix compatibility with megaparsec 9
-
----
-Taken from <https://github.com/idris-lang/Idris-dev/pull/4892>
-
- src/Idris/Parser/Stack.hs | 4 ++++
- 1 file changed, 4 insertions(+)
-
-diff --git a/src/Idris/Parser/Stack.hs b/src/Idris/Parser/Stack.hs
-index fb7b611440..879786f4d2 100644
---- a/src/Idris/Parser/Stack.hs
-+++ b/src/Idris/Parser/Stack.hs
-@@ -84,7 +84,11 @@ instance Message ParseError where
- (pos, _) = P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)
- #endif
- messageText = PP.text . init . P.parseErrorTextPretty . parseError
-+#if MIN_VERSION_megaparsec(9,0,0)
-+ messageSource err = sline
-+#else
- messageSource err = Just sline
-+#endif
- where
- #if MIN_VERSION_megaparsec(8,0,0)
- (sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)
diff --git a/gnu/packages/patches/idris-disable-test.patch b/gnu/packages/patches/idris-disable-test.patch
deleted file mode 100644
index ec8c7c8451..0000000000
--- a/gnu/packages/patches/idris-disable-test.patch
+++ /dev/null
@@ -1,19 +0,0 @@
-The "pkg010" test output depends on the version of optparse-applicative being
-used. The expected output requires optparse-applicative >= 0.15.1.0. Skip
-the test for now.
-
---- idris-1.3.3/test/TestData.hs 2021-01-19 23:05:24.238958262 -0600
-+++ idris-1.3.3/test/TestData.hs 2021-01-19 23:10:33.314390997 -0600
-@@ -212,8 +212,10 @@
- ( 5, ANY ),
- ( 6, ANY ),
- ( 7, ANY ),
-- ( 8, ANY ),
-- ( 10, ANY )]),
-+ ( 8, ANY )]),
-+-- FIXME: Expected output depends on optparse-applicative version.
-+-- See https://github.com/idris-lang/Idris-dev/issues/4896
-+-- ( 10, ANY )]),
- ("prelude", "Prelude",
- [ ( 1, ANY )]),
- ("primitives", "Primitive types",
--
2.35.1
^ permalink raw reply related [flat|nested] 17+ messages in thread
* [bug#49607] [PATCH 3/3] gnu: idris: Add doc output and build the html documentation.
2022-04-14 12:16 ` [bug#49607] [PATCH v2 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
2022-04-14 12:16 ` [bug#49607] [PATCH 2/3] gnu: idris: Add idris2 0.5.1, and update idris to 1.3.4 Attila Lendvai
@ 2022-04-14 12:16 ` Attila Lendvai
1 sibling, 0 replies; 17+ messages in thread
From: Attila Lendvai @ 2022-04-14 12:16 UTC (permalink / raw)
To: 49607; +Cc: Attila Lendvai
* gnu/packages/idris.scm (make-idris-package): Build the html docs and install
it into the doc output.
---
gnu/packages/idris.scm | 23 ++++++++++++++++++++---
1 file changed, 20 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 28e918a486..b9b309d6d5 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -50,7 +50,9 @@ (define-module (gnu packages idris)
#:use-module (gnu packages ncurses)
#:use-module (gnu packages node)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages python)
#:use-module (gnu packages racket)
+ #:use-module (gnu packages sphinx)
#:use-module (gnu packages version-control)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
@@ -248,11 +250,17 @@ (define* (make-idris-package source idris-version
bootstrap-idris)
clang-toolchain-12 ; older clang-toolchain versions don't have a bin/cc
coreutils which git
- node ; only for the tests
- racket ; only for the tests
- sed))
+ sed
+ ;; Only for the tests
+ node
+ racket
+ ;; Only for the docs
+ python-minimal
+ python-sphinx
+ python-sphinx-rtd-theme))
(inputs
(list bash-minimal chez-scheme gmp))
+ (outputs '("out" "doc"))
(arguments
(list
#:tests? tests?
@@ -275,6 +283,15 @@ (define* (make-idris-package source idris-version
(delete 'bootstrap)
(delete 'configure)
(delete 'check) ; check must happen after install and wrap-program
+ (add-before 'build 'build-doc
+ (lambda* (#:key outputs #:allow-other-keys)
+ (invoke "make" "--directory" "docs/" "html")))
+ (add-after 'build-doc 'install-doc
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((doc (assoc-ref outputs "doc")))
+ (copy-recursively "docs/build/html"
+ (string-append doc "/share/doc/"
+ ,name "-" ,version)))))
(add-after 'unpack 'patch-paths
(lambda* (#:key inputs #:allow-other-keys)
(let ((files-to-patch (filter file-exists?
--
2.35.1
^ permalink raw reply related [flat|nested] 17+ messages in thread
* [bug#49607] a note
2021-07-17 15:42 [bug#49607] [PATCH] gnu: Add Idris 2 Xinglu Chen
2021-10-05 16:37 ` [bug#49607] [PATCH 1/3] gnu: ghc-cheapskate: Update to 0.1.1.2 Attila Lendvai
2022-04-14 12:16 ` [bug#49607] [PATCH v2 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
@ 2022-04-14 15:53 ` Attila Lendvai
2022-04-28 13:28 ` [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
` (3 subsequent siblings)
6 siblings, 0 replies; 17+ messages in thread
From: Attila Lendvai @ 2022-04-14 15:53 UTC (permalink / raw)
To: 49607@debbugs.gnu.org
note that some of these packages are pointing to my own fork of the Idris2 repo.
if that is an issue, then feel free to comment out those packages for the time being.
i'm working on incorporating these branches back into the official Idris2 repo.
(the current milestone of that process is to get my build system refactor merged https://github.com/idris-lang/Idris2/pull/1990)
--
• attila lendvai
• PGP: 963F 5D5F 45C7 DFCD 0A39
--
“Journalism is printing what someone else does not want printed: everything else is public relations.”
— George Orwell (1903–1950)
^ permalink raw reply [flat|nested] 17+ messages in thread
* [bug#49607] [PATCH 2/3] gnu: idris: Add idris2 0.5.1, and update idris to 1.3.4.
2022-04-14 12:16 ` [bug#49607] [PATCH 2/3] gnu: idris: Add idris2 0.5.1, and update idris to 1.3.4 Attila Lendvai
@ 2022-04-20 13:50 ` Eric Bavier
0 siblings, 0 replies; 17+ messages in thread
From: Eric Bavier @ 2022-04-20 13:50 UTC (permalink / raw)
To: 49607
Hi!
On Thu, 2022-04-14 at 14:16 +0200, Attila Lendvai wrote:
> * gnu/packages/idris.scm (idris-1.3.4): New variable, the latest from
> the v1.x
> line of Idris at the time of writing.
> (make-idris-package): New function to instantiate a package of
> Idris2.
> (idris2-0.5.1): New variable.
> * gnu/packages/patches/idris-build-with-haskeline-0.8.patch: Deleted.
> * gnu/packages/patches/idris-build-with-megaparsec-9.patch: Deleted.
> * gnu/packages/patches/idris-disable-test.patch: Deleted.
> ---
> gnu/local.mk | 3 -
> gnu/packages/idris.scm | 307
> +++++++++++++++++-
> .../idris-build-with-haskeline-0.8.patch | 85 -----
> .../idris-build-with-megaparsec-9.patch | 27 --
> gnu/packages/patches/idris-disable-test.patch | 19 --
> 5 files changed, 293 insertions(+), 148 deletions(-)
> delete mode 100644 gnu/packages/patches/idris-build-with-haskeline-
> 0.8.patch
> delete mode 100644 gnu/packages/patches/idris-build-with-megaparsec-
> 9.patch
> delete mode 100644 gnu/packages/patches/idris-disable-test.patch
I've pushed the 1.3.4 update portion of this patch in commit
0cf1178a65. I am still reviewing the rest.
`~Eric
^ permalink raw reply [flat|nested] 17+ messages in thread
* [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC
2021-07-17 15:42 [bug#49607] [PATCH] gnu: Add Idris 2 Xinglu Chen
` (2 preceding siblings ...)
2022-04-14 15:53 ` [bug#49607] a note Attila Lendvai
@ 2022-04-28 13:28 ` Attila Lendvai
2022-04-28 13:28 ` [bug#49607] [PATCH v3 2/3] gnu: idris: Add idris2 0.5.1 Attila Lendvai
` (2 more replies)
2022-07-11 10:41 ` [bug#49607] why not to propagate gcc as a dependency Attila Lendvai
` (2 subsequent siblings)
6 siblings, 3 replies; 17+ messages in thread
From: Attila Lendvai @ 2022-04-28 13:28 UTC (permalink / raw)
To: 49607; +Cc: Attila Lendvai
Idris requires a C compiler at runtime to generate executables.
* gnu/packages/idris.scm (idris) [inputs]: Add bash-minimal (for wrap-program).
[phases]: Add wrap-program phase to define IDRIS_CC, use (cc-for-target).
---
v3: i have rebased them to master, i.e. on top of the idris-1.3.4 update.
it also cleans it up a bit more (e.g. got rid of the clang-toolchain dependency).
gnu/packages/idris.scm | 15 ++++++++++++---
1 file changed, 12 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 8f08ed3a3e..61de4883b1 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -22,6 +22,7 @@
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages bash)
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (gnu packages haskell-xyz)
@@ -35,7 +36,8 @@ (define-module (gnu packages idris)
#:use-module (guix git-download)
#:use-module (guix utils)
#:use-module ((guix licenses) #:prefix license:)
- #:use-module (guix packages))
+ #:use-module (guix packages)
+ #:use-module (guix utils))
(define-public idris
(package
@@ -56,7 +58,8 @@ (define-public idris
(list perl ghc-cheapskate ghc-tasty ghc-tasty-golden
ghc-tasty-rerun))
(inputs
- (list gmp
+ (list bash-minimal
+ gmp
ncurses
ghc-aeson
ghc-annotated-wl-pprint
@@ -132,7 +135,13 @@ (define-public idris
(static (assoc-ref outputs "static"))
(filename "/lib/idris/rts/libidris_rts.a"))
(rename-file (string-append static filename)
- (string-append out filename))))))))
+ (string-append out filename)))))
+ (add-before 'check 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (exe (string-append out "/bin/idris")))
+ (wrap-program exe
+ `("IDRIS_CC" = (,',(cc-for-target))))))))))
(native-search-paths
(list (search-path-specification
(variable "IDRIS_LIBRARY_PATH")
--
2.35.1
^ permalink raw reply related [flat|nested] 17+ messages in thread
* [bug#49607] [PATCH v3 2/3] gnu: idris: Add idris2 0.5.1.
2022-04-28 13:28 ` [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
@ 2022-04-28 13:28 ` Attila Lendvai
2022-04-28 13:28 ` [bug#49607] [PATCH v3 3/3] gnu: idris: Add doc output and build the html documentation Attila Lendvai
2022-05-17 20:04 ` [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Eric Bavier
2 siblings, 0 replies; 17+ messages in thread
From: Attila Lendvai @ 2022-04-28 13:28 UTC (permalink / raw)
To: 49607; +Cc: Attila Lendvai
The extra generality (e.g. the make-idris-package function) is added so that
it becomes possible to bootstrap Idris HEAD all the way down from GHC. Some
of the past releases require patching, which in turn requires importing them
into separate git branches. This work has not been merged into upstream yet,
therefore some of the historical versions in this commit temprorarily point to
my own fork, as noted in the comments.
The historical versions are marked #:substitutable #false (but they are not
hidden), so that they don't load the substitute servers unnecessarily, but at
the same time are installable.
Idris can bootstrap itself from the checked in Scheme files of the ChezScheme
or Racket backends (it can take a so called 'bootstrap shortcut'), therefore
the historical versions are not needed for compiling the latest version. They
are only needed when one wants to run the bootstrap of Idris all the way down
from Haskell (Idris 1 is written in Haskell).
Create binaries with the version in their name, and add a symlink to them;
e.g. rename the upstream's binary to `bin/idris-1.3.4` and symlink it to
`bin/idris`. This helps when multiple versions are installed.
* gnu/packages/idris.scm (idris): Rename the scheme variable to idris-1.3.
(make-idris-package): New function to instantiate a package of Idris2.
(idris2, idris2-0.1.1, idris2-0.2.1, idris2-0.2.2, idris2-0.3.0, idris2-0.4.0,
idris2-dev): New variables.
---
gnu/packages/idris.scm | 288 ++++++++++++++++++++++++++++++++++++++++-
1 file changed, 285 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 61de4883b1..1488996b6a 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -20,26 +20,56 @@
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
+;;; TODO:
+;;;
+;;; - Idris has multiple backends, but we only register Chez as an
+;;; input. Decide how to make backends optional, and/or which ones to package
+;;; by default.
+;;;
+;;; - Set RUNPATH instead of using LD_LIBRARY_PATH. See
+;;; http://blog.tremily.us/posts/rpath/ This probably needs patching Idris
+;;; because it uses its FFI infrastrucutre to open libidris_support.so, which
+;;; is based on dlopen.
+;;;
+;;; - The reason some of the historical packages point to
+;;; github.com/attila-lendvai-patches is that these versions need some
+;;; patches to make them buildable today, and these branches haven't been
+;;; incorporated into the official repo yet. Once/if that happens, these
+;;; URL's can be changed to point to the official repo.
+
(define-module (gnu packages idris)
#:use-module (gnu packages)
+ #:use-module (gnu packages base)
#: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)
#:use-module (gnu packages libffi)
#:use-module (gnu packages multiprecision)
#:use-module (gnu packages ncurses)
+ #:use-module (gnu packages node)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages racket)
+ #:use-module (gnu packages version-control)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
#:use-module (guix download)
+ #:use-module (guix git)
#:use-module (guix git-download)
#:use-module (guix utils)
#:use-module ((guix licenses) #:prefix license:)
+ #:use-module (guix gexp)
#:use-module (guix packages)
- #:use-module (guix utils))
+ #:use-module (guix utils)
+ #:use-module (ice-9 match)
+ #:use-module (ice-9 regex)
+ #:export (make-idris-package))
-(define-public idris
+;;;
+;;; Idris 1
+;;;
+(define-public idris-1.3
(package
(name "idris")
(version "1.3.4")
@@ -141,7 +171,11 @@ (define-public idris
(let* ((out (assoc-ref outputs "out"))
(exe (string-append out "/bin/idris")))
(wrap-program exe
- `("IDRIS_CC" = (,',(cc-for-target))))))))))
+ `("IDRIS_CC" = (,',(cc-for-target))))
+ (with-directory-excursion (string-append out "/bin/")
+ (let ((versioned-name ,(string-append name "-" version)))
+ (rename-file ,name versioned-name)
+ (symlink versioned-name ,name)))))))))
(native-search-paths
(list (search-path-specification
(variable "IDRIS_LIBRARY_PATH")
@@ -155,6 +189,254 @@ (define-public idris
Epigram and Agda.")
(license license:bsd-3)))
+(define-public idris idris-1.3)
+
+;;;
+;;; Idris 2
+;;;
+(define* (make-idris-package source idris-version
+ #:key bootstrap-idris
+ (idris-version-tag #false)
+ (guix-version (string-append
+ idris-version
+ (if idris-version-tag
+ (string-append
+ "-" idris-version-tag)
+ "")))
+ (ignore-test-failures? #false)
+ (unwrap? #true)
+ (tests? #true)
+ (historical? #false)
+ (hidden? #false) ; or (hidden? historical?)
+ (substitutable? (not historical?))
+ (files-to-patch-for-shell
+ '("src/Compiler/Scheme/Chez.idr"
+ "src/Compiler/Scheme/Racket.idr"
+ "src/Compiler/Scheme/Gambit.idr"
+ "src/Compiler/ES/Node.idr"
+ "bootstrap/idris2_app/idris2.rkt"
+ "bootstrap/idris2_app/idris2.ss"
+ "build/stage1/idris2_app/idris2.ss"
+ "build/stage1/idris2_app/idris2.rkt"
+ ))
+ (with-bootstrap-shortcut? (not historical?)))
+ "HISTORICAL? means that it's only interesting for historical reasons, e.g. to be
+used as a bootsrapping stage.
+
+WITH-BOOTSTRAP-SHORTCUT? controls whether to use a previous version of Idris to
+build us (which is potentially recursive), or use the captured compiler output
+(Scheme code)."
+ (package
+ (name "idris2")
+ (version guix-version)
+ (source (match source
+ ((commit hash . url)
+ (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url (if (null? url)
+ "https://github.com/idris-lang/Idris2.git"
+ (car url)))
+ (commit commit)))
+ (sha256 (base32 hash))
+ (file-name (git-file-name name version))))
+ ((or (? git-checkout?)
+ (? local-file?))
+ source)))
+ (build-system gnu-build-system)
+ (native-inputs
+ (list (if with-bootstrap-shortcut?
+ chez-scheme
+ bootstrap-idris)
+ coreutils which git
+ node ; only for the tests
+ racket ; only for the tests
+ sed))
+ (inputs
+ (list bash-minimal chez-scheme gmp))
+ (arguments
+ (list
+ #:tests? tests?
+ #:substitutable? substitutable?
+ #:make-flags
+ #~(list (string-append "CC=" #$(cc-for-target))
+ #$(string-append "IDRIS_VERSION=" idris-version)
+ #$(string-append "IDRIS_VERSION_TAG=" (or idris-version-tag ""))
+ #$(if with-bootstrap-shortcut?
+ #~(string-append "SCHEME="
+ #$(this-package-input "chez-scheme")
+ "/bin/scheme")
+ #~(string-append "BOOTSTRAP_IDRIS="
+ #$bootstrap-idris
+ "/bin/" #$(package-name bootstrap-idris)))
+ (string-append "PREFIX=" (assoc-ref %outputs "out"))
+ "-j1")
+ #:phases
+ `(modify-phases %standard-phases
+ (delete 'bootstrap)
+ (delete 'configure)
+ (delete 'check) ; check must happen after install and wrap-program
+ (add-after 'unpack 'patch-paths
+ (lambda* (#:key inputs #:allow-other-keys)
+ (let ((files-to-patch (filter file-exists?
+ ',files-to-patch-for-shell)))
+ (substitute* files-to-patch
+ ((,(regexp-quote "#!/bin/sh"))
+ (string-append "#!" (assoc-ref inputs "bash") "/bin/sh"))
+ (("/usr/bin/env")
+ (string-append (assoc-ref inputs "coreutils") "/bin/env"))))))
+ ,@(if unwrap?
+ `((add-after 'install 'unwrap
+ (lambda* (#:key outputs #:allow-other-keys)
+ ;; The bin/idris2 calls bin/idris2_app/idris2.so which is
+ ;; the real executable, but it sets LD_LIBRARY_PATH
+ ;; incorrectly. Remove bin/idris2 and replace it with
+ ;; bin/idris2_app/idris2.so instead.
+ (let* ((out (assoc-ref outputs "out"))
+ (image-base (string-append
+ out "/bin/idris2_app/idris2"))
+ (image (if (file-exists? image-base)
+ image-base
+ ;; For v0.5.1 and older.
+ (string-append image-base ".so"))))
+ (delete-file (string-append out "/bin/idris2"))
+ (rename-file image (string-append out "/bin/idris2"))
+ (delete-file-recursively (string-append out "/bin/idris2_app"))
+ (delete-file-recursively (string-append out "/lib"))))))
+ '())
+ ,@(if with-bootstrap-shortcut?
+ `((replace 'build
+ (lambda* (#:key make-flags #:allow-other-keys)
+ ;; i.e. do not build it using the previous version of
+ ;; Idris, but rather compile the comitted compiler
+ ;; output.
+ (apply invoke "make" "bootstrap" make-flags))))
+ '())
+ (add-after 'unwrap 'wrap-program
+ (lambda* (#:key outputs inputs #:allow-other-keys)
+ (let* ((chez (string-append (assoc-ref inputs "chez-scheme")
+ "/bin/scheme"))
+ (out (assoc-ref outputs "out"))
+ (exe (string-append out "/bin/" ,name))
+ (version ,idris-version))
+ (wrap-program exe
+ `("IDRIS2_PREFIX" = (,out))
+ `("LD_LIBRARY_PATH" prefix (,(string-append
+ out "/idris2-" version "/lib")))
+ `("CC" = (,',(cc-for-target)))
+ `("CHEZ" = (,chez)))
+ (with-directory-excursion (string-append out "/bin/")
+ (let ((versioned-name ,(string-append name "-" version)))
+ (rename-file ,name versioned-name)
+ (symlink versioned-name ,name))))))
+ (add-after 'wrap-program 'check
+ (lambda* (#:key outputs make-flags #:allow-other-keys)
+ (let ((invoke-make
+ (lambda (target)
+ (apply invoke "make"
+ "INTERACTIVE="
+ ;; "THREADS=1" ; for reproducible test output
+ (string-append "IDRIS2="
+ (assoc-ref outputs "out")
+ "/bin/" ,name)
+ target make-flags))))
+ ;; TODO This is something like how it should be handled, but
+ ;; the Makefile unconditionally invokes the `testenv` target,
+ ;; and thus overwrites the `runtest` script when `make test` is
+ ;; invoked. For now this situation is resolved in the Idris
+ ;; Makefile, by explicitly invoking the Idris `runtest` wrapper
+ ;; script with an sh prefix.
+ ;;
+ ;;(invoke-make "testenv")
+ ;;(patch-shebang "build/stage2/runtests")
+ (,(if ignore-test-failures?
+ 'false-if-exception
+ 'begin)
+ (invoke-make "test"))))))))
+ (properties `((hidden? . ,hidden?)))
+ (home-page "https://www.idris-lang.org")
+ (synopsis "General purpose language with full dependent types")
+ (description "Idris is a general purpose language with full dependent
+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. The language is closely related to
+Epigram and Agda.")
+ (license license:bsd-3)))
+
+(define-public idris2-0.1.1
+ ;; branch idris.2
+ ;; This is the first (untagged) Idris2 version that bootstraps off of the
+ ;; Idris1 line. Originally it was in the repo called Idris2-boot.
+ (make-idris-package '("3c2335ee6bc00b7f417ac672a4ab7b73599abeb3"
+ "10w10ggyvlw7m1pazbfxr4sj3wpb6z1ap6rg3lxc0z6f2s3x53cb")
+ "0.1.1"
+ #:bootstrap-idris idris-1.3
+ #:historical? #true
+ #:unwrap? #false
+ ;; TODO `make bootstrap` needs to be backported into the
+ ;; Makefile in this branch. Force the bootstrap
+ ;; shortcut to be turned off.
+ #:with-bootstrap-shortcut? #false))
+
+(define-public idris2-0.2.1
+ ;; branch idris.3
+ (make-idris-package '("257bbc27498808e8cd4155cc06ea3f6a07541537"
+ "0idxplcmd6p13i2n0g49bc2snddny4kdr4wvd8854snzsiwqn7p1"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.2.1"
+ #:bootstrap-idris idris2-0.1.1
+ #:historical? #true))
+
+(define-public idris2-0.2.2
+ ;; branch idris.4
+ (make-idris-package '("9bc8e6e9834cbc7b52dc6ca2d80d7e96afeb47d1"
+ "0xzl1mb5yxgp6v36rngy00i59cfy67niyiblcpaksllrgmg639p4"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.2.2"
+ #:bootstrap-idris idris2-0.2.1
+ #:historical? #true))
+
+(define-public idris2-0.3.0
+ ;; branch idris.5
+ (make-idris-package '("025b5cd25b76eae28283a10bd155c384e46fbd82"
+ "00a83paib571ahknipmgw7g9pbym105isk3bz0c1ng41s4kjpsxh"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.3.0"
+ #:bootstrap-idris idris2-0.2.2
+ #:historical? #true))
+
+(define-public idris2-0.4.0
+ ;; branch idris.6
+ (make-idris-package '("v0.4.0"
+ "105jybjf5s0k6003qzfxchzsfcpsxip180bh3mdmi74d464d0h8g")
+ "0.4.0"
+ #:bootstrap-idris idris2-0.3.0
+ #:ignore-test-failures? #true ; TODO investigate
+ #:historical? #true))
+
+(define-public idris2-0.5.1
+ (make-idris-package '("v0.5.1"
+ "09k5fxnplp6fv3877ynz1lwq9zapxcxbvfvkn6g68yb0ivrff978")
+ "0.5.1"))
+
+;; TODO re build failure: in the build sandbox some parts of the test output
+;; is missing. I cannot reproduce it in a guix shell. My assumption is that
+;; it's an Idris bug that only manifests in certain circumstances. There are
+;; some other issues left with the use of #!/bin/sh, too.
+(define-public idris2-dev
+ (make-idris-package '("4bb12225424d76c7874b176e2bfb8b5550c112eb"
+ "0kb800cgfm0afa83pbyi3x9bpswcl8jz4pr68zy092fs50km3bj7"
+ "https://github.com/attila-lendvai-patches/Idris2")
+ "0.5.1"
+ #:ignore-test-failures? #true
+ #:idris-version-tag "dev"))
+
+(define-public idris2 idris2-0.5.1)
+
+;;;
+;;; Idris apps
+;;;
+
;; 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.35.1
^ permalink raw reply related [flat|nested] 17+ messages in thread
* [bug#49607] [PATCH v3 3/3] gnu: idris: Add doc output and build the html documentation.
2022-04-28 13:28 ` [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
2022-04-28 13:28 ` [bug#49607] [PATCH v3 2/3] gnu: idris: Add idris2 0.5.1 Attila Lendvai
@ 2022-04-28 13:28 ` Attila Lendvai
2022-05-17 20:04 ` [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Eric Bavier
2 siblings, 0 replies; 17+ messages in thread
From: Attila Lendvai @ 2022-04-28 13:28 UTC (permalink / raw)
To: 49607; +Cc: Attila Lendvai
* gnu/packages/idris.scm (make-idris-package): Build the html docs and install
it into the doc output.
---
gnu/packages/idris.scm | 23 ++++++++++++++++++++---
1 file changed, 20 insertions(+), 3 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 1488996b6a..e03ca3bfbf 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -50,7 +50,9 @@ (define-module (gnu packages idris)
#:use-module (gnu packages ncurses)
#:use-module (gnu packages node)
#:use-module (gnu packages perl)
+ #:use-module (gnu packages python)
#:use-module (gnu packages racket)
+ #:use-module (gnu packages sphinx)
#:use-module (gnu packages version-control)
#:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
@@ -249,11 +251,17 @@ (define* (make-idris-package source idris-version
chez-scheme
bootstrap-idris)
coreutils which git
- node ; only for the tests
- racket ; only for the tests
- sed))
+ sed
+ ;; Only for the tests
+ node
+ racket
+ ;; Only for the docs
+ python-minimal
+ python-sphinx
+ python-sphinx-rtd-theme))
(inputs
(list bash-minimal chez-scheme gmp))
+ (outputs '("out" "doc"))
(arguments
(list
#:tests? tests?
@@ -276,6 +284,15 @@ (define* (make-idris-package source idris-version
(delete 'bootstrap)
(delete 'configure)
(delete 'check) ; check must happen after install and wrap-program
+ (add-before 'build 'build-doc
+ (lambda* (#:key outputs #:allow-other-keys)
+ (invoke "make" "--directory" "docs/" "html")))
+ (add-after 'build-doc 'install-doc
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((doc (assoc-ref outputs "doc")))
+ (copy-recursively "docs/build/html"
+ (string-append doc "/share/doc/"
+ ,name "-" ,version)))))
(add-after 'unpack 'patch-paths
(lambda* (#:key inputs #:allow-other-keys)
(let ((files-to-patch (filter file-exists?
--
2.35.1
^ permalink raw reply related [flat|nested] 17+ messages in thread
* [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC
2022-04-28 13:28 ` [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
2022-04-28 13:28 ` [bug#49607] [PATCH v3 2/3] gnu: idris: Add idris2 0.5.1 Attila Lendvai
2022-04-28 13:28 ` [bug#49607] [PATCH v3 3/3] gnu: idris: Add doc output and build the html documentation Attila Lendvai
@ 2022-05-17 20:04 ` Eric Bavier
2022-05-18 17:22 ` Attila Lendvai
2 siblings, 1 reply; 17+ messages in thread
From: Eric Bavier @ 2022-05-17 20:04 UTC (permalink / raw)
To: Attila Lendvai, 49607
[-- Attachment #1: Type: text/plain, Size: 846 bytes --]
Hi,
On Thu, 2022-04-28 at 15:28 +0200, Attila Lendvai wrote:
> Idris requires a C compiler at runtime to generate executables.
>
> * gnu/packages/idris.scm (idris) [inputs]: Add bash-minimal (for
> wrap-program).
> [phases]: Add wrap-program phase to define IDRIS_CC, use (cc-for-
> target).
> ---
I believe this would prevent someone from effectively setting
`IDRIS_CC` to a different compiler from within their environment,
correct? I would like to leave that option available to users. Also,
can this be a simple compiler reference, or does it need to be a
"toolchain compiler"? E.g. I usually set `IDRIS_CC` to gcc from a
"gcc-toolchain" package.
Could we possibly instead override the default C compiler in the
compiler's C backend? Either way we'd be embedding a reference to some
compiler/toolchain.
`~Eric
[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 858 bytes --]
^ permalink raw reply [flat|nested] 17+ messages in thread
* [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC
2022-05-17 20:04 ` [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Eric Bavier
@ 2022-05-18 17:22 ` Attila Lendvai
0 siblings, 0 replies; 17+ messages in thread
From: Attila Lendvai @ 2022-05-18 17:22 UTC (permalink / raw)
To: Eric Bavier; +Cc: 49607
> > * gnu/packages/idris.scm (idris) [inputs]: Add bash-minimal (for
> > wrap-program).
> > [phases]: Add wrap-program phase to define IDRIS_CC, use (cc-for-
> > target).
> > ---
>
>
> I believe this would prevent someone from effectively setting
> `IDRIS_CC` to a different compiler from within their environment,
> correct? I would like to leave that option available to users. Also,
good point! and i think you're correct, because wrapper scripts set the value unconditionally.
would it work if we set CC instead? idris first tries IDRIS_CC, and then CC (and then falls back to "cc").
or would you prefer to use substitute* in the build to replace cc = "cc" with a full path to gcc in the source code of idris?
> can this be a simple compiler reference, or does it need to be a
> "toolchain compiler"?
i'm unable to answer that, i don't know the difference.
i just noticed that i can't use idris as-is when trying the examples, because it couldn't invoke the c compiler to produce executables. this is my attempt at fixing this issue.
--
• attila lendvai
• PGP: 963F 5D5F 45C7 DFCD 0A39
--
If ethics are pure subjective preference, then rape is just competing preferences.
^ permalink raw reply [flat|nested] 17+ messages in thread
* [bug#49607] why not to propagate gcc as a dependency
2021-07-17 15:42 [bug#49607] [PATCH] gnu: Add Idris 2 Xinglu Chen
` (3 preceding siblings ...)
2022-04-28 13:28 ` [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
@ 2022-07-11 10:41 ` Attila Lendvai
2022-08-23 12:37 ` [bug#49607] Package proposition: Idris2 v0.5.1 contact
2022-12-08 0:42 ` [bug#49607] idris bootstrap, bailing out Attila Lendvai
6 siblings, 0 replies; 17+ messages in thread
From: Attila Lendvai @ 2022-07-11 10:41 UTC (permalink / raw)
To: 49607@debbugs.gnu.org
please note this discussion:
https://lists.gnu.org/archive/html/guix-devel/2022-07/msg00131.html
the conclusion, roughly: it's better if the user can pick whichever c compiler they want, but to retain a slick user experience, maybe we should introduce an idris-toolchain package that does the propagation.
- attila
^ permalink raw reply [flat|nested] 17+ messages in thread
* [bug#49607] Package proposition: Idris2 v0.5.1
2021-07-17 15:42 [bug#49607] [PATCH] gnu: Add Idris 2 Xinglu Chen
` (4 preceding siblings ...)
2022-07-11 10:41 ` [bug#49607] why not to propagate gcc as a dependency Attila Lendvai
@ 2022-08-23 12:37 ` contact
2022-12-08 0:42 ` [bug#49607] idris bootstrap, bailing out Attila Lendvai
6 siblings, 0 replies; 17+ messages in thread
From: contact @ 2022-08-23 12:37 UTC (permalink / raw)
To: 49607
[-- Attachment #1: Type: text/plain, Size: 170 bytes --]
Dear Guixers,
This package proposition follows from a discussion which last message
was:
https://lists.gnu.org/archive/html/help-guix/2022-08/msg00177.html
— PHF
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #2: 0001-gnu-Add-idris2-v0.5.1.patch --]
[-- Type: text/x-diff; name=0001-gnu-Add-idris2-v0.5.1.patch, Size: 10349 bytes --]
From 06d20e3e6ad2e08b0acd291cd4de3efeec76deb9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Henry=20Fr=C3=B6hring?= <contact@phfrohring.com>
Date: Tue, 23 Aug 2022 14:29:23 +0200
Subject: [PATCH] gnu: Add idris2 v0.5.1.
* gnu/packages/idris.scm (idris2): New variable.
---
gnu/packages/idris.scm | 180 +++++++++++++++++++++++++++++++++++++----
1 file changed, 163 insertions(+), 17 deletions(-)
diff --git a/gnu/packages/idris.scm b/gnu/packages/idris.scm
index 8f08ed3a3e..34511012ec 100644
--- a/gnu/packages/idris.scm
+++ b/gnu/packages/idris.scm
@@ -20,22 +20,36 @@
;;; You should have received a copy of the GNU General Public License
;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
-(define-module (gnu packages idris)
- #:use-module (gnu packages)
- #:use-module (gnu packages haskell-check)
- #:use-module (gnu packages haskell-web)
- #:use-module (gnu packages haskell-xyz)
- #:use-module (gnu packages libffi)
- #:use-module (gnu packages multiprecision)
- #:use-module (gnu packages ncurses)
- #:use-module (gnu packages perl)
- #:use-module (guix build-system gnu)
- #:use-module (guix build-system haskell)
- #:use-module (guix download)
- #:use-module (guix git-download)
- #:use-module (guix utils)
- #:use-module ((guix licenses) #:prefix license:)
- #:use-module (guix packages))
+(define-module (gnu packages idris))
+
+(use-modules
+ (gnu)
+ (guix gexp)
+ (guix utils)
+ (guix store)
+ (guix derivations)
+ (guix packages)
+ (guix download)
+ (guix git-download)
+ (guix build-system gnu)
+ (guix build-system haskell)
+ (guix build utils)
+ ((guix licenses) #:prefix license:))
+
+(use-package-modules
+ haskell-check
+ haskell-web
+ haskell-xyz
+ libffi
+ ncurses
+ perl
+ gcc
+ multiprecision
+ bash
+ base
+ linux
+ python
+ chez)
(define-public idris
(package
@@ -146,6 +160,138 @@ (define-public idris
Epigram and Agda.")
(license license:bsd-3)))
+(define-public idris2
+ (package
+ (name "idris2")
+ (version "0.5.1")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/idris-lang/Idris2")
+ (commit (string-append "v" version))))
+ (sha256
+ (base32
+ "09k5fxnplp6fv3877ynz1lwq9zapxcxbvfvkn6g68yb0ivrff978"))
+ (file-name (git-file-name name version))))
+ (build-system gnu-build-system)
+ (arguments
+ (list #:make-flags #~(list "SCHEME=chez-scheme"
+ (string-append "CC="
+ #$(cc-for-target))
+ (string-append "PREFIX="
+ #$output))
+ #:phases #~(modify-phases %standard-phases
+ (add-after 'set-paths 'patch-paths
+ (lambda* _
+ (define (add value var)
+ (let ((prev (getenv var)))
+ (if prev
+ (setenv var
+ (string-join (list prev value) ":"))
+ (setenv var value))))
+ (add (string-append #$output "/lib")
+ "LD_LIBRARY_PATH")
+ (add (string-append #$output "/bin") "PATH")))
+ (add-after 'unpack 'patch-shebangs
+ (lambda* (#:key inputs #:allow-other-keys)
+ (substitute* '("src/Compiler/Scheme/ChezSep.idr"
+ "src/Compiler/Scheme/Chez.idr"
+ "src/Compiler/Scheme/Racket.idr"
+ "bootstrap/idris2_app/idris2.rkt"
+ "bootstrap/idris2_app/idris2.ss")
+ (("(#!) *(/bin/sh)" _ shebang exec)
+ (string-append shebang " "
+ (assoc-ref inputs "bash-minimal")
+ exec)))))
+ (delete 'bootstrap)
+ (delete 'configure)
+ (add-before 'build 'bootstrap
+ (lambda* (#:key make-flags #:allow-other-keys)
+ (apply invoke "make" "bootstrap" make-flags)
+ (apply invoke "make" "install" make-flags)))
+ (replace 'build
+ (lambda* (#:key make-flags #:allow-other-keys)
+ (apply invoke "make" "clean" make-flags)
+ (apply invoke "make" "all" make-flags)))
+ (add-after 'install 'patch-/bin/idris2
+ (lambda* _
+ (let ((idris2 (string-append #$output "/bin/"
+ #$name))
+ (idris2_app (string-append #$output
+ "/bin/idris2_app")))
+ (delete-file idris2)
+ (rename-file (string-append idris2_app
+ "/idris2.so") idris2)
+ (delete-file-recursively idris2_app))))
+ (add-after 'patch-/bin/idris2 'wrap-idris2
+ (lambda* (#:key inputs #:allow-other-keys)
+ (let* ((chez (string-append (assoc-ref inputs
+ "chez-scheme")
+ "/bin/chez-scheme"))
+ (idris2-prefix #$output)
+ (idris2-version (string-append
+ idris2-prefix "/"
+ #$name "-"
+ #$version))
+ (idris2-lib (string-append idris2-version
+ "/lib"))
+ (idris2-support (string-append
+ idris2-version "/support"))
+ (idris2-bin (string-append idris2-prefix
+ "/bin/"
+ #$name)))
+ (wrap-program idris2-bin
+ (list "CHEZ"
+ '=
+ (list chez))
+ (list "IDRIS2_PREFIX"
+ '=
+ (list idris2-prefix))
+ (list "IDRIS2_LIBS"
+ 'suffix
+ (list idris2-lib))
+ (list "IDRIS2_DATA"
+ 'suffix
+ (list idris2-support))
+ (list "IDRIS2_PACKAGE_PATH"
+ 'suffix
+ (list idris2-version))
+ (list "LD_LIBRARY_PATH"
+ 'suffix
+ (list idris2-lib))
+ (list "DYLD_LIBRARY_PATH"
+ 'suffix
+ (list idris2-lib))))))
+ (add-before 'check 'set-INTERACTIVE-IDRIS2
+ (lambda* _
+ (setenv "INTERACTIVE" "")
+ (setenv "IDRIS2"
+ (string-append #$output "/bin/"
+ #$name))))
+ (add-after 'build 'build-doc
+ (lambda* (#:key make-flags #:allow-other-keys)
+ (apply invoke "make" "install-libdocs" make-flags))))
+ #:test-target "test"
+ #:parallel-build? #f))
+ (inputs (list gcc-12
+ chez-scheme
+ gmp
+ coreutils
+ bash-minimal
+ python))
+ (home-page "https://www.idris-lang.org/")
+ (synopsis
+ "Programming language designed to encourage Type-Driven Development")
+ (description
+ "Idris is a programming language designed to encourage Type-Driven Development.
+
+In type-driven development, types are tools for constructing programs. We
+treat the type as the plan for a program, and use the compiler and type
+checker as our assistant, guiding us to a complete program that satisfies the
+type. The more expressive the type is that we give up front, the more
+confidence we can have that the resulting program will be correct.")
+ (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)
@@ -178,7 +324,7 @@ (define (idris-default-arguments name)
(and path (match (stat:type (stat path))
('directory #t)
(_ #f))))
- idris-path-files))
+ idris-path-files))
(install-cmd (cons* idris-bin
"--ibcsubdir" ibcsubdir
"--build" ipkg
--
2.37.2
^ permalink raw reply related [flat|nested] 17+ messages in thread
* [bug#49607] idris bootstrap, bailing out
2021-07-17 15:42 [bug#49607] [PATCH] gnu: Add Idris 2 Xinglu Chen
` (5 preceding siblings ...)
2022-08-23 12:37 ` [bug#49607] Package proposition: Idris2 v0.5.1 contact
@ 2022-12-08 0:42 ` Attila Lendvai
6 siblings, 0 replies; 17+ messages in thread
From: Attila Lendvai @ 2022-12-08 0:42 UTC (permalink / raw)
To: 49607@debbugs.gnu.org
FTR, i have failed to inspire the idris maintainers with my refactor of the idris build system, and my setup that enables chain-bootstrapping the entire idris language evolution all the way down from GHC.
https://github.com/idris-lang/Idris2/pull/1990
i have also lost my initial interest in delving deep into idris, so i will not pursue my idris related work anymore.
i'm happy to help anyone who wants to pick up this work, though! i may even get involved if there's someone else who steps up to champion the cause.
--
• attila lendvai
• PGP: 963F 5D5F 45C7 DFCD 0A39
--
“Knowledge makes a man unfit to be a slave.”
— Frederick Douglass (1818–1895), a former slave.
^ permalink raw reply [flat|nested] 17+ messages in thread
end of thread, other threads:[~2022-12-08 0:43 UTC | newest]
Thread overview: 17+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2021-07-17 15:42 [bug#49607] [PATCH] gnu: Add Idris 2 Xinglu Chen
2021-10-05 16:37 ` [bug#49607] [PATCH 1/3] gnu: ghc-cheapskate: Update to 0.1.1.2 Attila Lendvai
2021-10-05 16:37 ` [bug#49607] [PATCH 2/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
2021-10-05 16:37 ` [bug#49607] [PATCH 3/3] gnu: idris: Add idris2 0.5.1, and 1.3.3-1.5545986 Attila Lendvai
2022-04-14 12:16 ` [bug#49607] [PATCH v2 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
2022-04-14 12:16 ` [bug#49607] [PATCH 2/3] gnu: idris: Add idris2 0.5.1, and update idris to 1.3.4 Attila Lendvai
2022-04-20 13:50 ` Eric Bavier
2022-04-14 12:16 ` [bug#49607] [PATCH 3/3] gnu: idris: Add doc output and build the html documentation Attila Lendvai
2022-04-14 15:53 ` [bug#49607] a note Attila Lendvai
2022-04-28 13:28 ` [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Attila Lendvai
2022-04-28 13:28 ` [bug#49607] [PATCH v3 2/3] gnu: idris: Add idris2 0.5.1 Attila Lendvai
2022-04-28 13:28 ` [bug#49607] [PATCH v3 3/3] gnu: idris: Add doc output and build the html documentation Attila Lendvai
2022-05-17 20:04 ` [bug#49607] [PATCH v3 1/3] gnu: idris: Use wrap-program to define IDRIS_CC Eric Bavier
2022-05-18 17:22 ` Attila Lendvai
2022-07-11 10:41 ` [bug#49607] why not to propagate gcc as a dependency Attila Lendvai
2022-08-23 12:37 ` [bug#49607] Package proposition: Idris2 v0.5.1 contact
2022-12-08 0:42 ` [bug#49607] idris bootstrap, bailing out Attila Lendvai
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).