From patchwork Tue Aug 23 12:37:16 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: =?utf-8?q?Pierre-Henry_Fr=C3=B6hring?= X-Patchwork-Id: 41877 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id B3F7A27BBEA; Tue, 23 Aug 2022 13:48:33 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-2.9 required=5.0 tests=BAYES_00,MAILING_LIST_MULTI, SPF_HELO_PASS,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 02E3C27BBE9 for ; Tue, 23 Aug 2022 13:48:33 +0100 (BST) Received: from localhost ([::1]:53354 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1oQTKa-0002Uy-1C for patchwork@mira.cbaines.net; Tue, 23 Aug 2022 08:48:32 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:45630) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1oQTAQ-0000Nx-Hy for guix-patches@gnu.org; Tue, 23 Aug 2022 08:38:02 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:53144) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1oQTAQ-00052L-9B for guix-patches@gnu.org; Tue, 23 Aug 2022 08:38:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1oQTAQ-0001T7-5R for guix-patches@gnu.org; Tue, 23 Aug 2022 08:38:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#49607] Package proposition: Idris2 v0.5.1 References: In-Reply-To: Resent-From: contact@phfrohring.com Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 23 Aug 2022 12:38:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 49607 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 49607@debbugs.gnu.org Received: via spool by 49607-submit@debbugs.gnu.org id=B49607.16612582465599 (code B ref 49607); Tue, 23 Aug 2022 12:38:02 +0000 Received: (at 49607) by debbugs.gnu.org; 23 Aug 2022 12:37:26 +0000 Received: from localhost ([127.0.0.1]:42893 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oQT9p-0001SF-Nd for submit@debbugs.gnu.org; Tue, 23 Aug 2022 08:37:26 -0400 Received: from relay8-d.mail.gandi.net ([217.70.183.201]:51789) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1oQT9n-0001S0-Np for 49607@debbugs.gnu.org; Tue, 23 Aug 2022 08:37:24 -0400 Received: (Authenticated sender: contact@phfrohring.com) by mail.gandi.net (Postfix) with ESMTPA id 332481BF205 for <49607@debbugs.gnu.org>; Tue, 23 Aug 2022 12:37:16 +0000 (UTC) MIME-Version: 1.0 Date: Tue, 23 Aug 2022 14:37:16 +0200 From: contact@phfrohring.com Message-ID: X-Sender: contact@phfrohring.com X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches 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 From 06d20e3e6ad2e08b0acd291cd4de3efeec76deb9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Henry=20Fr=C3=B6hring?= 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 . -(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