summaryrefslogtreecommitdiff
path: root/gnu/packages/coq.scm
diff options
context:
space:
mode:
authorJulien Lepiller <julien@lepiller.eu>2019-12-12 19:38:09 +0100
committerJulien Lepiller <julien@lepiller.eu>2019-12-12 20:10:18 +0100
commit4d6d88bb7e7c8fd1a406c063eb7771343a18ad4a (patch)
tree3e6026b31ef668c21e4c17a89008bcb0130bf5c4 /gnu/packages/coq.scm
parentd8421fef1db92908719dfa92b78fce7952319abb (diff)
downloadpatches-4d6d88bb7e7c8fd1a406c063eb7771343a18ad4a.tar
patches-4d6d88bb7e7c8fd1a406c063eb7771343a18ad4a.tar.gz
gnu: coq: Split coqide.
* gnu/packages/coq.scm (coq)[outputs]: Add "ide" output.
Diffstat (limited to 'gnu/packages/coq.scm')
-rw-r--r--gnu/packages/coq.scm25
1 files changed, 25 insertions, 0 deletions
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 75b9831d39..7b2cdfec5d 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -58,6 +58,7 @@
(variable "COQPATH")
(files (list "lib/coq/user-contrib")))))
(build-system ocaml-build-system)
+ (outputs '("out" "ide"))
(inputs
`(("lablgtk" ,lablgtk)
("python" ,python-2)
@@ -72,6 +73,13 @@
(lambda _
(for-each make-file-writable (find-files "."))
#t))
+ (add-after 'unpack 'remove-lablgtk-references
+ (lambda _
+ ;; This is not used anywhere, but creates a reference to lablgtk in
+ ;; every binary
+ (substitute* '("config/coq_config.mli" "configure.ml")
+ ((".*coqideincl.*") ""))
+ #t))
(replace 'configure
(lambda* (#:key outputs #:allow-other-keys)
(let* ((out (assoc-ref outputs "out"))
@@ -88,6 +96,23 @@
"-j" (number->string (parallel-job-count))
"world")))
(delete 'check)
+ (add-after 'install 'remove-duplicate
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let* ((out (assoc-ref outputs "out"))
+ (bin (string-append out "/bin")))
+ ;; These are exact copies of the version without the .opt suffix.
+ ;; Remove them to save 35 MiB in the result
+ (delete-file (string-append bin "/coqtop.opt"))
+ (delete-file (string-append bin "/coqidetop.opt")))
+ #t))
+ (add-after 'install 'install-ide
+ (lambda* (#:key outputs #:allow-other-keys)
+ (let ((out (assoc-ref outputs "out"))
+ (ide (assoc-ref outputs "ide")))
+ (mkdir-p (string-append ide "/bin"))
+ (rename-file (string-append out "/bin/coqide")
+ (string-append ide "/bin/coqide")))
+ #t))
(add-after 'install 'check
(lambda _
(with-directory-excursion "test-suite"