From 8b09f1a7c012dbff89b3e703a43f654e3121b4af Mon Sep 17 00:00:00 2001 From: John Soo 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/local.mk (cedille): Add cedille.scm to GNU_SYSTEM_MODULES. --- gnu/local.mk | 2 + gnu/packages/cedille.scm | 124 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 126 insertions(+) create mode 100644 gnu/packages/cedille.scm diff --git a/gnu/local.mk b/gnu/local.mk index a756316f77..8fb16a3ab6 100644 --- a/gnu/local.mk +++ b/gnu/local.mk @@ -21,6 +21,7 @@ # Copyright © 2018 Stefan Stefanović # Copyright © 2018 Maxim Cournoyer # Copyright © 2019 Guillaume Le Vaillant +# Copyright © 2019 John Soo # # This file is part of GNU Guix. # @@ -99,6 +100,7 @@ GNU_SYSTEM_MODULES = \ %D%/packages/calcurse.scm \ %D%/packages/ccache.scm \ %D%/packages/cdrom.scm \ + %D%/packages/cedille.scm \ %D%/packages/certs.scm \ %D%/packages/check.scm \ %D%/packages/chemistry.scm \ diff --git a/gnu/packages/cedille.scm b/gnu/packages/cedille.scm new file mode 100644 index 0000000000..36fa3ae17e --- /dev/null +++ b/gnu/packages/cedille.scm @@ -0,0 +1,124 @@ +;;; GNU Guix --- Functional package management for GNU +;;; Copyright © 2019 John Soo +;;; +;;; 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 . + +(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 (guix build-system emacs) + #: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 git-fetch) + (uri (git-reference + (url "https://github.com/cedille/cedille") + (commit (string-append "v" version)))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "07kv9wncyipfjf5w4ax8h2p35g70zb1qw6zc4afd7c225xia55wp")))) + (inputs + `(("agda" ,agda) + ("agda-ial" ,agda-ial) + ("ghc" ,ghc-8.4) + ("ghc-alex" ,ghc-alex) + ("ghc-happy" ,ghc-happy))) + (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")) + (lisp + (string-append + out "/share/emacs/site-lisp/guix.d/cedille-" + ,version "/"))) + (mkdir-p (string-append lisp "cedille-mode")) + (copy-recursively + "cedille-mode" + (string-append lisp "cedille-mode")) + (mkdir-p (string-append lisp "se-mode")) + (copy-recursively + "se-mode" + (string-append lisp "se-mode")) + #t))) + ;; FIXME: 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 "touch" "src/Templates.hs") + (make-file-writable "src/Templates.hs") + (invoke "touch" "src/templates.agda") + (make-file-writable "src/templates.agda") + (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 + "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