me/guix
Archived
1
0
Fork 0
Code Activity

gnu: coq-mathcomp: Use INVOKE.

Browse source 
* gnu/packages/coq.scm (coq-mathcomp)[arguments]: Unconditionally return #T
from build phases.
This commit is contained in:
Ricardo Wurmus 2019-01-25 09:28:53 +01:00
parent ace73a93cd
commit 492ee4f83b
No known key found for this signature in database
GPG key ID: 197A5888235FACAC
1 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
gnu/packages/coq.scm
View file

@ -295,15 +295,14 @@ assistant.")
(modify-phases %standard-phases (modify-phases %standard-phases
(delete 'configure) (delete 'configure)
(add-before 'build 'chdir (add-before 'build 'chdir
(lambda _ (lambda _ (chdir "mathcomp") #t))
(chdir "mathcomp")))
(replace 'install (replace 'install
(lambda* (#:key outputs #:allow-other-keys) (lambda* (#:key outputs #:allow-other-keys)
(setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/")) (setenv "COQLIB" (string-append (assoc-ref outputs "out") "/lib/coq/"))
(zero? (system* "make" "-f" "Makefile.coq" (invoke "make" "-f" "Makefile.coq"
(string-append "COQLIB=" (assoc-ref outputs "out") (string-append "COQLIB=" (assoc-ref outputs "out")
"/lib/coq/") "/lib/coq/")
"install"))))))) "install"))))))
(home-page "https://math-comp.github.io/math-comp/") (home-page "https://math-comp.github.io/math-comp/")
(synopsis "Mathematical Components for Coq") (synopsis "Mathematical Components for Coq")
(description "Mathematical Components for Coq has its origins in the formal (description "Mathematical Components for Coq has its origins in the formal