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") | |
33 | (version "1.1.1") | |
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 | |
43 | "07kv9wncyipfjf5w4ax8h2p35g70zb1qw6zc4afd7c225xia55wp")))) | |
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") | |
59 | (string-append | |
60 | out "/share/emacs/site-lisp/guix.d/cedille-" | |
61 | ,version))) | |
62 | #t))) | |
63 | (add-after 'unpack 'copy-cedille-mode | |
64 | (lambda* (#:key outputs #:allow-other-keys) | |
65 | (let* ((out (assoc-ref outputs "out")) | |
66 | (lisp | |
67 | (string-append | |
68 | out "/share/emacs/site-lisp/guix.d/cedille-" | |
69 | ,version "/"))) | |
70 | (mkdir-p (string-append lisp "cedille-mode")) | |
71 | (copy-recursively | |
72 | "cedille-mode" | |
73 | (string-append lisp "cedille-mode")) | |
74 | (mkdir-p (string-append lisp "se-mode")) | |
75 | (copy-recursively | |
76 | "se-mode" | |
77 | (string-append lisp "se-mode")) | |
78 | #t))) | |
79 | ;; FIXME: Byte compilation fails | |
80 | (delete 'build) | |
81 | (replace 'check | |
82 | (lambda _ | |
83 | (with-directory-excursion "cedille-tests" | |
84 | (invoke "sh" "run-tests.sh")))) | |
85 | (add-after 'unpack 'patch-libraries | |
86 | (lambda _ (patch-shebang "create-libraries.sh") #t)) | |
87 | (add-after 'unpack 'copy-ial | |
88 | (lambda* (#:key inputs #:allow-other-keys) | |
89 | (copy-recursively | |
90 | (string-append (assoc-ref inputs "agda-ial") | |
91 | "/include/agda/ial") | |
92 | "ial") | |
93 | ;; Ambiguous module if main is included from ial | |
94 | (delete-file "ial/main.agda") | |
95 | #t)) | |
96 | (add-after 'check 'build-cedille | |
97 | ;; Agda has a hard time with parallel compilation | |
98 | (lambda _ | |
99 | (invoke "touch" "src/Templates.hs") | |
100 | (make-file-writable "src/Templates.hs") | |
101 | (invoke "touch" "src/templates.agda") | |
102 | (make-file-writable "src/templates.agda") | |
103 | (invoke "make" "--jobs=1"))) | |
104 | (add-after 'install 'install-cedille | |
105 | (lambda* (#:key outputs #:allow-other-keys) | |
106 | (let ((out (assoc-ref outputs "out"))) | |
107 | (copy-recursively | |
108 | "lib" (string-append out "/lib/cedille")) | |
109 | (install-file "cedille" (string-append out "/bin")) | |
110 | (install-file "core/cedille-core" | |
111 | (string-append out "/bin")) | |
112 | #t)))))) | |
113 | (home-page "https://cedille.github.io/") | |
114 | (synopsis | |
115 | "Language based on Calculus of Dependent Lambda Eliminations") | |
116 | (description | |
117 | "Cedille is an interactive theorem-prover and dependently typed | |
118 | programming language, based on extrinsic (aka Curry-style) type theory. This | |
119 | makes it rather different from type theories like Coq and Agda, which are | |
120 | intrinsic (aka Church-style). In Cedille, terms are nothing more than | |
121 | annotated versions of terms of pure untyped lambda calculus. In contrast, in | |
122 | Coq or Agda, the typing annotations are intrinsic parts of terms. The typing | |
123 | annotations can only be erased as an optimization under certain conditions, | |
124 | not by virtue of the definition of the type theory.") | |
125 | (license license:expat))) |