me
/
guix
Archived
1
0
Fork 0
Code

gnu: coq: Reword several comments. 

* gnu/packages/coq.scm (coq): Reword several comments to improve readability.
master
Brett Gilio 2020-01-06 01:34:23 -06:00
parent 1ac4004502
commit a5727da96a
No known key found for this signature in database
GPG Key ID: 672243C4A03F0EEE
1 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
gnu/packages/coq.scm
View File

@ -95,8 +95,8 @@
(lambda* (#:key outputs #:allow-other-keys) (lambda* (#:key outputs #:allow-other-keys)
(let* ((out (assoc-ref outputs "out")) (let* ((out (assoc-ref outputs "out"))
(bin (string-append out "/bin"))) (bin (string-append out "/bin")))
;; These are exact copies of the version without the .opt suffix. ;; These files are exact copies without `.opt` extension.
;; Remove them to save 35 MiB in the result ;; Removing these saves 35 MiB in the resulting package.
(delete-file (string-append bin "/coqtop.opt")) (delete-file (string-append bin "/coqtop.opt"))
(delete-file (string-append bin "/coqidetop.opt"))) (delete-file (string-append bin "/coqidetop.opt")))
#t)) #t))
@ -112,9 +112,9 @@
(lambda _ (lambda _
(with-directory-excursion "test-suite" (with-directory-excursion "test-suite"
;; These two tests fail. ;; These two tests fail.
;; This one fails because the output is not formatted as expected. ;; Fails because the output is not formatted as expected.
(delete-file-recursively "coq-makefile/timing") (delete-file-recursively "coq-makefile/timing")
;; This one fails because we didn't build coqtop.byte. ;; Fails because we didn't build coqtop.byte.
(delete-file-recursively "coq-makefile/findlib-package") (delete-file-recursively "coq-makefile/findlib-package")
(invoke "make"))))))) (invoke "make")))))))
(home-page "https://coq.inria.fr") (home-page "https://coq.inria.fr")
@ -123,7 +123,7 @@
"Coq is a proof assistant for higher-order logic, which allows the "Coq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal specification. development of computer programs consistent with their formal specification.
It is developed using Objective Caml and Camlp5.") It is developed using Objective Caml and Camlp5.")
;; The code is distributed under lgpl2.1. ;; The source code is distributed under lgpl2.1.
;; Some of the documentation is distributed under opl1.0+. ;; Some of the documentation is distributed under opl1.0+.
(license (list license:lgpl2.1 license:opl1.0+)))) (license (list license:lgpl2.1 license:opl1.0+))))