guix_mirror_bot pushed a commit to branch master
in repository guix.
commit 6ba91aa9b0d7ae81a5077cac5a799e9ef272a412
Author: Andreas Enge <[email protected]>
AuthorDate: Tue Nov 18 17:48:45 2025 +0100
gnu: Remove cedille.
* gnu/packages/cedille.scm: Delete file.
* gnu/local.mk (GNU_SYSTEM_MODULES), po/packages/POTFILES.in: Unregister
deleted file.
Fixes: guix/guix#3637
Change-Id: I96da41d220b84a31a76e834e578e0f538d506cb6
---
gnu/local.mk | 1 -
gnu/packages/cedille.scm | 124 -----------------------------------------------
po/packages/POTFILES.in | 1 -
3 files changed, 126 deletions(-)
diff --git a/gnu/local.mk b/gnu/local.mk
index 7618a6ec51..2559ca26ad 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -187,7 +187,6 @@ 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 \
diff --git a/gnu/packages/cedille.scm b/gnu/packages/cedille.scm
deleted file mode 100644
index 1f00e8f698..0000000000
--- a/gnu/packages/cedille.scm
+++ /dev/null
@@ -1,124 +0,0 @@
-;;; GNU Guix --- Functional package management for GNU
-;;; Copyright © 2019 John Soo <[email protected]>
-;;;
-;;; 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 (gnu packages haskell-xyz)
- #: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.2")
- (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
- "1h5s6ayh3s76z184jai3jidcs4cjk8s4nvkkv2am8dg4gfsybq22"))))
- (inputs
- (list agda agda-ial ghc ghc-alex ghc-happy))
- (build-system emacs-build-system)
- (arguments
- `(#:phases
- (modify-phases %standard-phases
- (add-after 'unpack 'patch-cedille-paths
- (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/cedille")))
- (substitute* "cedille-mode/cedille-mode-info.el"
- (("\\(concat cedille-path-el \"cedille-info-main.info\"\\)")
- (string-append
- "\"" out "/share/info/cedille-info-main.info.gz\"")))
- #t)))
- (add-after 'patch-cedille-paths 'copy-cedille-mode
- (lambda* (#:key outputs #:allow-other-keys)
- (let* ((out (assoc-ref outputs "out"))
- (lisp
- (string-append
- out "/share/emacs/site-lisp/cedille/")))
- (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
- (search-input-directory inputs "/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"))
- (install-file "docs/info/cedille-info-main.info"
- (string-append out "/share/info"))
- #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)))
diff --git a/po/packages/POTFILES.in b/po/packages/POTFILES.in
index 284793ec71..f5d042844a 100644
--- a/po/packages/POTFILES.in
+++ b/po/packages/POTFILES.in
@@ -55,7 +55,6 @@ gnu/packages/calcurse.scm
gnu/packages/calendar.scm
gnu/packages/ccache.scm
gnu/packages/cdrom.scm
-gnu/packages/cedille.scm
gnu/packages/certs.scm
gnu/packages/check.scm
gnu/packages/chemistry.scm
