From 4d6d88bb7e7c8fd1a406c063eb7771343a18ad4a Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Thu, 12 Dec 2019 19:38:09 +0100 Subject: gnu: coq: Split coqide. * gnu/packages/coq.scm (coq)[outputs]: Add "ide" output. --- gnu/packages/coq.scm | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) 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 @@ (define-public coq (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 @@ (define-public coq (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 @@ (define-public coq "-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" -- cgit v1.2.3