gnu: coq: Split coqide.
* gnu/packages/coq.scm (coq)[outputs]: Add "ide" output.
This commit is contained in:
parent
d8421fef1d
commit
4d6d88bb7e
1 changed files with 25 additions and 0 deletions
|
@ -58,6 +58,7 @@
|
||||||
(variable "COQPATH")
|
(variable "COQPATH")
|
||||||
(files (list "lib/coq/user-contrib")))))
|
(files (list "lib/coq/user-contrib")))))
|
||||||
(build-system ocaml-build-system)
|
(build-system ocaml-build-system)
|
||||||
|
(outputs '("out" "ide"))
|
||||||
(inputs
|
(inputs
|
||||||
`(("lablgtk" ,lablgtk)
|
`(("lablgtk" ,lablgtk)
|
||||||
("python" ,python-2)
|
("python" ,python-2)
|
||||||
|
@ -72,6 +73,13 @@
|
||||||
(lambda _
|
(lambda _
|
||||||
(for-each make-file-writable (find-files "."))
|
(for-each make-file-writable (find-files "."))
|
||||||
#t))
|
#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
|
(replace 'configure
|
||||||
(lambda* (#:key outputs #:allow-other-keys)
|
(lambda* (#:key outputs #:allow-other-keys)
|
||||||
(let* ((out (assoc-ref outputs "out"))
|
(let* ((out (assoc-ref outputs "out"))
|
||||||
|
@ -88,6 +96,23 @@
|
||||||
"-j" (number->string (parallel-job-count))
|
"-j" (number->string (parallel-job-count))
|
||||||
"world")))
|
"world")))
|
||||||
(delete 'check)
|
(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
|
(add-after 'install 'check
|
||||||
(lambda _
|
(lambda _
|
||||||
(with-directory-excursion "test-suite"
|
(with-directory-excursion "test-suite"
|
||||||
|
|
Reference in a new issue