GNU bug report logs - #37038
[PATCH] Add Cedille.

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 37038 in the body.
You can then email your comments to 37038 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: John Soo <jsoo1 <at> asu.edu>
To: guix-patches <at> gnu.org
Subject: [PATCH] Add Cedille.
Date: Thu, 15 Aug 2019 16:07:49 +0000

[Message part 1 (text/plain, inline)]

HI all,

I wanted to try out the Cedille language (cedille.github.io) so I packaged
it.  It has a nice emacs mode included and an interesting type theory.

Thanks!

- John

[Message part 2 (text/html, inline)]

[0001-gnu-Add-agda-ial.patch (text/x-patch, attachment)]

[0002-gnu-Add-cedille.patch (text/x-patch, attachment)]

Message #8 received at 37038 <at> debbugs.gnu.org (full text, mbox):

From: John Soo <jsoo1 <at> asu.edu>
To: 37038 <at> debbugs.gnu.org
Subject: Amending author email
Date: Fri, 16 Aug 2019 03:16:51 +0000

[Message part 1 (text/plain, inline)]

Hi all,

I realized just now that I had some ambient git configuration with the
wrong email address. I have amended the patches to reflect my correct email
address.

Thanks,

John

[Message part 2 (text/html, inline)]

[0001-gnu-Add-agda-ial.patch (text/x-patch, attachment)]

[0002-gnu-Add-cedille.patch (text/x-patch, attachment)]

Message #11 received at 37038 <at> debbugs.gnu.org (full text, mbox):

From: Ludovic Courtès <ludo <at> gnu.org>
To: John Soo <jsoo1 <at> asu.edu>
Cc: 37038 <at> debbugs.gnu.org
Subject: Re: [bug#37038] Amending author email
Date: Wed, 28 Aug 2019 00:32:24 +0200

Hi John,

John Soo <jsoo1 <at> asu.edu> skribis:

> From f9cfc764f79f2c454726ebef4a074e6e80bec449 Mon Sep 17 00:00:00 2001
> From: John Soo <jsoo1 <at> asu.edu>
> 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 ‘guix lint’ warnings.

> From 22ff16058b7b43622beaca1742b9520fb987310c Mon Sep 17 00:00:00 2001
> From: John Soo <jsoo1 <at> 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 ‘guix lint’ 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’d call the variable just ’lisp’; long names aren’t
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"))

‘string-append’ 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’.

Message #14 received at 37038 <at> debbugs.gnu.org (full text, mbox):

From: John Soo <jsoo1 <at> asu.edu>
To: Ludovic Courtès <ludo <at> gnu.org>
Cc: 37038 <at> debbugs.gnu.org
Subject: Re: [bug#37038] Amending author email
Date: Wed, 28 Aug 2019 05:05:20 +0000

[Message part 1 (text/plain, inline)]

> Applied with a followup commit to address ‘guix lint’ 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.

>  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 <jsoo1 <at> 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 ‘guix lint’ 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’d call the variable just ’lisp’; long names aren’t
> 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"))
>
> ‘string-append’ 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’.
>

[Message part 2 (text/html, inline)]

Message #17 received at 37038 <at> debbugs.gnu.org (full text, mbox):

From: John Soo <jsoo1 <at> asu.edu>
To: Ludovic Courtès <ludo <at> gnu.org>
Cc: 37038 <at> debbugs.gnu.org
Subject: Re: [bug#37038] Amending author email
Date: Wed, 28 Aug 2019 05:11:30 +0000

[Message part 1 (text/plain, inline)]

Hey everyone,

Sorry for that last response, stupid email client. Redoing that.  I would
love to use gnus for email but I think I need to work on a more recent
commit. Sorry for any formatting issues in my emails for now.

> Applied with a followup commit to address ‘guix lint’ 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.

>  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

> To aid readability, I’d call the variable just ’lisp’; long names aren’t
> helpful for local variables IMO.

Fixed, I agree.

> Should it be a FIXME?

I made it a FIXME.

> ‘string-append’ is unnecessary.

Fixed, woops!.

> M-q here if you use Emacs.  :-)

I am an Emacs user but I do not know what M-q does (evil mode user, here).
What does it do?

Thanks again!

- John

[Message part 2 (text/html, inline)]

[0001-gnu-agda-ial-Fix-install-step.patch (text/x-patch, attachment)]

[0002-gnu-Add-cedille.patch (text/x-patch, attachment)]

Message #20 received at 37038 <at> debbugs.gnu.org (full text, mbox):

From: John Soo <jsoo1 <at> asu.edu>
To: Ludovic Courtès <ludo <at> gnu.org>
Cc: 37038 <at> debbugs.gnu.org
Subject: Re: [bug#37038] Amending author email
Date: Wed, 28 Aug 2019 05:17:38 +0000

[Message part 1 (text/plain, inline)]

One last item:

> Could you (1) add this file to gnu/local.mk, and (2) address the
> remaining ‘guix lint’ warnings?

I thought my patches would fix the `guix lint` warnings, but they do not. I
do not know what to do about them, sorry.

Thanks again,

- John

[Message part 2 (text/html, inline)]

Message #23 received at 37038 <at> debbugs.gnu.org (full text, mbox):

From: Ricardo Wurmus <rekado <at> elephly.net>
To: John Soo <jsoo1 <at> asu.edu>
Cc: 37038 <at> debbugs.gnu.org, Ludovic Courtès <ludo <at> gnu.org>
Subject: Re: [bug#37038] Amending author email
Date: Wed, 28 Aug 2019 07:23:08 +0200

John Soo <jsoo1 <at> asu.edu> writes:

>> M-q here if you use Emacs.  :-)
>
> I am an Emacs user but I do not know what M-q does (evil mode user, here).
> What does it do?

It runs ‘fill-paragraph‘ on the text at point.  (Or
’paredit-reindent-defun“ if you’re using paredit.)

--
Ricardo

Message #26 received at 37038 <at> debbugs.gnu.org (full text, mbox):

From: John Soo <jsoo1 <at> asu.edu>
To: Ricardo Wurmus <rekado <at> elephly.net>
Cc: 37038 <at> debbugs.gnu.org, Ludovic Courtès <ludo <at> gnu.org>
Subject: Re: [bug#37038] Amending author email
Date: Wed, 28 Aug 2019 06:21:27 +0000

[Message part 1 (text/plain, inline)]

Hi Ricardo and Ludo,

Thank you for fill-paragraph, what a great function! I never knew. I love
how Emacs is an editor for all kinds of text aside from code.

I fixed the lint warnings from before and removed a dependency on git with
this patchset (along with the fill-paragraph magic).

Thanks again!

- John

[Message part 2 (text/html, inline)]

[0001-gnu-agda-ial-Fix-install-step.patch (text/x-patch, attachment)]

[0002-gnu-Add-cedille.patch (text/x-patch, attachment)]

Message #29 received at 37038 <at> debbugs.gnu.org (full text, mbox):

From: John Soo <jsoo1 <at> asu.edu>
To: Ricardo Wurmus <rekado <at> elephly.net>
Cc: 37038 <at> debbugs.gnu.org, Ludovic Courtès <ludo <at> gnu.org>
Subject: Re: [bug#37038] Amending author email
Date: Wed, 28 Aug 2019 15:10:30 +0000

[Message part 1 (text/plain, inline)]

Hi again,

One last set removing an unused import and moving a comment.

- John

[Message part 2 (text/html, inline)]

[0001-gnu-agda-ial-Fix-install-step.patch (application/x-patch, attachment)]

[0002-gnu-Add-cedille.patch (application/x-patch, attachment)]

Message #34 received at 37038-done <at> debbugs.gnu.org (full text, mbox):

From: Ludovic Courtès <ludo <at> gnu.org>
To: John Soo <jsoo1 <at> asu.edu>
Cc: Ricardo Wurmus <rekado <at> elephly.net>, 37038-done <at> debbugs.gnu.org
Subject: Re: [bug#37038] Amending author email
Date: Wed, 28 Aug 2019 17:48:25 +0200

Hi,

John Soo <jsoo1 <at> asu.edu> skribis:

> I fixed the lint warnings from before and removed a dependency on git with
> this patchset (along with the fill-paragraph magic).

Perfect, I applied both after tweaking the commit log of the second
patch.

Apologies if I introduced a regression in agda-ial when I switched it to
‘git-fetch’!

Thanks,
Ludo’.

Message #37 received at 37038-done <at> debbugs.gnu.org (full text, mbox):

From: John Soo <jsoo1 <at> asu.edu>
To: Ludovic Courtès <ludo <at> gnu.org>
Cc: Ricardo Wurmus <rekado <at> elephly.net>, 37038-done <at> debbugs.gnu.org
Subject: Re: [bug#37038] Amending author email
Date: Wed, 28 Aug 2019 10:00:01 -0700

No problem thanks so much Ludo!

> On Aug 28, 2019, at 8:48 AM, Ludovic Courtès <ludo <at> gnu.org> wrote:
> 
> Hi,
> 
> John Soo <jsoo1 <at> asu.edu> skribis:
> 
>> I fixed the lint warnings from before and removed a dependency on git with
>> this patchset (along with the fill-paragraph magic).
> 
> Perfect, I applied both after tweaking the commit log of the second
> patch.
> 
> Apologies if I introduced a regression in agda-ial when I switched it to
> ‘git-fetch’!
> 
> Thanks,
> Ludo’.

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.