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 | |
be41d7d9 | 54 | (add-after 'unpack 'patch-cedille-paths |
5416d9a9 JS |
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") | |
a8f1b520 JS |
59 | (string-append |
60 | out "/share/emacs/site-lisp/cedille"))) | |
be41d7d9 JS |
61 | (substitute* "cedille-mode/cedille-mode-info.el" |
62 | (("\\(concat cedille-path-el \"cedille-info-main.info\"\\)") | |
63 | (string-append | |
64 | "\"" out "/share/info/cedille-info-main.info.gz\""))) | |
5416d9a9 | 65 | #t))) |
be41d7d9 | 66 | (add-after 'patch-cedille-paths 'copy-cedille-mode |
5416d9a9 JS |
67 | (lambda* (#:key outputs #:allow-other-keys) |
68 | (let* ((out (assoc-ref outputs "out")) | |
a8f1b520 JS |
69 | (lisp |
70 | (string-append | |
71 | out "/share/emacs/site-lisp/cedille/"))) | |
5416d9a9 JS |
72 | (mkdir-p (string-append lisp "cedille-mode")) |
73 | (copy-recursively | |
74 | "cedille-mode" | |
75 | (string-append lisp "cedille-mode")) | |
76 | (mkdir-p (string-append lisp "se-mode")) | |
77 | (copy-recursively | |
78 | "se-mode" | |
79 | (string-append lisp "se-mode")) | |
80 | #t))) | |
81 | ;; FIXME: Byte compilation fails | |
82 | (delete 'build) | |
83 | (replace 'check | |
84 | (lambda _ | |
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) | |
91 | (copy-recursively | |
92 | (string-append (assoc-ref inputs "agda-ial") | |
93 | "/include/agda/ial") | |
94 | "ial") | |
95 | ;; Ambiguous module if main is included from ial | |
96 | (delete-file "ial/main.agda") | |
97 | #t)) | |
98 | (add-after 'check 'build-cedille | |
99 | ;; Agda has a hard time with parallel compilation | |
100 | (lambda _ | |
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"))) | |
109 | (copy-recursively | |
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")) | |
be41d7d9 JS |
114 | (install-file "docs/info/cedille-info-main.info" |
115 | (string-append out "/share/info")) | |
5416d9a9 JS |
116 | #t)))))) |
117 | (home-page "https://cedille.github.io/") | |
118 | (synopsis | |
119 | "Language based on Calculus of Dependent Lambda Eliminations") | |
120 | (description | |
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))) |