From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:32814) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1i2q9m-0005Y7-Ua for guix-patches@gnu.org; Wed, 28 Aug 2019 01:06:08 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1i2q9j-0001Kd-5k for guix-patches@gnu.org; Wed, 28 Aug 2019 01:06:06 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:40899) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1i2q9i-0001K2-HS for guix-patches@gnu.org; Wed, 28 Aug 2019 01:06:03 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1i2q9i-0004md-Bd for guix-patches@gnu.org; Wed, 28 Aug 2019 01:06:02 -0400 Subject: [bug#37038] Amending author email Resent-Message-ID: MIME-Version: 1.0 References: <87tva2kznr.fsf@gnu.org> In-Reply-To: <87tva2kznr.fsf@gnu.org> From: John Soo Date: Wed, 28 Aug 2019 05:05:20 +0000 Message-ID: Content-Type: multipart/alternative; boundary="0000000000009920980591265610" 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: Ludovic =?UTF-8?Q?Court=C3=A8s?= Cc: 37038@debbugs.gnu.org --0000000000009920980591265610 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > Applied with a followup commit to address =E2=80=98guix lint=E2=80=99 war= nings. Thank you! I was unsure what to do about those lint errors. I updated cedille with the proper fetch to fix the lint issues with it. > Also, it fails to build for me I included a second patch to fix the build issue. It looks like this line in the Makefile would cause this problem: ./ial/ial.agda-lib: git submodule update --init --recursive > > 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? > > > --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. > --0000000000009920980591265610 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
> Applied with a followup commit to ad= dress =E2=80=98guix lint=E2=80=99 warnings.

Thank you! I was unsure what to do about those lint errors. I updated= cedille with the proper fetch to fix the lint issues with it.
>=C2=A0 Also, it fails to build for me

=
I included a second patch to fix the build issue. It looks like this l= ine in the Makefile would cause this problem:

./ia= l/ial.agda-lib:
git submodule update --init --recursive


> From 22ff16058b7b43622beaca1742b9520fb987310c Mon Sep 17 00:00:00 2001=
> From: John Soo <= jsoo1@asu.edu>
> 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?


--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---


[...]

> +=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0(lambda* (#:key outputs #:al= low-other-keys)
> +=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0(let* ((out (assoc-re= f outputs "out"))
> +=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= (cedille-site-lisp
> +=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= =C2=A0(string-append
> +=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= =C2=A0 out "/share/emacs/site-lisp/guix.d/cedille-"
> +=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= =C2=A0 ,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.

> +=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0;; Byte compilation fails
> +=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0(delete 'build)

Should it be a FIXME?

> +=C2=A0 =C2=A0 (synopsis
> +=C2=A0 =C2=A0 =C2=A0(string-append
> +=C2=A0 =C2=A0 =C2=A0 "Language based on Calculus of Dependent La= mbda Eliminations"))

=E2=80=98string-append=E2=80=99 is unnecessary.

> +=C2=A0 =C2=A0 (description
> +=C2=A0 =C2=A0 =C2=A0"Cedille is an interactive theorem-prover an= d dependently
> +typed programming language, based on extrinsic (aka Curry-style)
> +type theory.=C2=A0 This makes it rather different from type theories<= br> > +like Coq and Agda, which are intrinsic (aka Church-style).=C2=A0 In > +Cedille, terms are nothing more than annotated versions of terms
> +of pure untyped lambda calculus.=C2=A0 In contrast, in Coq or Agda, > +the typing annotations are intrinsic parts of terms.=C2=A0 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.=C2=A0 :-)

Could you send an updated patch?

Thanks,
Ludo=E2=80=99.
--0000000000009920980591265610--