[PATCH] Add Cedille.

  • Done
  • quality assurance status badge
Details
3 participants
  • John Soo
  • Ludovic Courtès
  • Ricardo Wurmus
Owner
unassigned
Submitted by
John Soo
Severity
normal

Debbugs page

John Soo wrote 6 years ago
(address . guix-patches@gnu.org)
CAKf5CqV5qA-XNK8o9rf1u384X1GiY-3EF4hJfVya+h8DUNA1EA@mail.gmail.com
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
Attachment: file
From 2d4a5299a1fbed8ed1f05a8a9fade8714375ff4f Mon Sep 17 00:00:00 2001
From: John Soo <jsoo@panosoft.com>
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.
---
gnu/packages/agda.scm | 48 +++++++++++++++++++++++++++++++++++++++++++
1 file changed, 48 insertions(+)

Toggle diff (72 lines)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 0f9b4299c3..8840790058 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -3,6 +3,7 @@
;;; Copyright © 2018 Ricardo Wurmus <rekado@elephly.net>
;;; Copyright © 2018 Alex Vong <alexvong1995@gmail.com>
;;; Copyright © 2018 Tobias Geerinckx-Rice <me@tobias.gr>
+;;; Copyright © 2018 John Soo <jsoo1@asu.edu>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -24,6 +25,7 @@
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (guix build-system emacs)
+ #:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
#:use-module (guix build-system trivial)
#:use-module (guix download)
@@ -154,3 +156,49 @@ such as Coq, Epigram and NuPRL.")
(synopsis "Emacs mode for Agda")
(description "This Emacs mode enables interactive development with
Agda. It also aids the input of Unicode characters.")))
+
+(define-public agda-ial
+ (package
+ (name "agda-ial")
+ (version "1.5.0")
+ (source
+ (origin
+ (method url-fetch)
+ (uri (string-append
+ "https://github.com/cedille/ial/archive/v"
+ version ".tar.gz"))
+ (file-name (string-append name "-" version))
+ (sha256
+ (base32
+ "0ilgalmx3kljy6j9i8d7w6r7ky4bq0xzxanwfr6kyx56mf2sf0zh"))))
+ (build-system gnu-build-system)
+ (inputs
+ `(("agda" ,agda)))
+ (arguments
+ `(#:parallel-build? #f
+ #:phases
+ (modify-phases %standard-phases
+ (delete 'configure)
+ (add-before 'build 'patch-dependencies
+ (lambda _ (patch-shebang "find-deps.sh") #t))
+ (delete 'check)
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (for-each
+ (lambda (file)
+ (install-file
+ file
+ (string-append
+ (assoc-ref outputs "out") "/include/agda/ial")))
+ (find-files "." ".*agda.*"))
+ #t)))))
+ (home-page "https://github.com/cedille/ial")
+ (synopsis
+ "The Iowa Agda Library")
+ (description
+ "The goal is to provide a concrete library focused on verification
+examples, as opposed to mathematics. The library has a good number
+of theorems for booleans, natural numbers, and lists. It also has
+trees, tries, vectors, and rudimentary IO. A number of good ideas
+come from Agda's standard library.")
+ (license license:expat)))
--
2.22.0
Attachment: 0002-gnu-Add-cedille.patch
John Soo wrote 6 years ago
Amending author email
(address . 37038@debbugs.gnu.org)
CAKf5CqXjUa_ZDzuUxsKZ5mWHJ1yyb6N9Xx0-zqErh+cE23kgxQ@mail.gmail.com
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
Attachment: file
From f9cfc764f79f2c454726ebef4a074e6e80bec449 Mon Sep 17 00:00:00 2001
From: John Soo <jsoo1@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.
---
gnu/packages/agda.scm | 48 +++++++++++++++++++++++++++++++++++++++++++
1 file changed, 48 insertions(+)

Toggle diff (72 lines)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 0f9b4299c3..8840790058 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -3,6 +3,7 @@
;;; Copyright © 2018 Ricardo Wurmus <rekado@elephly.net>
;;; Copyright © 2018 Alex Vong <alexvong1995@gmail.com>
;;; Copyright © 2018 Tobias Geerinckx-Rice <me@tobias.gr>
+;;; Copyright © 2018 John Soo <jsoo1@asu.edu>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -24,6 +25,7 @@
#:use-module (gnu packages haskell-check)
#:use-module (gnu packages haskell-web)
#:use-module (guix build-system emacs)
+ #:use-module (guix build-system gnu)
#:use-module (guix build-system haskell)
#:use-module (guix build-system trivial)
#:use-module (guix download)
@@ -154,3 +156,49 @@ such as Coq, Epigram and NuPRL.")
(synopsis "Emacs mode for Agda")
(description "This Emacs mode enables interactive development with
Agda. It also aids the input of Unicode characters.")))
+
+(define-public agda-ial
+ (package
+ (name "agda-ial")
+ (version "1.5.0")
+ (source
+ (origin
+ (method url-fetch)
+ (uri (string-append
+ "https://github.com/cedille/ial/archive/v"
+ version ".tar.gz"))
+ (file-name (string-append name "-" version))
+ (sha256
+ (base32
+ "0ilgalmx3kljy6j9i8d7w6r7ky4bq0xzxanwfr6kyx56mf2sf0zh"))))
+ (build-system gnu-build-system)
+ (inputs
+ `(("agda" ,agda)))
+ (arguments
+ `(#:parallel-build? #f
+ #:phases
+ (modify-phases %standard-phases
+ (delete 'configure)
+ (add-before 'build 'patch-dependencies
+ (lambda _ (patch-shebang "find-deps.sh") #t))
+ (delete 'check)
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (for-each
+ (lambda (file)
+ (install-file
+ file
+ (string-append
+ (assoc-ref outputs "out") "/include/agda/ial")))
+ (find-files "." ".*agda.*"))
+ #t)))))
+ (home-page "https://github.com/cedille/ial")
+ (synopsis
+ "The Iowa Agda Library")
+ (description
+ "The goal is to provide a concrete library focused on verification
+examples, as opposed to mathematics. The library has a good number
+of theorems for booleans, natural numbers, and lists. It also has
+trees, tries, vectors, and rudimentary IO. A number of good ideas
+come from Agda's standard library.")
+ (license license:expat)))
--
2.22.0
Attachment: 0002-gnu-Add-cedille.patch
Ludovic Courtès wrote 6 years ago
(name . John Soo)(address . jsoo1@asu.edu)(address . 37038@debbugs.gnu.org)
87tva2kznr.fsf@gnu.org
Hi John,

John Soo <jsoo1@asu.edu> skribis:

Toggle quote (7 lines)
> From f9cfc764f79f2c454726ebef4a074e6e80bec449 Mon Sep 17 00:00:00 2001
> From: John Soo <jsoo1@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.

Toggle quote (8 lines)
> 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 ‘guix lint’ warnings?

Also, it fails to build for me:

Toggle snippet (7 lines)
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


[...]

Toggle quote (7 lines)
> + (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.

Toggle quote (3 lines)
> + ;; Byte compilation fails
> + (delete 'build)

Should it be a FIXME?

Toggle quote (4 lines)
> + (synopsis
> + (string-append
> + "Language based on Calculus of Dependent Lambda Eliminations"))

‘string-append’ is unnecessary.

Toggle quote (11 lines)
> + (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’.
John Soo wrote 6 years ago
(name . Ludovic Courtès)(address . ludo@gnu.org)(address . 37038@debbugs.gnu.org)
CAKf5CqXbXgSkxA3pzPmKyd0BtexWhbEyiKz9kyYFbuJtBaDG7g@mail.gmail.com
Toggle quote (2 lines)
> 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.

Toggle quote (2 lines)
> 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


Toggle quote (62 lines)
> > 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 ‘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’.
>
Attachment: file
John Soo wrote 6 years ago
(name . Ludovic Courtès)(address . ludo@gnu.org)(address . 37038@debbugs.gnu.org)
CAKf5CqU_fKu6bP71MJo7tVv-Jbw+CRJf03-PwiHe=GR5Scu09A@mail.gmail.com
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.

Toggle quote (2 lines)
> 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.

Toggle quote (2 lines)
> 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

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

Fixed, I agree.

Toggle quote (2 lines)
> Should it be a FIXME?

I made it a FIXME.

Toggle quote (2 lines)
> ‘string-append’ is unnecessary.

Fixed, woops!.

Toggle quote (2 lines)
> 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
Attachment: file
From 00e546f650b5a909092e41fbeb45588096c92a18 Mon Sep 17 00:00:00 2001
From: John Soo <jsoo1@asu.edu>
Date: Tue, 27 Aug 2019 21:46:26 -0700
Subject: [PATCH 1/2] gnu: agda-ial: Fix install step.

* gnu/packages/agda.scm (agda-ial): copy library and agdai files when installing.
---
gnu/packages/agda.scm | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)

Toggle diff (15 lines)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 56d4b15940..c085bfac2e 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -190,7 +190,7 @@ Agda. It also aids the input of Unicode characters.")))
(for-each (lambda (file)
(make-file-writable file)
(install-file file include))
- (find-files "." "\\.agda$"))
+ (find-files "." "\\.agdai?(-lib)?$"))
#t))))))
(synopsis "The Iowa Agda Library")
(description
--
2.22.0
Attachment: 0002-gnu-Add-cedille.patch
John Soo wrote 6 years ago
(name . Ludovic Courtès)(address . ludo@gnu.org)(address . 37038@debbugs.gnu.org)
CAKf5CqVp6sF35XBMTSoxHbZ46M-sNNWW8eJZ1wwX-qsfxMJXAA@mail.gmail.com
One last item:

Toggle quote (3 lines)
> 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
Attachment: file
Ricardo Wurmus wrote 6 years ago
(name . John Soo)(address . jsoo1@asu.edu)(address . 37038@debbugs.gnu.org)(name . Ludovic Courtès)(address . ludo@gnu.org)
87r255hnib.fsf@elephly.net
John Soo <jsoo1@asu.edu> writes:

Toggle quote (5 lines)
>> 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
John Soo wrote 6 years ago
(name . Ricardo Wurmus)(address . rekado@elephly.net)(address . 37038@debbugs.gnu.org)(name . Ludovic Courtès)(address . ludo@gnu.org)
CAKf5CqV1n8372dGg6NuTLpBcNywmBVMm9M=bX6xd9fpOq1k_jA@mail.gmail.com
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
Attachment: file
From 00e546f650b5a909092e41fbeb45588096c92a18 Mon Sep 17 00:00:00 2001
From: John Soo <jsoo1@asu.edu>
Date: Tue, 27 Aug 2019 21:46:26 -0700
Subject: [PATCH 1/2] gnu: agda-ial: Fix install step.

* gnu/packages/agda.scm (agda-ial): copy library and agdai files when installing.
---
gnu/packages/agda.scm | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)

Toggle diff (15 lines)
diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 56d4b15940..c085bfac2e 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -190,7 +190,7 @@ Agda. It also aids the input of Unicode characters.")))
(for-each (lambda (file)
(make-file-writable file)
(install-file file include))
- (find-files "." "\\.agda$"))
+ (find-files "." "\\.agdai?(-lib)?$"))
#t))))))
(synopsis "The Iowa Agda Library")
(description
--
2.22.0
Attachment: 0002-gnu-Add-cedille.patch
John Soo wrote 6 years ago
(name . Ricardo Wurmus)(address . rekado@elephly.net)(address . 37038@debbugs.gnu.org)(name . Ludovic Courtès)(address . ludo@gnu.org)
CAKf5CqU6558MxkZyRQ_yb7mdjCq3QH2T=4KUqCHnDH9UYT1uCA@mail.gmail.com
Hi again,

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

- John
Attachment: file
Attachment: 0001-gnu-agda-ial-Fix-install-step.patch
Attachment: 0002-gnu-Add-cedille.patch
Ludovic Courtès wrote 6 years ago
(name . John Soo)(address . jsoo1@asu.edu)(name . Ricardo Wurmus)(address . rekado@elephly.net)(address . 37038-done@debbugs.gnu.org)
87blw9i94m.fsf@gnu.org
Hi,

John Soo <jsoo1@asu.edu> skribis:

Toggle quote (3 lines)
> 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’.
Closed
John Soo wrote 6 years ago
(name . Ludovic Courtès)(address . ludo@gnu.org)(name . Ricardo Wurmus)(address . rekado@elephly.net)(address . 37038-done@debbugs.gnu.org)
8DCCB479-9EB7-4B40-B2DB-C6C0EE2AB053@asu.edu
No problem thanks so much Ludo!

Toggle quote (17 lines)
> On Aug 28, 2019, at 8:48 AM, Ludovic Courtès <ludo@gnu.org> wrote:
>
> Hi,
>
> John Soo <jsoo1@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’.
Closed
?
Your comment

This issue is archived.

To comment on this conversation send an email to 37038@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it
mumi current 37038
Then, you may apply the latest patchset in this issue (with sign off)
mumi am -- -s
Or, compose a reply to this issue
mumi compose
Or, send patches to this issue
mumi send-email *.patch
You may also tag this issue. See list of standard tags. For example, to set the confirmed and easy tags
mumi command -t +confirmed -t +easy
Or, remove the moreinfo tag and set the help tag
mumi command -t -moreinfo -t +help