Commit | Line | Data |
---|---|---|
5416d9a9 JS |
1 | ;;; GNU Guix --- Functional package management for GNU |
2 | ;;; Copyright © 2019 John Soo <jsoo1@asu.edu> | |
3 | ;;; | |
4 | ;;; This file is part of GNU Guix. | |
5 | ;;; | |
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. | |
10 | ;;; | |
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. | |
15 | ;;; | |
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/>. | |
18 | ||
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) | |
aa0f6834 | 24 | #:use-module (gnu packages haskell-xyz) |
5416d9a9 JS |
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)) | |
29 | ||
30 | (define-public cedille | |
31 | (package | |
32 | (name "cedille") | |
1063dea4 | 33 | (version "1.1.2") |
5416d9a9 JS |
34 | (source |
35 | (origin | |
36 | (method git-fetch) | |
37 | (uri (git-reference | |
38 | (url "https://github.com/cedille/cedille") | |
39 | (commit (string-append "v" version)))) | |
40 | (file-name (git-file-name name version)) | |
41 | (sha256 | |
42 | (base32 | |
1063dea4 | 43 | "1h5s6ayh3s76z184jai3jidcs4cjk8s4nvkkv2am8dg4gfsybq22")))) |
5416d9a9 JS |
44 | (inputs |
45 | `(("agda" ,agda) | |
46 | ("agda-ial" ,agda-ial) | |
8e41d38a | 47 | ("ghc" ,ghc) |
5416d9a9 JS |
48 | ("ghc-alex" ,ghc-alex) |
49 | ("ghc-happy" ,ghc-happy))) | |
50 | (build-system emacs-build-system) | |
51 | (arguments | |
52 | `(#:phases | |
53 | (modify-phases %standard-phases | |
54 | (add-after 'unpack 'patch-cedille-path-el | |
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") | |
0a3ce077 | 59 | (string-append out "/share/emacs/site-lisp"))) |
5416d9a9 JS |
60 | #t))) |
61 | (add-after 'unpack 'copy-cedille-mode | |
62 | (lambda* (#:key outputs #:allow-other-keys) | |
63 | (let* ((out (assoc-ref outputs "out")) | |
0a3ce077 | 64 | (lisp (string-append out "/share/emacs/site-lisp"))) |
5416d9a9 JS |
65 | (mkdir-p (string-append lisp "cedille-mode")) |
66 | (copy-recursively | |
67 | "cedille-mode" | |
68 | (string-append lisp "cedille-mode")) | |
69 | (mkdir-p (string-append lisp "se-mode")) | |
70 | (copy-recursively | |
71 | "se-mode" | |
72 | (string-append lisp "se-mode")) | |
73 | #t))) | |
74 | ;; FIXME: Byte compilation fails | |
75 | (delete 'build) | |
76 | (replace 'check | |
77 | (lambda _ | |
78 | (with-directory-excursion "cedille-tests" | |
79 | (invoke "sh" "run-tests.sh")))) | |
80 | (add-after 'unpack 'patch-libraries | |
81 | (lambda _ (patch-shebang "create-libraries.sh") #t)) | |
82 | (add-after 'unpack 'copy-ial | |
83 | (lambda* (#:key inputs #:allow-other-keys) | |
84 | (copy-recursively | |
85 | (string-append (assoc-ref inputs "agda-ial") | |
86 | "/include/agda/ial") | |
87 | "ial") | |
88 | ;; Ambiguous module if main is included from ial | |
89 | (delete-file "ial/main.agda") | |
90 | #t)) | |
91 | (add-after 'check 'build-cedille | |
92 | ;; Agda has a hard time with parallel compilation | |
93 | (lambda _ | |
94 | (invoke "touch" "src/Templates.hs") | |
95 | (make-file-writable "src/Templates.hs") | |
96 | (invoke "touch" "src/templates.agda") | |
97 | (make-file-writable "src/templates.agda") | |
98 | (invoke "make" "--jobs=1"))) | |
99 | (add-after 'install 'install-cedille | |
100 | (lambda* (#:key outputs #:allow-other-keys) | |
101 | (let ((out (assoc-ref outputs "out"))) | |
102 | (copy-recursively | |
103 | "lib" (string-append out "/lib/cedille")) | |
104 | (install-file "cedille" (string-append out "/bin")) | |
105 | (install-file "core/cedille-core" | |
106 | (string-append out "/bin")) | |
107 | #t)))))) | |
108 | (home-page "https://cedille.github.io/") | |
109 | (synopsis | |
110 | "Language based on Calculus of Dependent Lambda Eliminations") | |
111 | (description | |
112 | "Cedille is an interactive theorem-prover and dependently typed | |
113 | programming language, based on extrinsic (aka Curry-style) type theory. This | |
114 | makes it rather different from type theories like Coq and Agda, which are | |
115 | intrinsic (aka Church-style). In Cedille, terms are nothing more than | |
116 | annotated versions of terms of pure untyped lambda calculus. In contrast, in | |
117 | Coq or Agda, the typing annotations are intrinsic parts of terms. The typing | |
118 | annotations can only be erased as an optimization under certain conditions, | |
119 | not by virtue of the definition of the type theory.") | |
120 | (license license:expat))) |