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