From: "Ludovic Courtès" <ludo@gnu.org>
To: John Soo <jsoo1@asu.edu>
Cc: 37038@debbugs.gnu.org
Subject: [bug#37038] Amending author email
Date: Wed, 28 Aug 2019 00:32:24 +0200 [thread overview]
Message-ID: <87tva2kznr.fsf@gnu.org> (raw)
In-Reply-To: <CAKf5CqXjUa_ZDzuUxsKZ5mWHJ1yyb6N9Xx0-zqErh+cE23kgxQ@mail.gmail.com> (John Soo's message of "Fri, 16 Aug 2019 03:16:51 +0000")
Hi John,
John Soo <jsoo1@asu.edu> skribis:
> 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.
> 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:
--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’.
next prev parent reply other threads:[~2019-08-27 22:33 UTC|newest]
Thread overview: 11+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-08-15 16:07 [bug#37038] [PATCH] Add Cedille John Soo
2019-08-16 3:16 ` [bug#37038] Amending author email John Soo
2019-08-27 22:32 ` Ludovic Courtès [this message]
2019-08-28 5:05 ` John Soo
2019-08-28 5:11 ` John Soo
2019-08-28 5:17 ` John Soo
2019-08-28 5:23 ` Ricardo Wurmus
2019-08-28 6:21 ` John Soo
2019-08-28 15:10 ` John Soo
2019-08-28 15:48 ` bug#37038: " Ludovic Courtès
2019-08-28 17:00 ` [bug#37038] " John Soo
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
List information: https://guix.gnu.org/
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=87tva2kznr.fsf@gnu.org \
--to=ludo@gnu.org \
--cc=37038@debbugs.gnu.org \
--cc=jsoo1@asu.edu \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).