gnu/packages/cedille.scm

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