| Message ID | CAKf5CqXjUa_ZDzuUxsKZ5mWHJ1yyb6N9Xx0-zqErh+cE23kgxQ@mail.gmail.com |
|---|---|
| State | Accepted |
| Headers | show |
| Series | [bug#37038] Amending author email | expand |
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’.
> 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’. >
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. --- gnu/packages/cedille.scm | 125 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 125 insertions(+) create mode 100644 gnu/packages/cedille.scm diff --git a/gnu/packages/cedille.scm b/gnu/packages/cedille.scm new file mode 100644 index 0000000000..1d6ff88673 --- /dev/null +++ b/gnu/packages/cedille.scm @@ -0,0 +1,125 @@ +;;; GNU Guix --- Functional package management for GNU +;;; Copyright © 2019 John Soo <jsoo1@asu.edu> +;;; +;;; This file is part of GNU Guix. +;;; +;;; GNU Guix is free software; you can redistribute it and/or modify it +;;; under the terms of the GNU General Public License as published by +;;; the Free Software Foundation; either version 3 of the License, or (at +;;; your option) any later version. +;;; +;;; GNU Guix is distributed in the hope that it will be useful, but +;;; WITHOUT ANY WARRANTY; without even the implied warranty of +;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;;; GNU General Public License for more details. +;;; +;;; You should have received a copy of the GNU General Public License +;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>. + +(define-module (gnu packages cedille) + #:use-module (gnu packages) + #:use-module (gnu packages agda) + #:use-module (gnu packages emacs-xyz) + #:use-module (gnu packages haskell) + #:use-module (gnu packages version-control) + #:use-module (guix build-system emacs) + #:use-module (guix download) + #:use-module (guix git-download) + #:use-module ((guix licenses) #:prefix license:) + #:use-module (guix packages)) + +(define-public cedille + (package + (name "cedille") + (version "1.1.1") + (source + (origin + (method url-fetch) + (uri (string-append + "https://github.com/cedille/cedille/archive/v" + version ".tar.gz")) + (sha256 + (base32 + "05b32fsshcjrbh9ysz4pfv5y5jndkycd7qrg8sdh4spnlf077r92")))) + (inputs + `(("agda" ,agda) + ("agda-ial" ,agda-ial) + ("ghc" ,ghc-8.4) + ("ghc-alex" ,ghc-alex) + ("ghc-happy" ,ghc-happy) + ("git" ,git))) + (build-system emacs-build-system) + (arguments + `(#:phases + (modify-phases %standard-phases + (add-after 'unpack 'patch-cedille-path-el + (lambda* (#:key outputs #:allow-other-keys) + (let ((out (assoc-ref outputs "out"))) + (substitute* "cedille-mode.el" + (("/usr/share/emacs/site-lisp/cedille-mode") + (string-append + out "/share/emacs/site-lisp/guix.d/cedille-" + ,version))) + #t))) + (add-after 'unpack 'copy-cedille-mode + (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 "/"))) + (mkdir-p + (string-append cedille-site-lisp "cedille-mode")) + (copy-recursively + "cedille-mode" + (string-append cedille-site-lisp "cedille-mode")) + (mkdir-p + (string-append cedille-site-lisp "se-mode")) + (copy-recursively + "se-mode" + (string-append cedille-site-lisp "se-mode")) + #t))) + ;; Byte compilation fails + (delete 'build) + (replace 'check + (lambda _ + (with-directory-excursion "cedille-tests" + (invoke "sh" "run-tests.sh")))) + (add-after 'unpack 'patch-libraries + (lambda _ (patch-shebang "create-libraries.sh") #t)) + (add-after 'unpack 'copy-ial + (lambda* (#:key inputs #:allow-other-keys) + (copy-recursively + (string-append (assoc-ref inputs "agda-ial") + "/include/agda/ial") + "ial") + ;; Ambiguous module if main is included from ial + (delete-file "ial/main.agda") + #t)) + (add-after 'check 'build-cedille + ;; Agda has a hard time with parallel compilation + (lambda _ (invoke "make" "--jobs=1"))) + (add-after 'install 'install-cedille + (lambda* (#:key outputs #:allow-other-keys) + (let ((out (assoc-ref outputs "out"))) + (copy-recursively + "lib" (string-append out "/lib/cedille")) + (install-file "cedille" (string-append out "/bin")) + (install-file "core/cedille-core" + (string-append out "/bin")) + #t)))))) + (home-page "https://cedille.github.io/") + (synopsis + (string-append + "Language based on Calculus of Dependent Lambda Eliminations")) + (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.") + (license license:expat))) -- 2.22.0