From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:43822) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1i2k1U-0002qh-9c for guix-patches@gnu.org; Tue, 27 Aug 2019 18:33:09 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1i2k1R-0008R4-2j for guix-patches@gnu.org; Tue, 27 Aug 2019 18:33:06 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:40750) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1i2k1O-0008QN-Ax for guix-patches@gnu.org; Tue, 27 Aug 2019 18:33:05 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1i2k1O-00037o-5q for guix-patches@gnu.org; Tue, 27 Aug 2019 18:33:02 -0400 Subject: [bug#37038] Amending author email Resent-Message-ID: From: Ludovic =?UTF-8?Q?Court=C3=A8s?= References: Date: Wed, 28 Aug 2019 00:32:24 +0200 In-Reply-To: (John Soo's message of "Fri, 16 Aug 2019 03:16:51 +0000") Message-ID: <87tva2kznr.fsf@gnu.org> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: John Soo Cc: 37038@debbugs.gnu.org Hi John, John Soo skribis: > From f9cfc764f79f2c454726ebef4a074e6e80bec449 Mon Sep 17 00:00:00 2001 > From: John Soo > Date: Mon, 12 Aug 2019 08:33:36 -0700 > Subject: [PATCH 1/2] gnu: Add agda-ial. > > * gnu/packages/agda.scm (agda-ial): new variable. Applied with a followup commit to address =E2=80=98guix lint=E2=80=99 warni= ngs. > From 22ff16058b7b43622beaca1742b9520fb987310c Mon Sep 17 00:00:00 2001 > From: John Soo > Date: Mon, 12 Aug 2019 08:43:07 -0700 > Subject: [PATCH 2/2] gnu: Add cedille. > > * gnu/packages/cedille.scm: new file. > * gnu/packages/cedille.scm (cedille): new variable. Could you (1) add this file to gnu/local.mk, and (2) address the remaining =E2=80=98guix lint=E2=80=99 warnings? Also, it fails to build for me: --8<---------------cut here---------------start------------->8--- make[1]: Leaving directory '/tmp/guix-build-cedille-1.1.1.drv-0/cedille-1.1= .1/core' git submodule update --init --recursive fatal: not a git repository (or any of the parent directories): .git make: *** [Makefile:102: ial/ial.agda-lib] Error 128 --8<---------------cut here---------------end--------------->8--- [...] > + (lambda* (#:key outputs #:allow-other-keys) > + (let* ((out (assoc-ref outputs "out")) > + (cedille-site-lisp > + (string-append > + out "/share/emacs/site-lisp/guix.d/cedille-" > + ,version "/"))) To aid readability, I=E2=80=99d call the variable just =E2=80=99lisp=E2=80= =99; long names aren=E2=80=99t helpful for local variables IMO. > + ;; Byte compilation fails > + (delete 'build) Should it be a FIXME? > + (synopsis > + (string-append > + "Language based on Calculus of Dependent Lambda Eliminations")) =E2=80=98string-append=E2=80=99 is unnecessary. > + (description > + "Cedille is an interactive theorem-prover and dependently > +typed programming language, based on extrinsic (aka Curry-style) > +type theory. This makes it rather different from type theories > +like Coq and Agda, which are intrinsic (aka Church-style). In > +Cedille, terms are nothing more than annotated versions of terms > +of pure untyped lambda calculus. In contrast, in Coq or Agda, > +the typing annotations are intrinsic parts of terms. The typing > +annotations can only be erased as an optimization under certain > +conditions, not by virtue of the definition of the type theory.") M-q here if you use Emacs. :-) Could you send an updated patch? Thanks, Ludo=E2=80=99.