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

Previous Next

Full log

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

Previous Next

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