diff options
author | Julien Lepiller <julien@lepiller.eu> | 2019-12-12 19:38:09 +0100 |
---|---|---|
committer | Julien Lepiller <julien@lepiller.eu> | 2019-12-12 20:10:18 +0100 |
commit | 4d6d88bb7e7c8fd1a406c063eb7771343a18ad4a (patch) | |
tree | 3e6026b31ef668c21e4c17a89008bcb0130bf5c4 /gnu/packages/coq.scm | |
parent | d8421fef1db92908719dfa92b78fce7952319abb (diff) | |
download | patches-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.scm | 25 |
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" |