1 ;;; GNU Guix --- Functional package management for GNU
2 ;;; Copyright © 2019 John Soo <jsoo1@asu.edu>
4 ;;; This file is part of GNU Guix.
6 ;;; GNU Guix is free software; you can redistribute it and/or modify it
7 ;;; under the terms of the GNU General Public License as published by
8 ;;; the Free Software Foundation; either version 3 of the License, or (at
9 ;;; your option) any later version.
11 ;;; GNU Guix is distributed in the hope that it will be useful, but
12 ;;; WITHOUT ANY WARRANTY; without even the implied warranty of
13 ;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
14 ;;; GNU General Public License for more details.
16 ;;; You should have received a copy of the GNU General Public License
17 ;;; along with GNU Guix. If not, see <http://www.gnu.org/licenses/>.
19 (define-module (gnu packages cedille)
20 #:use-module (gnu packages)
21 #:use-module (gnu packages agda)
22 #:use-module (gnu packages emacs-xyz)
23 #:use-module (gnu packages haskell)
24 #:use-module (gnu packages haskell-xyz)
25 #:use-module (guix build-system emacs)
26 #:use-module (guix git-download)
27 #:use-module ((guix licenses) #:prefix license:)
28 #:use-module (guix packages))
30 (define-public cedille
38 (url "https://github.com/cedille/cedille")
39 (commit (string-append "v" version))))
40 (file-name (git-file-name name version))
43 "1h5s6ayh3s76z184jai3jidcs4cjk8s4nvkkv2am8dg4gfsybq22"))))
46 ("agda-ial" ,agda-ial)
48 ("ghc-alex" ,ghc-alex)
49 ("ghc-happy" ,ghc-happy)))
50 (build-system emacs-build-system)
53 (modify-phases %standard-phases
54 (add-after 'unpack 'patch-cedille-paths
55 (lambda* (#:key outputs #:allow-other-keys)
56 (let ((out (assoc-ref outputs "out")))
57 (substitute* "cedille-mode.el"
58 (("/usr/share/emacs/site-lisp/cedille-mode")
60 out "/share/emacs/site-lisp/cedille")))
61 (substitute* "cedille-mode/cedille-mode-info.el"
62 (("\\(concat cedille-path-el \"cedille-info-main.info\"\\)")
64 "\"" out "/share/info/cedille-info-main.info.gz\"")))
66 (add-after 'patch-cedille-paths 'copy-cedille-mode
67 (lambda* (#:key outputs #:allow-other-keys)
68 (let* ((out (assoc-ref outputs "out"))
71 out "/share/emacs/site-lisp/cedille/")))
72 (mkdir-p (string-append lisp "cedille-mode"))
75 (string-append lisp "cedille-mode"))
76 (mkdir-p (string-append lisp "se-mode"))
79 (string-append lisp "se-mode"))
81 ;; FIXME: Byte compilation fails
85 (with-directory-excursion "cedille-tests"
86 (invoke "sh" "run-tests.sh"))))
87 (add-after 'unpack 'patch-libraries
88 (lambda _ (patch-shebang "create-libraries.sh") #t))
89 (add-after 'unpack 'copy-ial
90 (lambda* (#:key inputs #:allow-other-keys)
92 (string-append (assoc-ref inputs "agda-ial")
95 ;; Ambiguous module if main is included from ial
96 (delete-file "ial/main.agda")
98 (add-after 'check 'build-cedille
99 ;; Agda has a hard time with parallel compilation
101 (invoke "touch" "src/Templates.hs")
102 (make-file-writable "src/Templates.hs")
103 (invoke "touch" "src/templates.agda")
104 (make-file-writable "src/templates.agda")
105 (invoke "make" "--jobs=1")))
106 (add-after 'install 'install-cedille
107 (lambda* (#:key outputs #:allow-other-keys)
108 (let ((out (assoc-ref outputs "out")))
110 "lib" (string-append out "/lib/cedille"))
111 (install-file "cedille" (string-append out "/bin"))
112 (install-file "core/cedille-core"
113 (string-append out "/bin"))
114 (install-file "docs/info/cedille-info-main.info"
115 (string-append out "/share/info"))
117 (home-page "https://cedille.github.io/")
119 "Language based on Calculus of Dependent Lambda Eliminations")
121 "Cedille is an interactive theorem-prover and dependently typed
122 programming language, based on extrinsic (aka Curry-style) type theory. This
123 makes it rather different from type theories like Coq and Agda, which are
124 intrinsic (aka Church-style). In Cedille, terms are nothing more than
125 annotated versions of terms of pure untyped lambda calculus. In contrast, in
126 Coq or Agda, the typing annotations are intrinsic parts of terms. The typing
127 annotations can only be erased as an optimization under certain conditions,
128 not by virtue of the definition of the type theory.")
129 (license license:expat)))