From unknown Sat Sep 06 14:23:55 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode. Resent-From: Alex ter Weele Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 21 Jul 2018 16:01:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 32235 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 32235@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.15321888082039 (code B ref -1); Sat, 21 Jul 2018 16:01:01 +0000 Received: (at submit) by debbugs.gnu.org; 21 Jul 2018 16:00:08 +0000 Received: from localhost ([127.0.0.1]:51228 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fguIh-0000Wp-NP for submit@debbugs.gnu.org; Sat, 21 Jul 2018 12:00:07 -0400 Received: from eggs.gnu.org ([208.118.235.92]:38950) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fguId-0000Uq-Oa for submit@debbugs.gnu.org; Sat, 21 Jul 2018 12:00:03 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1fguIX-0007XZ-Ss for submit@debbugs.gnu.org; Sat, 21 Jul 2018 11:59:58 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM, T_DKIM_INVALID autolearn=disabled version=3.3.2 Received: from lists.gnu.org ([2001:4830:134:3::11]:40268) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1fguIX-0007XO-PC for submit@debbugs.gnu.org; Sat, 21 Jul 2018 11:59:57 -0400 Received: from eggs.gnu.org ([2001:4830:134:3::10]:58149) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1fguIW-0004zK-Pq for guix-patches@gnu.org; Sat, 21 Jul 2018 11:59:57 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1fguIT-0007VJ-OH for guix-patches@gnu.org; Sat, 21 Jul 2018 11:59:56 -0400 Received: from mail-it0-x22c.google.com ([2607:f8b0:4001:c0b::22c]:37111) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1fguIT-0007V9-Iz for guix-patches@gnu.org; Sat, 21 Jul 2018 11:59:53 -0400 Received: by mail-it0-x22c.google.com with SMTP id p17-v6so18367329itc.2 for ; Sat, 21 Jul 2018 08:59:53 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:subject:date:message-id:user-agent:mime-version; bh=47DEQpj8HBSa+/TImW+5JCeuQeRkm5NMpJWZG3hSuFU=; b=HcPk91rfZwmPQ/zlqBrda8lDffXIN4k3Q4hInAnBp7s5HZVwPecbA6pZRP3s/SD9mK YOPMwGnEuYsXWeVHZyKrX3L0ylYiroorvy8LUjcMzWLezL2C50deya8bdIjZ097OiCVl 9fXeYKCpxW3vCfem52FCWQfEDIbDJkA8c95jpUzmq+KCWo4V2zqFSqUIOvh6Gxr9R092 0/0P55kwxy717bp+zMR45z+3QaGyZvieP0x46YUwC1MbK+nsKh0WN3IO+++SLb1phpgw r7Ho1GOKYcYAf96bcfZWBoaxenW2VYUFl1IQoOw472ScgDGbCQBn9m6Lle99JUB4iAJj szxQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:subject:date:message-id:user-agent :mime-version; bh=47DEQpj8HBSa+/TImW+5JCeuQeRkm5NMpJWZG3hSuFU=; b=L1gNX52AjIv9AKlh1mXV/cP0g75ChpvslO6UXk2qoengs08lOR1JiLq1BfJCo+FUCw 8uNVOgUFzxOBdZcmTyFXfew3UaOtse2pwc6KSxn3bmFRo/EAF1jS72Is3/qhXA0jKImX 5ogiWk/F7AcuyJsfp31FlVRtF+rAW/9iivW4WUwYtQpsB/TGVv+wE1VxgOAzROs9vKvs YO24dJUNP00SQ+ElVuDNgOVOZfMdSA6LOS/4XiCw1bBblZPHMdFwG85jBAffD+39Ogur IfQPsfgI+B6MfVqVSM19ZZCz44FFpAHaS3rAgIA09wDsQ1A9tJISuOzIa7peifDZyLco x2rA== X-Gm-Message-State: AOUpUlG2oxlhlnMuNB6VB35B8lwz/g/Biqp87SJiiCHWFNHrzMvEchYZ TFwnBXw42PHZMA6Rk/fvwRow50DC X-Google-Smtp-Source: AAOMgpdIbfmh4iMJYe71LANpAI7nOouPl+dp6XtMj5ynu7GfKFZm6mt78VIWsXojomzlEtTmjEdS8A== X-Received: by 2002:a24:2581:: with SMTP id g123-v6mr5044562itg.59.1532188792248; Sat, 21 Jul 2018 08:59:52 -0700 (PDT) Received: from librem (24-148-50-16.s5644.c3-0.mart-ubr1.chi-mart.il.cable.rcncustomer.com. [24.148.50.16]) by smtp.gmail.com with ESMTPSA id k8-v6sm2639381itk.14.2018.07.21.08.59.51 for (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Sat, 21 Jul 2018 08:59:51 -0700 (PDT) From: Alex ter Weele X-Google-Original-From: Alex ter Weele Date: Sat, 21 Jul 2018 10:59:50 -0500 Message-ID: <876018pojt.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Received-From: 2001:4830:134:3::11 X-Spam-Score: -4.0 (----) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -5.0 (-----) From unknown Sat Sep 06 14:23:55 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode. Resent-From: Alex ter Weele Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 21 Jul 2018 16:15:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 32235 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 32235@debbugs.gnu.org Received: via spool by 32235-submit@debbugs.gnu.org id=B32235.15321896413291 (code B ref 32235); Sat, 21 Jul 2018 16:15:01 +0000 Received: (at 32235) by debbugs.gnu.org; 21 Jul 2018 16:14:01 +0000 Received: from localhost ([127.0.0.1]:51239 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fguW9-0000qw-CX for submit@debbugs.gnu.org; Sat, 21 Jul 2018 12:14:01 -0400 Received: from mail-qk0-f194.google.com ([209.85.220.194]:38553) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fguW8-0000qa-1C for 32235@debbugs.gnu.org; Sat, 21 Jul 2018 12:14:00 -0400 Received: by mail-qk0-f194.google.com with SMTP id 126-v6so6290490qke.5 for <32235@debbugs.gnu.org>; Sat, 21 Jul 2018 09:14:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:subject:references:date:in-reply-to:message-id:user-agent :mime-version; bh=ZNM56nRO6mbZ1EIpUtkOnbwC3Dqo9y452ubjNRI8Aqk=; b=C+aX5aBtKbyNSmMEBv+DY9pbXE3OhFVDa1ROHZ1YEPFCYRwEVPGB0Unm2xcQVnvNE3 gBHssqN9wntvMtaPZNC8Xks3tBCQfBAfihMiFp/1hiD7KZQauPr+PrAK3AhsOW/j+5wT jMcVUA9wumo1wjumIG3biDl8ZRurf6wnUls/HRzJ0wW/4K+81GgMcHD83IaYdTGpwmDU +qTYHm620jGiQC2o+fAPCYvhWVlY3nqYZfvo0Pd1HwE/WU3maE9eI/IqB7GVZDQ6btV5 84GHsUcwqMNM+LfYYLyvgngkGnMa87tfu1KFqOidqjHL5ltCeJAwNhhmeeNzS92nRzWf tZhQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:subject:references:date:in-reply-to :message-id:user-agent:mime-version; bh=ZNM56nRO6mbZ1EIpUtkOnbwC3Dqo9y452ubjNRI8Aqk=; b=jEIL60rFVCIaIPxADdTr2ogruS4yzCcq6TxQbXLIYDg0ISlBbYlYze3XZ1XsfQZVVG d1A3iuLrRohEKdk/aL5yNNw4gE4Kj9T62d4M2cG87HWkMAWahYH+RHClgfStmwePXpHM ekqK8HPJIwDZG1f6ZpgKLYfdSJW8DTRFVnPHM6R7kVc5v7zp5Jy2XoTJCYu1P58HMVil 6tVJsYsZ12OUGXSwRuBDqzLL3CrdPalQAQ2qSDD4DyTNVqgrjks/jshB0tU7NmdWLq4u QrzShP6w5DGq1VQicluoxDixKZcNcSFfl6pmJajzuK2vFaYCXcsptN6l/DIBLCtPEvnL CzZw== X-Gm-Message-State: AOUpUlG5wxMyPbB/QHdjUsnMljpVbjJduBvVq52yq9Sl7HCjcleqeA5J Yia2+XSCRvYFHnNx64F+BUJUhHkq X-Google-Smtp-Source: AAOMgpfeeRt3LbTOciLXWuFBcHnmpsUnLI2wDkrV/nTgoBbG9daIkvba+kJ340Stch8L2xZkPNyvjg== X-Received: by 2002:a37:f50f:: with SMTP id l15-v6mr5782714qkk.251.1532189634311; Sat, 21 Jul 2018 09:13:54 -0700 (PDT) Received: from librem (24-148-50-16.s5644.c3-0.mart-ubr1.chi-mart.il.cable.rcncustomer.com. [24.148.50.16]) by smtp.gmail.com with ESMTPSA id p5-v6sm3020602qkd.81.2018.07.21.09.13.52 for <32235@debbugs.gnu.org> (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Sat, 21 Jul 2018 09:13:53 -0700 (PDT) From: Alex ter Weele X-Google-Original-From: Alex ter Weele References: <876018pojt.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> Date: Sat, 21 Jul 2018 11:13:52 -0500 In-Reply-To: (GNU bug Tracking System's message of "Sat, 21 Jul 2018 16:01:02 +0000") Message-ID: <87va98o9bz.fsf_-_@librem.i-did-not-set--mail-host-address--so-tickle-me> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="=-=-=" X-Spam-Score: -0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) --=-=-= Content-Type: text/x-patch Content-Disposition: attachment; filename=0001-gnu-agda-Compile-.agda-files.patch >From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001 From: Alex ter Weele Date: Fri, 20 Jul 2018 21:35:14 -0500 Subject: [PATCH 1/2] gnu: agda: Compile .agda files. * gnu/packages/agda.scm: (agda)[arguments]: Compile .agda files. --- gnu/packages/agda.scm | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 6aa230116..f7474aae3 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -67,6 +67,29 @@ ("ghc-text" ,ghc-text) ("ghc-unordered-containers" ,ghc-unordered-containers) ("ghc-zlib" ,ghc-zlib))) + (arguments + `(#:modules ((guix build haskell-build-system) + (guix build utils) + (srfi srfi-26)) + #:phases + (modify-phases %standard-phases + (add-after 'compile 'agda-compile + (lambda* (#:key outputs #:allow-other-keys) + (let* ((out (assoc-ref outputs "out")) + (agda-compiler (string-append out "/bin/agda")) + (agda-files-path (string-append + out + "/share/x86_64-linux-ghc-8.0.2/Agda-" + ,version + "/lib/prim/Agda/")) + (agda-files (append + (find-files agda-files-path "\\.agda$") + (find-files (string-append + agda-files-path + "Builtin") + "\\.agda$")))) + (for-each (cut invoke agda-compiler <>) agda-files) + #t)))))) (home-page "http://wiki.portal.chalmers.se/agda/") (synopsis "Dependently typed functional programming language and proof assistant") -- 2.18.0 --=-=-= Content-Type: text/x-patch Content-Disposition: attachment; filename=0002-gnu-Add-emacs-agda2-mode.patch >From ff441cb0b500d247de9a54c3212f80b4fcfaf04f Mon Sep 17 00:00:00 2001 From: Alex ter Weele Date: Sat, 21 Jul 2018 10:57:35 -0500 Subject: [PATCH 2/2] gnu: Add emacs-agda2-mode * gnu/packages/agda.scm (emacs-agda2-mode): New variable. --- gnu/packages/agda.scm | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index f7474aae3..1a2078c07 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -20,6 +20,7 @@ #:use-module (gnu packages haskell) #:use-module (gnu packages haskell-check) #:use-module (gnu packages haskell-web) + #:use-module (guix build-system emacs) #:use-module (guix build-system haskell) #:use-module (guix build-system trivial) #:use-module (guix download) @@ -107,3 +108,18 @@ such as Coq, Epigram and NuPRL.") ;; Agda is distributed under the MIT license, and a couple of ;; source files are BSD-3. See LICENSE for details. (license (list license:expat license:bsd-3)))) + +(define-public emacs-agda2-mode + (package + (inherit agda) + (name "agda2-mode") + (build-system emacs-build-system) + (arguments + `(#:phases + (modify-phases %standard-phases + (add-after 'unpack 'enter-elisp-dir + (lambda _ (chdir "src/data/emacs-mode")))))) + (home-page "https://agda.readthdocs.io/en/latest/tools/emacs-mode.html") + (synopsis "Emacs mode for Agda") + (description "This Emacs mode enables interactive development with +Agda. It also aids the input of Unicode characters."))) -- 2.18.0 --=-=-=-- From unknown Sat Sep 06 14:23:55 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode. Resent-From: Marius Bakke Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 22 Jul 2018 14:41:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 32235 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Alex ter Weele , 32235@debbugs.gnu.org Received: via spool by 32235-submit@debbugs.gnu.org id=B32235.15322704244110 (code B ref 32235); Sun, 22 Jul 2018 14:41:02 +0000 Received: (at 32235) by debbugs.gnu.org; 22 Jul 2018 14:40:24 +0000 Received: from localhost ([127.0.0.1]:52510 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fhFX6-00014D-Iu for submit@debbugs.gnu.org; Sun, 22 Jul 2018 10:40:24 -0400 Received: from out1-smtp.messagingengine.com ([66.111.4.25]:45881) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fhFX4-000146-Tb for 32235@debbugs.gnu.org; Sun, 22 Jul 2018 10:40:23 -0400 Received: from compute5.internal (compute5.nyi.internal [10.202.2.45]) by mailout.nyi.internal (Postfix) with ESMTP id 8831B20F50; Sun, 22 Jul 2018 10:40:22 -0400 (EDT) Received: from mailfrontend2 ([10.202.2.163]) by compute5.internal (MEProxy); Sun, 22 Jul 2018 10:40:22 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=fastmail.com; h= content-type:date:from:in-reply-to:message-id:mime-version :references:subject:to:x-me-sender:x-me-sender:x-sasl-enc; s= fm3; bh=VdHlQWltvixCZwm4zNBTBgV7JAHvA143rCptOW/HR3Y=; b=aNlGUOah OaRAs0Th9FbCXZXbqaMuORy8ozarmxXA5oBBqnTNT9eM5EjCttGRNoHj0ZvS6WYI UnRhfLfqtxyT+GrtJSLx6pBQi33Azt6IAl/5xs00D6JsStiIUP1w0s07SB07kCy9 GMKxELlqAQ8tVGVLNoHH8ljjRKcJdk3Vm7Gzk1xHfKWNvJNfUlIkbobIUQd/2wlS SqNKFund5DnD+mHohn/y7INQ0wSHr3/8aQJQgnw8dCo4f+kxVv8noTV/nyvqmIIb a3HFdLP3/r25lj602Tp0cZSFzf3IrNKbKK9YYzjKhYSrnsH43nNyqPZUDKph4YFN dX+5o6cPXw42xQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=content-type:date:from:in-reply-to :message-id:mime-version:references:subject:to:x-me-sender :x-me-sender:x-sasl-enc; s=fm3; bh=VdHlQWltvixCZwm4zNBTBgV7JAHvA 143rCptOW/HR3Y=; b=vQamcH8W0lntcpGwKKV2N80FSNRjehdAqTEBpC6HtDQ0n gl3KR982eVjo6jxuePNXyaIRQQGPQA/MDdjBu9P1E6iBf4cCHo8Cf4v575Fz0Cvz 2R3A9lqBuj4IguOMV0T6s7UHRh47McLGjHV7KmxciFMNVWVmprlGGEf2LWplY5tK ysPnCG0+WBaizv9ymnSgH5GiRFZhnaDPnGYGmtDU4bJuTaVW2S4fAmPDqtoCOXyf aYScxE3WoMWyl5iFIGyLStOjS2ViSJx1lvWUgFCKt4uQ7C6y8oxJTdqivQLSL8lc n3UPtx55TvC4FYIQ4ooR2o1pDWrpv6UoWcPlkyQAQ== X-ME-Proxy: X-ME-Sender: Received: from localhost (95.92-221-151.customer.lyse.net [92.221.151.95]) by mail.messagingengine.com (Postfix) with ESMTPA id D87F01025D; Sun, 22 Jul 2018 10:40:21 -0400 (EDT) From: Marius Bakke In-Reply-To: <87va98o9bz.fsf_-_@librem.i-did-not-set--mail-host-address--so-tickle-me> References: <876018pojt.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> <87va98o9bz.fsf_-_@librem.i-did-not-set--mail-host-address--so-tickle-me> User-Agent: Notmuch/0.27 (https://notmuchmail.org) Emacs/26.1 (x86_64-pc-linux-gnu) Date: Sun, 22 Jul 2018 16:40:20 +0200 Message-ID: <87a7qj5o6j.fsf@fastmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" X-Spam-Score: -0.7 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.7 (-) --=-=-= Content-Type: text/plain Alex ter Weele writes: > From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001 > From: Alex ter Weele > Date: Fri, 20 Jul 2018 21:35:14 -0500 > Subject: [PATCH 1/2] gnu: agda: Compile .agda files. > > * gnu/packages/agda.scm: (agda)[arguments]: Compile .agda files. [...] > + (arguments > + `(#:modules ((guix build haskell-build-system) > + (guix build utils) > + (srfi srfi-26)) > + #:phases > + (modify-phases %standard-phases > + (add-after 'compile 'agda-compile > + (lambda* (#:key outputs #:allow-other-keys) > + (let* ((out (assoc-ref outputs "out")) > + (agda-compiler (string-append out "/bin/agda")) > + (agda-files-path (string-append > + out > + "/share/x86_64-linux-ghc-8.0.2/Agda-" This is unfortunate, since it hard-codes both architecture and GHC version. Can you think of another method to find these files? Are there ".agda" files elsewhere under "/share"? Could the find-files invokation below simply search "out/share", for example? Worst case scenario we'll have to dynamically generate that GHC path based on architecture and version, but hoping there's another way. > + ,version > + "/lib/prim/Agda/")) > + (agda-files (append > + (find-files agda-files-path "\\.agda$") > + (find-files (string-append > + agda-files-path > + "Builtin") > + "\\.agda$")))) (find-files ...) recurses through subdirectories, are you sure adding an extra pass for "Builtin/*.agda" makes a difference here? > + (for-each (cut invoke agda-compiler <>) agda-files) > + #t)))))) > (home-page "http://wiki.portal.chalmers.se/agda/") Otherwise LGTM. [...] > From ff441cb0b500d247de9a54c3212f80b4fcfaf04f Mon Sep 17 00:00:00 2001 > From: Alex ter Weele > Date: Sat, 21 Jul 2018 10:57:35 -0500 > Subject: [PATCH 2/2] gnu: Add emacs-agda2-mode > > * gnu/packages/agda.scm (emacs-agda2-mode): New variable. LGTM! --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQEzBAEBCgAdFiEEu7At3yzq9qgNHeZDoqBt8qM6VPoFAltUl1QACgkQoqBt8qM6 VPqKZgf+P0xxg4CypdzrgeEWaffg3IC5M8H96uKxVAbFi/tNCSmEK6I2Ay0ceC7g ParMhCCDwVlZtrfpEP1TqnOVZ1ZIC/dmc8dn2Qq33lhTUfSDXqAmOlXcmH5F1jeV MNMa+4FSPXSrVt4wX8rNIlHd1w37puNe4AsPCFX7wJtcY956kacsym4d/XseOoKm Q+Y1DhcmsqY36qeBPeYwMgw+YhFrhErwHdAk9VftSyLrpxcUXZ7mZRfPG5OWrBld tD5SNIRwrx+TMPOm0RDECFtJVqZfkdDDElrJyde0hMWajvqyCuVupgAhi4j6XVsg 7YxVmCTLjlQpjB5+3I7D+uIOokjXKw== =uRW1 -----END PGP SIGNATURE----- --=-=-=-- From unknown Sat Sep 06 14:23:55 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode. Resent-From: Alex ter Weele Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 28 Jul 2018 02:40:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 32235 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Marius Bakke Cc: Alex ter Weele , 32235@debbugs.gnu.org Received: via spool by 32235-submit@debbugs.gnu.org id=B32235.153274558329039 (code B ref 32235); Sat, 28 Jul 2018 02:40:02 +0000 Received: (at 32235) by debbugs.gnu.org; 28 Jul 2018 02:39:43 +0000 Received: from localhost ([127.0.0.1]:60674 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fjF8w-0007YJ-B7 for submit@debbugs.gnu.org; Fri, 27 Jul 2018 22:39:42 -0400 Received: from mail-it0-f51.google.com ([209.85.214.51]:39022) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fjF8u-0007Y4-Q9 for 32235@debbugs.gnu.org; Fri, 27 Jul 2018 22:39:41 -0400 Received: by mail-it0-f51.google.com with SMTP id g141-v6so9948150ita.4 for <32235@debbugs.gnu.org>; Fri, 27 Jul 2018 19:39:40 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:cc:subject:references:date:in-reply-to:message-id :user-agent:mime-version; bh=GdHx3wh9bMtK0XO/W6YvE/QLCwgoXDmiWBLEb6egEI4=; b=U2ok2vgk6jWoRl3Bf6bIeVil7oaVqCYilGK5AcYdpEG4N3bFZL7sreogZz34u/+iC8 1drKQW4Oz/iYSP7DF5aOMoTUkF3us7wK6odDY9LdQTMFtS1cPhqca3KJAbG+Ug9o2Bjt 2R/rWrDy3Cw95DeLp9CNMXMe1DqtVq3q5y3d7N7PAYLEjYxhMc+VhSpTe/SO7MTTVWR1 Ela6ewI7cHpEp0vAzNZcT4Ezqcs1EO7B/es7CidGy5fFQhPyCdUvBKW1tDBuqQS0+NhA CCJsfix35/vMgJVUU2V4bKacAhh1+LQPEGieV+alyQj3AblI8RQ6FEUxuedJQw8I7gXT 7yVQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to :message-id:user-agent:mime-version; bh=GdHx3wh9bMtK0XO/W6YvE/QLCwgoXDmiWBLEb6egEI4=; b=cEOMAdpE8tTmclmpOyJzE1JkCftwmM+IBVoHqYcjJU3ztmooMRhdQ7wt/YmpE74rsn JunGlavYNTdq2Zo2LZLedZuWaNqpiPkUqyD1afHrtTBIkSSQu7eCiXdpFXhY2OzGciDr tO+r3oEbMTUzV1QuZ2rXWL79+8EE1XNHnePX1C9roVrl7Y/Udr5/3tej5LvAhGk/j+/a I+4zfuPbAAgNdhVpdtbdWJqUiFNu1Opz4jLOJmqAVO6S66LvY1bNtjcJbjsVDXPbkutI yZoQnwSz4gtR1uGxNXbpwb1HMUVqUfashpr2ZZUfGACWwJ1bFk8fkNCitAtxmncieCeR i28w== X-Gm-Message-State: AOUpUlGi4/k+bp6A4tMws4ZaRv3EPyOqnBoFm61Qy1uGXYSEGAGG95Mq ut91cfzK9WNLPzepyghVfOb47mwM X-Google-Smtp-Source: AAOMgpcuuw8LbaWVeqqa7lAVKOsTyIx0pZnCZYr23V6kXFxh1zDiUpdFPwzT4ld0z0KzSnH/0G5ddA== X-Received: by 2002:a02:5103:: with SMTP id s3-v6mr8414236jaa.102.1532745574827; Fri, 27 Jul 2018 19:39:34 -0700 (PDT) Received: from librem (24-148-50-16.s5644.c3-0.mart-ubr1.chi-mart.il.cable.rcncustomer.com. [24.148.50.16]) by smtp.gmail.com with ESMTPSA id u125-v6sm3600665ita.15.2018.07.27.19.39.33 (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Fri, 27 Jul 2018 19:39:33 -0700 (PDT) From: Alex ter Weele X-Google-Original-From: Alex ter Weele References: <876018pojt.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> <87va98o9bz.fsf_-_@librem.i-did-not-set--mail-host-address--so-tickle-me> <87a7qj5o6j.fsf@fastmail.com> Date: Fri, 27 Jul 2018 21:39:33 -0500 In-Reply-To: <87a7qj5o6j.fsf@fastmail.com> (Marius Bakke's message of "Sun, 22 Jul 2018 16:40:20 +0200") Message-ID: <87muucqe1m.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="=-=-=" X-Spam-Score: 0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) --=-=-= Content-Type: text/plain Marius Bakke writes: > Alex ter Weele writes: > >> From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001 >> From: Alex ter Weele >> Date: Fri, 20 Jul 2018 21:35:14 -0500 >> Subject: [PATCH 1/2] gnu: agda: Compile .agda files. >> >> * gnu/packages/agda.scm: (agda)[arguments]: Compile .agda files. > > [...] > >> + (arguments >> + `(#:modules ((guix build haskell-build-system) >> + (guix build utils) >> + (srfi srfi-26)) >> + #:phases >> + (modify-phases %standard-phases >> + (add-after 'compile 'agda-compile >> + (lambda* (#:key outputs #:allow-other-keys) >> + (let* ((out (assoc-ref outputs "out")) >> + (agda-compiler (string-append out "/bin/agda")) >> + (agda-files-path (string-append >> + out >> + "/share/x86_64-linux-ghc-8.0.2/Agda-" > > This is unfortunate, since it hard-codes both architecture and GHC > version. Can you think of another method to find these files? > > Are there ".agda" files elsewhere under "/share"? Could the find-files > invokation below simply search "out/share", for example? > That works! >> + ,version >> + "/lib/prim/Agda/")) >> + (agda-files (append >> + (find-files agda-files-path "\\.agda$") >> + (find-files (string-append >> + agda-files-path >> + "Builtin") >> + "\\.agda$")))) > > (find-files ...) recurses through subdirectories, are you sure adding an > extra pass for "Builtin/*.agda" makes a difference here? > Removed. >> + (for-each (cut invoke agda-compiler <>) agda-files) >> + #t)))))) >> (home-page "http://wiki.portal.chalmers.se/agda/") > > Otherwise LGTM. > > [...] > >> From ff441cb0b500d247de9a54c3212f80b4fcfaf04f Mon Sep 17 00:00:00 2001 >> From: Alex ter Weele >> Date: Sat, 21 Jul 2018 10:57:35 -0500 >> Subject: [PATCH 2/2] gnu: Add emacs-agda2-mode >> >> * gnu/packages/agda.scm (emacs-agda2-mode): New variable. > > LGTM! I found a few potential issues with it. The variable and package names were mismatched, the inputs were inherited, and the home page was misspelled. Corrected in the following patch series. Thanks for the review! --=-=-= Content-Type: text/x-patch Content-Disposition: inline; filename=0001-gnu-agda-Compile-.agda-files.patch >From 51ad1e736760fb083fd04d933f9aaf6658b4b7fe Mon Sep 17 00:00:00 2001 From: Alex ter Weele Date: Fri, 20 Jul 2018 21:35:14 -0500 Subject: [PATCH 1/2] gnu: agda: Compile .agda files. * gnu/packages/agda.scm: (agda)[arguments]: Compile .agda files. --- gnu/packages/agda.scm | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index 6aa230116..d677bb7e5 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -67,6 +67,19 @@ ("ghc-text" ,ghc-text) ("ghc-unordered-containers" ,ghc-unordered-containers) ("ghc-zlib" ,ghc-zlib))) + (arguments + `(#:modules ((guix build haskell-build-system) + (guix build utils) + (srfi srfi-26)) + #:phases + (modify-phases %standard-phases + (add-after 'compile 'agda-compile + (lambda* (#:key outputs #:allow-other-keys) + (let* ((out (assoc-ref outputs "out")) + (agda-compiler (string-append out "/bin/agda"))) + (for-each (cut invoke agda-compiler <>) + (find-files (string-append out "/share") "\\.agda$")) + #t)))))) (home-page "http://wiki.portal.chalmers.se/agda/") (synopsis "Dependently typed functional programming language and proof assistant") -- 2.18.0 --=-=-= Content-Type: text/x-patch Content-Disposition: inline; filename=0002-gnu-Add-emacs-agda2-mode.patch >From b57cfb8766e85a4c2c8491415f2bf0d9357bcca2 Mon Sep 17 00:00:00 2001 From: Alex ter Weele Date: Sat, 21 Jul 2018 10:57:35 -0500 Subject: [PATCH 2/2] gnu: Add emacs-agda2-mode * gnu/packages/agda.scm (emacs-agda2-mode): New variable. --- gnu/packages/agda.scm | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm index d677bb7e5..7bdf10e61 100644 --- a/gnu/packages/agda.scm +++ b/gnu/packages/agda.scm @@ -20,6 +20,7 @@ #:use-module (gnu packages haskell) #:use-module (gnu packages haskell-check) #:use-module (gnu packages haskell-web) + #:use-module (guix build-system emacs) #:use-module (guix build-system haskell) #:use-module (guix build-system trivial) #:use-module (guix download) @@ -97,3 +98,19 @@ such as Coq, Epigram and NuPRL.") ;; Agda is distributed under the MIT license, and a couple of ;; source files are BSD-3. See LICENSE for details. (license (list license:expat license:bsd-3)))) + +(define-public emacs-agda2-mode + (package + (inherit agda) + (name "emacs-agda2-mode") + (build-system emacs-build-system) + (inputs '()) + (arguments + `(#:phases + (modify-phases %standard-phases + (add-after 'unpack 'enter-elisp-dir + (lambda _ (chdir "src/data/emacs-mode")))))) + (home-page "https://agda.readthedocs.io/en/latest/tools/emacs-mode.html") + (synopsis "Emacs mode for Agda") + (description "This Emacs mode enables interactive development with +Agda. It also aids the input of Unicode characters."))) -- 2.18.0 --=-=-=-- From unknown Sat Sep 06 14:23:55 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode. Resent-From: Marius Bakke Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sat, 28 Jul 2018 15:44:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 32235 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Alex ter Weele Cc: Alex ter Weele , 32235@debbugs.gnu.org Received: via spool by 32235-submit@debbugs.gnu.org id=B32235.15327925823814 (code B ref 32235); Sat, 28 Jul 2018 15:44:02 +0000 Received: (at 32235) by debbugs.gnu.org; 28 Jul 2018 15:43:02 +0000 Received: from localhost ([127.0.0.1]:33050 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fjRMz-0000zH-Ua for submit@debbugs.gnu.org; Sat, 28 Jul 2018 11:43:02 -0400 Received: from out1-smtp.messagingengine.com ([66.111.4.25]:41541) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fjRMy-0000z1-3b for 32235@debbugs.gnu.org; Sat, 28 Jul 2018 11:43:00 -0400 Received: from compute5.internal (compute5.nyi.internal [10.202.2.45]) by mailout.nyi.internal (Postfix) with ESMTP id F33C621B98; Sat, 28 Jul 2018 11:42:59 -0400 (EDT) Received: from mailfrontend1 ([10.202.2.162]) by compute5.internal (MEProxy); Sat, 28 Jul 2018 11:42:59 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=fastmail.com; h= cc:content-type:date:from:in-reply-to:message-id:mime-version :references:subject:to:x-me-sender:x-me-sender:x-sasl-enc; s= fm3; bh=mNpo/XqLkZ7DvZejFvFIUaZKvttEHA0VxVkLsJXGn7o=; b=fi4xHgEo 78++YdIxO14wQOnKCZeos25CVIATvIT0vy+yKMsl/4OmQePnqWXfwqGCdvJI5Q2H wJuwvM6qinFIimAt7U1Ca+4GoriUsry2h70uGdLlEIBxkIGuRrXF98yMfMBtnPXt F8wjgh2n/mq3NzhCwW9sN5RpzBLhj+tDu5QseOeBGd60WPGYAzMeR7tW5WUwp6/d 2XeUHShfpR2gtSs9NLvNcNp88soLLI/Y84CAXs1wuimSPqveuw8myCImFjM8Hnne +H/TFwwFLM3Y+ffXE+YSgPBn9+gv8XBFdcgV1qBsrpYCZw24CCqA7BdSt/8RQLMn LUyMU1gOFhqqyQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=cc:content-type:date:from:in-reply-to :message-id:mime-version:references:subject:to:x-me-sender :x-me-sender:x-sasl-enc; s=fm3; bh=mNpo/XqLkZ7DvZejFvFIUaZKvttEH A0VxVkLsJXGn7o=; b=Eh1SNV9a8B7+VqGIWvj+lLrb/iwlG+YWQkCIEkmGGUgzy vUrCEx3UggEzDRC+eD/XRZaERYLWOJo61FKnK67a1E50co8Q3B3M7Riv++aI9jJo 5zgTNC4fbuIwGQ58zAWLyFflaKfJy1w+eHZH/KKz+DrdunCW+noq2ecrfuqnV1Eg SfUbbjCRJU4Yy6/Dpdh5p3p/hOIPdXlmxFadsopyqDQlCD+hwcCYCf5ZoXXwTFtC dxl0xJTLfhQ04kWtrn4N2yuGWFA+EvbLQY22SAuf6MXSpjEoF4lEdDI5PT0ZswU7 39nmwbF8aIfXV3dWEu0WfHdT38CUSGwSHiFlTFitw== X-ME-Proxy: X-ME-Sender: Received: from localhost (95.92-221-151.customer.lyse.net [92.221.151.95]) by mail.messagingengine.com (Postfix) with ESMTPA id 61F7BE405A; Sat, 28 Jul 2018 11:42:59 -0400 (EDT) From: Marius Bakke In-Reply-To: <87muucqe1m.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> References: <876018pojt.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> <87va98o9bz.fsf_-_@librem.i-did-not-set--mail-host-address--so-tickle-me> <87a7qj5o6j.fsf@fastmail.com> <87muucqe1m.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> User-Agent: Notmuch/0.27 (https://notmuchmail.org) Emacs/26.1 (x86_64-pc-linux-gnu) Date: Sat, 28 Jul 2018 17:42:57 +0200 Message-ID: <87d0v74b9a.fsf@fastmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" X-Spam-Score: -0.7 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.7 (-) --=-=-= Content-Type: text/plain Alex ter Weele writes: > Marius Bakke writes: > >> Alex ter Weele writes: >> >>> From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001 >>> From: Alex ter Weele >>> Date: Fri, 20 Jul 2018 21:35:14 -0500 >>> Subject: [PATCH 1/2] gnu: agda: Compile .agda files. >>> >>> * gnu/packages/agda.scm: (agda)[arguments]: Compile .agda files. >> >> [...] >> >>> + (arguments >>> + `(#:modules ((guix build haskell-build-system) >>> + (guix build utils) >>> + (srfi srfi-26)) >>> + #:phases >>> + (modify-phases %standard-phases >>> + (add-after 'compile 'agda-compile >>> + (lambda* (#:key outputs #:allow-other-keys) >>> + (let* ((out (assoc-ref outputs "out")) >>> + (agda-compiler (string-append out "/bin/agda")) >>> + (agda-files-path (string-append >>> + out >>> + "/share/x86_64-linux-ghc-8.0.2/Agda-" >> >> This is unfortunate, since it hard-codes both architecture and GHC >> version. Can you think of another method to find these files? >> >> Are there ".agda" files elsewhere under "/share"? Could the find-files >> invokation below simply search "out/share", for example? >> > > That works! > >>> + ,version >>> + "/lib/prim/Agda/")) >>> + (agda-files (append >>> + (find-files agda-files-path "\\.agda$") >>> + (find-files (string-append >>> + agda-files-path >>> + "Builtin") >>> + "\\.agda$")))) >> >> (find-files ...) recurses through subdirectories, are you sure adding an >> extra pass for "Builtin/*.agda" makes a difference here? >> > > Removed. > >>> + (for-each (cut invoke agda-compiler <>) agda-files) >>> + #t)))))) >>> (home-page "http://wiki.portal.chalmers.se/agda/") >> >> Otherwise LGTM. >> >> [...] >> >>> From ff441cb0b500d247de9a54c3212f80b4fcfaf04f Mon Sep 17 00:00:00 2001 >>> From: Alex ter Weele >>> Date: Sat, 21 Jul 2018 10:57:35 -0500 >>> Subject: [PATCH 2/2] gnu: Add emacs-agda2-mode >>> >>> * gnu/packages/agda.scm (emacs-agda2-mode): New variable. >> >> LGTM! > > I found a few potential issues with it. The variable and package names > were mismatched, the inputs were inherited, and the home page was > misspelled. Corrected in the following patch series. > > Thanks for the review! Thanks for catching my review mistake! All LGTM. --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQEzBAEBCgAdFiEEu7At3yzq9qgNHeZDoqBt8qM6VPoFAltcjwEACgkQoqBt8qM6 VPqaFwgAgIYoF+a+pyEHKzSBd37tHuIeWDAiTtPXd/I63/RlS/wc8NnPtEALB7uT B6Lj4SwqRYNrE1nH0rsVMJbT12ePNsYpUBcLL2+Oc4y92xPY4rG11U5j+L4Z8yWw 7Cr3JADxJ2YlaH9vhCKIa8duGGZAwFPL9edz0r0IJ0cWvUDojXMpU5ZGOuOEw4wI wPz3Jm7dGNN3n0iEJFse94QcoOY0ZoQaG/ZbSOG5mmiK0zKxSdzrjM3CzpXanzVc QvFiKYmDJPC2nHi6hPDiejpQmOhkN1jDo6uZc6eW6UkS98BHeSS4bvGvwWWX0A8Y jUE1cKh1i7aj0N1sr6snDCFjkA8dig== =3KsZ -----END PGP SIGNATURE----- --=-=-=-- From unknown Sat Sep 06 14:23:55 2025 MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) X-Loop: help-debbugs@gnu.org From: help-debbugs@gnu.org (GNU bug Tracking System) To: Alex ter Weele Subject: bug#32235: closed (Re: [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode.) Message-ID: References: <874lgh4t8k.fsf@fastmail.com> <876018pojt.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> X-Gnu-PR-Message: they-closed 32235 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 32235@debbugs.gnu.org Date: Sun, 29 Jul 2018 21:40:02 +0000 Content-Type: multipart/mixed; boundary="----------=_1532900402-7244-1" This is a multi-part message in MIME format... ------------=_1532900402-7244-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Your bug report #32235: [PATCH] Fix Agda compilation, add Agda's emacs mode. which was filed against the guix-patches package, has been closed. The explanation is attached below, along with your original report. If you require more details, please reply to 32235@debbugs.gnu.org. --=20 32235: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D32235 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems ------------=_1532900402-7244-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at 32235-done) by debbugs.gnu.org; 29 Jul 2018 21:39:12 +0000 Received: from localhost ([127.0.0.1]:34140 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fjtPD-0001ri-LR for submit@debbugs.gnu.org; Sun, 29 Jul 2018 17:39:11 -0400 Received: from out1-smtp.messagingengine.com ([66.111.4.25]:32837) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fjtPB-0001ra-MM for 32235-done@debbugs.gnu.org; Sun, 29 Jul 2018 17:39:09 -0400 Received: from compute5.internal (compute5.nyi.internal [10.202.2.45]) by mailout.nyi.internal (Postfix) with ESMTP id 8F4F021ADF; Sun, 29 Jul 2018 17:39:09 -0400 (EDT) Received: from mailfrontend1 ([10.202.2.162]) by compute5.internal (MEProxy); Sun, 29 Jul 2018 17:39:09 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=fastmail.com; h= cc:content-type:date:from:in-reply-to:message-id:mime-version :references:subject:to:x-me-sender:x-me-sender:x-sasl-enc; s= fm3; bh=I/UAhycBvO3+YsIsUm0GNdlHv8gGrpXCimGOgliyhPE=; b=JzDDzuHW P8Omy2IdBRq4fjdtrxiDjKd8WXXK91iPBKc0FZQTswAVoiryEXOS7c5dWtMG68I/ v2aC+2+5zBuktxwdHO0557OP9kXkysLI4Cx2JhRYXHRuEBxEm6oEP88lBWt9HtLf R2cRLTTl/D62scOknPl2YzUIrUnjg8m5Qx1n7hMJO0EEH7TeKam3RmQTAnXAWagc CZulQgPSWkvXtiLPztjoO8tTmAJqsfHXHpu/SbsarwUbXEIxB4HvjWgNjv9ygtgj w1DzdJxMq8J75Ia/NmFnwkvsNUf9NqUsixwB2wX5zrXBm5kfXxuObzf5rdClwg/8 21LPkcGjxdHG3A== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=cc:content-type:date:from:in-reply-to :message-id:mime-version:references:subject:to:x-me-sender :x-me-sender:x-sasl-enc; s=fm3; bh=I/UAhycBvO3+YsIsUm0GNdlHv8gGr pXCimGOgliyhPE=; b=XmW3QIYieBL+yyzhiuBxkN77yvfh/ch0fvLgx6e93kj7t QaItFSuyPuAWJAa4GBEJhWQ5roulcep36YPRNdPPbH2zMoq1kaxyw3AtWyF63mvB vctoYEG8GVXhTOO/16HLD+RyhVaisD6ThdEbk/c3zIE1BCPIhOHJ10urXxW5gppq csWN6LNN1f9bCLVVgozZwRICSXcNw0jk4yUPxhdAQ1i3Cf87VdrdSaGn9HHctaO2 tLOlNEcw2i/eXaulWgIGU6nOhp3wLfuOv22UVDnORxORiPu6wimD3O+Ht7ID9Ybu LQ/u6AG2ZKPTV738/trmuSHSwnmSroIZzrS3cu/bA== X-ME-Proxy: X-ME-Sender: Received: from localhost (95.92-221-151.customer.lyse.net [92.221.151.95]) by mail.messagingengine.com (Postfix) with ESMTPA id F0F41E450F; Sun, 29 Jul 2018 17:39:08 -0400 (EDT) From: Marius Bakke To: Alex ter Weele Subject: Re: [bug#32235] [PATCH] Fix Agda compilation, add Agda's emacs mode. In-Reply-To: <87d0v74b9a.fsf@fastmail.com> References: <876018pojt.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> <87va98o9bz.fsf_-_@librem.i-did-not-set--mail-host-address--so-tickle-me> <87a7qj5o6j.fsf@fastmail.com> <87muucqe1m.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> <87d0v74b9a.fsf@fastmail.com> User-Agent: Notmuch/0.27 (https://notmuchmail.org) Emacs/26.1 (x86_64-pc-linux-gnu) Date: Sun, 29 Jul 2018 23:39:07 +0200 Message-ID: <874lgh4t8k.fsf@fastmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha512; protocol="application/pgp-signature" X-Spam-Score: -0.7 (/) X-Debbugs-Envelope-To: 32235-done Cc: Alex ter Weele , 32235-done@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.7 (-) --=-=-= Content-Type: text/plain Marius Bakke writes: > Alex ter Weele writes: > >> Marius Bakke writes: >> >>> Alex ter Weele writes: >>> >>>> From 2774cc719fa132ed8fd34a1d71f2c5a0f8697645 Mon Sep 17 00:00:00 2001 >>>> From: Alex ter Weele >>>> Date: Fri, 20 Jul 2018 21:35:14 -0500 >>>> Subject: [PATCH 1/2] gnu: agda: Compile .agda files. >>>> >>>> * gnu/packages/agda.scm: (agda)[arguments]: Compile .agda files. >>> >>> [...] >>> >>>> + (arguments >>>> + `(#:modules ((guix build haskell-build-system) >>>> + (guix build utils) >>>> + (srfi srfi-26)) >>>> + #:phases >>>> + (modify-phases %standard-phases >>>> + (add-after 'compile 'agda-compile >>>> + (lambda* (#:key outputs #:allow-other-keys) >>>> + (let* ((out (assoc-ref outputs "out")) >>>> + (agda-compiler (string-append out "/bin/agda")) >>>> + (agda-files-path (string-append >>>> + out >>>> + "/share/x86_64-linux-ghc-8.0.2/Agda-" >>> >>> This is unfortunate, since it hard-codes both architecture and GHC >>> version. Can you think of another method to find these files? >>> >>> Are there ".agda" files elsewhere under "/share"? Could the find-files >>> invokation below simply search "out/share", for example? >>> >> >> That works! >> >>>> + ,version >>>> + "/lib/prim/Agda/")) >>>> + (agda-files (append >>>> + (find-files agda-files-path "\\.agda$") >>>> + (find-files (string-append >>>> + agda-files-path >>>> + "Builtin") >>>> + "\\.agda$")))) >>> >>> (find-files ...) recurses through subdirectories, are you sure adding an >>> extra pass for "Builtin/*.agda" makes a difference here? >>> >> >> Removed. >> >>>> + (for-each (cut invoke agda-compiler <>) agda-files) >>>> + #t)))))) >>>> (home-page "http://wiki.portal.chalmers.se/agda/") >>> >>> Otherwise LGTM. >>> >>> [...] >>> >>>> From ff441cb0b500d247de9a54c3212f80b4fcfaf04f Mon Sep 17 00:00:00 2001 >>>> From: Alex ter Weele >>>> Date: Sat, 21 Jul 2018 10:57:35 -0500 >>>> Subject: [PATCH 2/2] gnu: Add emacs-agda2-mode >>>> >>>> * gnu/packages/agda.scm (emacs-agda2-mode): New variable. >>> >>> LGTM! >> >> I found a few potential issues with it. The variable and package names >> were mismatched, the inputs were inherited, and the home page was >> misspelled. Corrected in the following patch series. >> >> Thanks for the review! > > Thanks for catching my review mistake! All LGTM. Whoops, Ludovic helpfully reminded me on IRC that you don't yet have commit access. I've pushed these patches. (note that I added a #t after the chdir for emacs-agda2-mode, since the return value of chdir is unspecified) --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQEzBAEBCgAdFiEEu7At3yzq9qgNHeZDoqBt8qM6VPoFAlteM/sACgkQoqBt8qM6 VPpMggf/RzgJhxbYy87xtJOUPuAcUg8nnoWiZC9xS8+yz6+gUUPMXa+FuoW3Rb8H j3zcilxfk4G+Wb0FNlojfPHnhbyjKMTJGX8/FUR8DrdZsUW9nXhFF0AdhmDQUDHb JqqJqVPPTqx/QSO8Gh5plJsbegMXHf8XDExQ7RtiyxlYooNefOBD030rTm5t9Sfj yAAXMyLeDMOdM4I2Hz3+sKUNbCmFSZPmLYUT15XnodrR/KaWtfMvdGj86Tv/RjXk ze6QYiif6I73msFNJIpi2pjX3hhslXeLM5FTMlOUjSnI474TypsBqBK+XEKjJG7p tDNirm9IyWIMOl/Dnu3FJV3svkS40A== =dw1p -----END PGP SIGNATURE----- --=-=-=-- ------------=_1532900402-7244-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at submit) by debbugs.gnu.org; 21 Jul 2018 16:00:08 +0000 Received: from localhost ([127.0.0.1]:51228 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fguIh-0000Wp-NP for submit@debbugs.gnu.org; Sat, 21 Jul 2018 12:00:07 -0400 Received: from eggs.gnu.org ([208.118.235.92]:38950) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1fguId-0000Uq-Oa for submit@debbugs.gnu.org; Sat, 21 Jul 2018 12:00:03 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1fguIX-0007XZ-Ss for submit@debbugs.gnu.org; Sat, 21 Jul 2018 11:59:58 -0400 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM, T_DKIM_INVALID autolearn=disabled version=3.3.2 Received: from lists.gnu.org ([2001:4830:134:3::11]:40268) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1fguIX-0007XO-PC for submit@debbugs.gnu.org; Sat, 21 Jul 2018 11:59:57 -0400 Received: from eggs.gnu.org ([2001:4830:134:3::10]:58149) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1fguIW-0004zK-Pq for guix-patches@gnu.org; Sat, 21 Jul 2018 11:59:57 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1fguIT-0007VJ-OH for guix-patches@gnu.org; Sat, 21 Jul 2018 11:59:56 -0400 Received: from mail-it0-x22c.google.com ([2607:f8b0:4001:c0b::22c]:37111) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1fguIT-0007V9-Iz for guix-patches@gnu.org; Sat, 21 Jul 2018 11:59:53 -0400 Received: by mail-it0-x22c.google.com with SMTP id p17-v6so18367329itc.2 for ; Sat, 21 Jul 2018 08:59:53 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:subject:date:message-id:user-agent:mime-version; bh=47DEQpj8HBSa+/TImW+5JCeuQeRkm5NMpJWZG3hSuFU=; b=HcPk91rfZwmPQ/zlqBrda8lDffXIN4k3Q4hInAnBp7s5HZVwPecbA6pZRP3s/SD9mK YOPMwGnEuYsXWeVHZyKrX3L0ylYiroorvy8LUjcMzWLezL2C50deya8bdIjZ097OiCVl 9fXeYKCpxW3vCfem52FCWQfEDIbDJkA8c95jpUzmq+KCWo4V2zqFSqUIOvh6Gxr9R092 0/0P55kwxy717bp+zMR45z+3QaGyZvieP0x46YUwC1MbK+nsKh0WN3IO+++SLb1phpgw r7Ho1GOKYcYAf96bcfZWBoaxenW2VYUFl1IQoOw472ScgDGbCQBn9m6Lle99JUB4iAJj szxQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:subject:date:message-id:user-agent :mime-version; bh=47DEQpj8HBSa+/TImW+5JCeuQeRkm5NMpJWZG3hSuFU=; b=L1gNX52AjIv9AKlh1mXV/cP0g75ChpvslO6UXk2qoengs08lOR1JiLq1BfJCo+FUCw 8uNVOgUFzxOBdZcmTyFXfew3UaOtse2pwc6KSxn3bmFRo/EAF1jS72Is3/qhXA0jKImX 5ogiWk/F7AcuyJsfp31FlVRtF+rAW/9iivW4WUwYtQpsB/TGVv+wE1VxgOAzROs9vKvs YO24dJUNP00SQ+ElVuDNgOVOZfMdSA6LOS/4XiCw1bBblZPHMdFwG85jBAffD+39Ogur IfQPsfgI+B6MfVqVSM19ZZCz44FFpAHaS3rAgIA09wDsQ1A9tJISuOzIa7peifDZyLco x2rA== X-Gm-Message-State: AOUpUlG2oxlhlnMuNB6VB35B8lwz/g/Biqp87SJiiCHWFNHrzMvEchYZ TFwnBXw42PHZMA6Rk/fvwRow50DC X-Google-Smtp-Source: AAOMgpdIbfmh4iMJYe71LANpAI7nOouPl+dp6XtMj5ynu7GfKFZm6mt78VIWsXojomzlEtTmjEdS8A== X-Received: by 2002:a24:2581:: with SMTP id g123-v6mr5044562itg.59.1532188792248; Sat, 21 Jul 2018 08:59:52 -0700 (PDT) Received: from librem (24-148-50-16.s5644.c3-0.mart-ubr1.chi-mart.il.cable.rcncustomer.com. [24.148.50.16]) by smtp.gmail.com with ESMTPSA id k8-v6sm2639381itk.14.2018.07.21.08.59.51 for (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Sat, 21 Jul 2018 08:59:51 -0700 (PDT) From: Alex ter Weele X-Google-Original-From: Alex ter Weele To: guix-patches@gnu.org Subject: [PATCH] Fix Agda compilation, add Agda's emacs mode. Date: Sat, 21 Jul 2018 10:59:50 -0500 Message-ID: <876018pojt.fsf@librem.i-did-not-set--mail-host-address--so-tickle-me> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Received-From: 2001:4830:134:3::11 X-Spam-Score: -4.0 (----) X-Debbugs-Envelope-To: submit X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -5.0 (-----) ------------=_1532900402-7244-1--