From patchwork Sun Apr 30 10:53:19 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 49703 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 A081A27BBE2; Sun, 30 Apr 2023 11:55:10 +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=-1.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, RCVD_IN_MSPIKE_H2,SPF_HELO_PASS,URIBL_BLOCKED autolearn=no 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 E3C3B27BBE9 for ; Sun, 30 Apr 2023 11:55:08 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1pt4h2-0002wj-6a; Sun, 30 Apr 2023 06:54:12 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1pt4gy-0002tZ-NZ for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from debbugs.gnu.org ([209.51.188.43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1pt4gv-0002UO-MX for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:08 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1pt4gv-0000WK-HH for guix-patches@gnu.org; Sun, 30 Apr 2023 06:54:05 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#61915] [PATCH v2 09/13] build-system: New agda-build-system. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 30 Apr 2023 10:54:05 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 61915 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Josselin Poiret , Simon Tournier , 61915@debbugs.gnu.org Received: via spool by 61915-submit@debbugs.gnu.org id=B61915.16828520381896 (code B ref 61915); Sun, 30 Apr 2023 10:54:05 +0000 Received: (at 61915) by debbugs.gnu.org; 30 Apr 2023 10:53:58 +0000 Received: from localhost ([127.0.0.1]:37356 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gn-0000UO-Ds for submit@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:58 -0400 Received: from jpoiret.xyz ([206.189.101.64]:53322) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1pt4gS-0000SQ-Sm for 61915@debbugs.gnu.org; Sun, 30 Apr 2023 06:53:38 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id 57DE7185328; Sun, 30 Apr 2023 10:53:36 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1682852016; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=pPL/DSCQF+3W4K+1Gvyk7r296y2+46/+M+J37j5HEv4=; b=TuzlN2YNQ3pUH3P9/FboktAGFcuqf4wr+oH075I4bns4L2uHUhMhp79M3Udax1oR7RM0vS GqCGtKaJqLmTB6VtXHZw74siI20qh1iDHZeLPyjWur/4C821HJT6m6B1g2ZzqAV1HwXT+y 0QunaB1zZMGjBU6JswF7fJVjmjG03sa+00OVS/v58XAWRQTVpz36n3G7OI5KwD3suLqyp7 T3beP5uIsgB+XMnBcNE2aDY3JmTGkbrF9jKODG9LSPjVoJDrnBm30WyCCDBdSt5Z3ceBi/ N9AnAuAX0ZX0JgpG2HizJH8f06dQTZJHLX58i/F9HMaci7rEzjrXxZdWyEC5OQ== Date: Sun, 30 Apr 2023 12:53:19 +0200 Message-Id: In-Reply-To: References: MIME-Version: 1.0 X-Spamd-Bar: / Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz 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: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret * guix/build-system/agda.scm: New file. * guix/build/agda-build-system.scm: New file. * Makefile.am (MODULES): Register them. * doc/guix.texi (Build Systems): Add documentation for agda-build-system. --- Makefile.am | 2 + doc/guix.texi | 21 ++++++ guix/build-system/agda.scm | 105 +++++++++++++++++++++++++++++ guix/build/agda-build-system.scm | 110 +++++++++++++++++++++++++++++++ 4 files changed, 238 insertions(+) create mode 100644 guix/build-system/agda.scm create mode 100644 guix/build/agda-build-system.scm diff --git a/Makefile.am b/Makefile.am index a763a7e305..9d137cfbb3 100644 --- a/Makefile.am +++ b/Makefile.am @@ -140,6 +140,7 @@ MODULES = \ guix/platforms/riscv.scm \ guix/platforms/x86.scm \ guix/build-system.scm \ + guix/build-system/agda.scm \ guix/build-system/android-ndk.scm \ guix/build-system/ant.scm \ guix/build-system/cargo.scm \ @@ -195,6 +196,7 @@ MODULES = \ guix/diagnostics.scm \ guix/ui.scm \ guix/status.scm \ + guix/build/agda-build-system.scm \ guix/build/android-ndk-build-system.scm \ guix/build/ant-build-system.scm \ guix/build/download.scm \ diff --git a/doc/guix.texi b/doc/guix.texi index 46e7fd3908..01cd199f0a 100644 --- a/doc/guix.texi +++ b/doc/guix.texi @@ -8885,6 +8885,27 @@ of @code{gnu-build-system}, and differ mainly in the set of inputs implicitly added to the build process, and in the list of phases executed. Some of these build systems are listed below. +@defvar agda-build-system +This variable is exported by @code{(guix build-system agda)}. It +implements a build procedure for Agda libraries. + +It adds @code{agda} to the set of inputs. A different Agda can be +specified with the @code{#:agda} key. + +The @code{#:plan} key is a list of cons cells @code{(@var{regexp} +. @var{parameters})}, where @var{regexp} is a regexp that should match +the @code{.agda} files to build, and @var{parameters} is an optional +list of parameters that will be passed to @code{agda} when type-checking +it. + +When the library uses Haskell to generate a file containing all imports, +the convenience @code{#:gnu-and-haskell?} can be set to @code{#t} to add +@code{ghc} and the standard inputs of @code{gnu-build-system} to the +input list. You will still need to manually add a phase or tweak the +@code{'build} phase, as in the definition of @code{agda-stdlib}. + +@end defvar + @defvar ant-build-system This variable is exported by @code{(guix build-system ant)}. It implements the build procedure for Java packages that can be built with diff --git a/guix/build-system/agda.scm b/guix/build-system/agda.scm new file mode 100644 index 0000000000..cf96ffaa68 --- /dev/null +++ b/guix/build-system/agda.scm @@ -0,0 +1,105 @@ +(define-module (guix build-system agda) + #:use-module (guix build-system) + #:use-module (guix build-system gnu) + #:use-module (guix build-system haskell) + #:use-module (guix gexp) + #:use-module (guix monads) + #:use-module (guix packages) + #:use-module (guix search-paths) + #:use-module (guix store) + #:use-module (guix utils) + #:export (default-agda + + %agda-build-system-modules + agda-build-system)) + +(define (default-agda) + ;; Lazily resolve the binding to avoid a circular dependency. + (let ((agda (resolve-interface '(gnu packages agda)))) + (module-ref agda 'agda))) + +(define %agda-build-system-modules + `((guix build agda-build-system) + ,@%gnu-build-system-modules)) + +(define %default-modules + '((guix build agda-build-system) + (guix build utils))) + +(define* (lower name + #:key source inputs native-inputs outputs system target + (agda (default-agda)) + gnu-and-haskell? + #:allow-other-keys + #:rest arguments) + "Return a bag for NAME." + (define private-keywords + '(#:target #:agda #:gnu-and-haskell? #:inputs #:native-inputs)) + + ;; TODO: cross-compilation support + (and (not target) + (bag + (name name) + (system system) + (host-inputs `(,@(if source + `(("source" ,source)) + '()) + ,@inputs)) + (build-inputs `(("agda" ,agda) + ,@(if gnu-and-haskell? + (cons* + (list "ghc" (default-haskell)) + (standard-packages)) + '()) + ,(assoc "locales" (standard-packages)) + ,@native-inputs)) + (outputs outputs) + (build agda-build) + (arguments (strip-keyword-arguments private-keywords arguments))))) + +(define* (agda-build name inputs + #:key + source + (phases '%standard-phases) + (outputs '("out")) + (search-paths '()) + (unpack-path "") + (build-flags ''()) + (tests? #t) + (system (%current-system)) + (guile #f) + plan + (extra-files '("^\\./.*\\.agda-lib$")) + (imported-modules %agda-build-system-modules) + (modules %default-modules)) + (define builder + (with-imported-modules imported-modules + #~(begin + (use-modules #$@(sexp->gexp modules)) + (agda-build #:name #$name + #:source #+source + #:system #$system + #:phases #$phases + #:outputs #$(outputs->gexp outputs) + #:search-paths '#$(sexp->gexp + (map search-path-specification->sexp + search-paths)) + #:unpack-path #$unpack-path + #:build-flags #$build-flags + #:tests? #$tests? + #:inputs #$(input-tuples->gexp inputs) + #:plan '#$plan + #:extra-files '#$extra-files)))) + + (mlet %store-monad ((guile (package->derivation (or guile (default-guile)) + system #:graft? #f))) + (gexp->derivation name builder + #:system system + #:guile-for-build guile))) + +(define agda-build-system + (build-system + (name 'agda) + (description + "Build system for Agda libraries") + (lower lower))) diff --git a/guix/build/agda-build-system.scm b/guix/build/agda-build-system.scm new file mode 100644 index 0000000000..1d7e80d61b --- /dev/null +++ b/guix/build/agda-build-system.scm @@ -0,0 +1,110 @@ +(define-module (guix build agda-build-system) + #:use-module ((guix build gnu-build-system) #:prefix gnu:) + #:use-module (guix build utils) + #:use-module (srfi srfi-26) + #:use-module (srfi srfi-34) + #:use-module (srfi srfi-35) + #:use-module (ice-9 ftw) + #:use-module (ice-9 match) + #:export (%standard-phases + agda-build)) + +(define* (set-locpath #:key inputs native-inputs #:allow-other-keys) + (let ((locales (assoc-ref (or native-inputs inputs) "locales"))) + (setenv "GUIX_LOCPATH" (string-append locales "/lib/locale")))) + +(define %agda-possible-extensions + (cons + ".agda" + (map (cute string-append ".lagda" <>) + '("" + ".md" + ".org" + ".rst" + ".tex")))) + +(define (pattern-predicate pattern) + (define compiled-rx (make-regexp pattern)) + (lambda (file stat) + (regexp-exec compiled-rx file))) + +(define* (build #:key plan #:allow-other-keys) + (for-each + (match-lambda + ((pattern . options) + (for-each + (lambda (file) + (apply invoke (cons* "agda" file options))) + (let ((files (find-files "." (pattern-predicate pattern)))) + (if (null? files) + (raise + (make-compound-condition + (condition + (&message + (message (format #f "Plan pattern `~a' did not match any files" + pattern)))) + (condition + (&error)))) + files)))) + (x + (raise + (make-compound-condition + (condition + (&message + (message (format #f "Malformed plan element `~a'" x)))) + (condition + (&error)))))) + plan)) + +(define* (install #:key outputs name extra-files #:allow-other-keys) + (define libdir (string-append (assoc-ref outputs "out") "/lib/agda/" name)) + (define agda-version + (car (scandir "./_build/" + (lambda (entry) + (not (member entry '("." ".."))))))) + (define agdai-files + (with-directory-excursion + (string-join (list "." "_build" agda-version "agda") "/") + (find-files "."))) + (define (install-source agdai) + (define dir (dirname agdai)) + ;; Drop .agdai + (define no-ext (string-drop-right agdai 6)) + (define source + (match (filter file-exists? (map (cute string-append no-ext <>) + %agda-possible-extensions)) + ((single) single) + (res (raise + (make-compound-condition + (condition + (&message + (message + (format #f + "Cannot find unique source file for agdai file `~a`, got `~a`" + agdai res)))) + (condition + (&error))))))) + (install-file source (string-append libdir "/" dir))) + (for-each install-source agdai-files) + (copy-recursively "_build" (string-append libdir "/_build")) + (for-each + (lambda (pattern) + (for-each + (lambda (file) + (install-file file libdir)) + (find-files "." (pattern-predicate pattern)))) + extra-files)) + +(define %standard-phases + (modify-phases gnu:%standard-phases + (add-before 'install-locale 'set-locpath set-locpath) + (delete 'bootstrap) + (delete 'configure) + (replace 'build build) + (delete 'check) ;; No universal checker + (replace 'install install))) + +(define* (agda-build #:key inputs (phases %standard-phases) + #:allow-other-keys #:rest args) + "Build the given Agda package, applying all of PHASES in order." + (apply gnu:gnu-build #:inputs inputs #:phases phases args))