mirror of
git://git.savannah.gnu.org/guix.git
synced 2023-12-14 03:33:07 +01:00
gnu: Add cedille.
* gnu/packages/cedille.scm: New file. * gnu/local.mk (GNU_SYSTEM_MODULES): Add it. Signed-off-by: Ludovic Courtès <ludo@gnu.org>
This commit is contained in:
John Soo
Ludovic Courtès
parent
83ac4c099a
commit
5416d9a942
2 changed files with 126 additions and 0 deletions
|
|
@ -21,6 +21,7 @@
|
|||
# Copyright © 2018 Stefan Stefanović <stefanx2ovic@gmail.com>
|
||||
# Copyright © 2018 Maxim Cournoyer <maxim.cournoyer@gmail.com>
|
||||
# Copyright © 2019 Guillaume Le Vaillant <glv@posteo.net>
|
||||
# Copyright © 2019 John Soo <jsoo1@asu.edu>
|
||||
#
|
||||
# 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 \
|
||||
|
|
|
|||
124
gnu/packages/cedille.scm
Normal file
124
gnu/packages/cedille.scm
Normal file
|
|
@ -0,0 +1,124 @@
|
|||
;;; GNU Guix --- Functional package management for GNU
|
||||
;;; Copyright © 2019 John Soo <jsoo1@asu.edu>
|
||||
;;;
|
||||
;;; 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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
(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)))
|
||||
Loading…
Reference in a new issue