(address . guix-patches@gnu.org)
87zfk62i6i.fsf@antr.me
Deprecates coq-ide-server, which is now part of the main coq package.
* gnu/packages/coq.scm (coq): Update to 8.20.0.
[native-inputs]: Add python, rsync.
[arguments]: Patch tests, build coqide-server, symlink `coqidetop`.
(coq-ide-server): Deprecate package.
(coq-ide)[propagated-inputs]: Remove coq-ide-server.
(coq-for-coqtail): Remove hidden package.
* gnu/packages/coq.scm (vim-coqtail)[native-inputs]: Remove
coq-for-coqtail.
[native-inputs]: Add coq.
Change-Id: Ic9c3985b76938f78352b8735fb832c7a78519172
---
gnu/packages/coq.scm | 74 ++++++++++++++++++++------------------------
gnu/packages/vim.scm | 2 +-
2 files changed, 35 insertions(+), 41 deletions(-)
Toggle diff (151 lines)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 3ef91ad78a..71b14e0dd8 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -57,7 +57,7 @@ (define-module (gnu packages coq)
(define-public coq
(package
(name "coq")
- (version "8.18.0")
+ (version "8.20.0")
(source
(origin
(method git-fetch)
@@ -67,7 +67,7 @@ (define-public coq
(file-name (git-file-name name version))
(sha256
(base32
- "1qy71gdr4s2l6847b4nwns6akib2f7l725zb01m7zc26n6mrrh1m"))))
+ "0pf3sfq61w9h7r418pl28cvqidf9iwdn9zzkfbsb9afvj584slkp"))))
(native-search-paths
(list (search-path-specification
(variable "COQPATH")
@@ -75,9 +75,31 @@ (define-public coq
(build-system dune-build-system)
(arguments
(list
- #:package "coq-core,coq-stdlib,coq"
+ #:package "coq-core,coq-stdlib,coq,coqide-server"
#:phases
#~(modify-phases %standard-phases
+ (add-after 'unpack 'fix-tests
+ (lambda _
+ ;; In 8.20, the test Makefile incorrectly assumes installation
+ ;; occurs before tests. Fixing it here.
+ (substitute* "test-suite/Makefile"
+ ;; Disable IDE tests (not available in this package)
+ ((" ide ide ")
+ " ")
+ ;; Disable tests with incorrect paths
+ ;; TODO: Maybe fixable upstream in a future release?
+ ((" coq-makefile precomputed-time-tests ")
+ " ")
+ ((" \\$\\(VSUBSYSTEMS\\) misc ")
+ " $(VSUBSYSTEMS) ")
+ ((" coqdoc ssr ")
+ " ssr ")
+ ;; Set COQLIB to correct path
+ (("COQLIB\\?=")
+ "COQLIB=../../install/default/lib/coq")
+ ;; Override incorrect bin directory
+ (("BIN:=\\$\\(COQPREFIX\\)/bin/")
+ "BIN=../../install/default/bin/"))))
(add-before 'build 'configure
(lambda* (#:key outputs #:allow-other-keys)
(let* ((out (assoc-ref outputs "out"))
@@ -91,13 +113,18 @@ (define-public coq
(let* ((out (assoc-ref outputs "out"))
(libdir (string-append out "/lib/ocaml/site-lib")))
(invoke "dune" "install" "--prefix" out
- "--libdir" libdir "coq" "coq-core" "coq-stdlib")))))))
+ "--libdir" libdir "coq" "coq-core" "coq-stdlib"
+ "coqide-server")
+ ;; coqide searches for coqidetop on $PATH, but it is installed
+ ;; as coqidetop.opt
+ (symlink (string-append #$output "/bin/coqidetop.opt")
+ (string-append #$output "/bin/coqidetop"))))))))
(propagated-inputs
(list ocaml-zarith))
(inputs
(list gmp))
(native-inputs
- (list ocaml-ounit2 which))
+ (list ocaml-ounit2 python rsync which))
(properties '((upstream-name . "coq"))) ; also for inherited packages
(home-page "https://coq.inria.fr")
(synopsis "Proof assistant for higher-order logic")
@@ -110,14 +137,7 @@ (define-public coq
(license (list license:lgpl2.1 license:opl1.0+))))
(define-public coq-ide-server
- (package
- (inherit coq)
- (name "coq-ide-server")
- (arguments
- `(#:tests? #f
- #:package "coqide-server"))
- (inputs
- (list coq gmp))))
+ (deprecated-package "coq-ide-server" coq))
(define-public coq-ide
(package
@@ -127,7 +147,7 @@ (define-public coq-ide
`(#:tests? #f
#:package "coqide"))
(propagated-inputs
- (list coq coq-ide-server zlib))
+ (list coq zlib))
(inputs
(list lablgtk3 ocaml-lablgtk3-sourceview3))))
@@ -255,32 +275,6 @@ (define-public coq-flocq
inside Coq.")
(license license:lgpl3+)))
-;; Union of coq and coq-ide-server as vim-coqtail expects coqc and coqidetop
-;; to be in the same bin folder, when vim-coqtail is installed coqc and
-;; coqidetop will be in the "same" bin folder in the profile, so this is only
-;; required for testing the package.
-;;
-;; This is deeply ingrained in the internals of vim-coqtail so this is why
-;; it's necessary.
-(define-public coq-for-coqtail
- (hidden-package
- (package
- (inherit coq)
- (name "coq-for-coqtail")
- (source #f)
- (build-system trivial-build-system)
- (arguments
- '(#:modules ((guix build union))
- #:builder
- (begin
- (use-modules (ice-9 match)
- (guix build union))
- (match %build-inputs
- (((names . directories) ...)
- (union-build (assoc-ref %outputs "out")
- directories))))))
- (inputs (list coq coq-ide-server)))))
-
(define-public coq-gappa
(package
(name "coq-gappa")
diff --git a/gnu/packages/vim.scm b/gnu/packages/vim.scm
index e77578cf18..01b53d5d92 100644
--- a/gnu/packages/vim.scm
+++ b/gnu/packages/vim.scm
@@ -515,7 +515,7 @@ (define-public vim-coqtail
;; they don't get installed.
(delete-file-recursively "python/__pycache__")))))))
(native-inputs
- (list coq-for-coqtail
+ (list coq
python-pytest
vim-vader))
(propagated-inputs (list coq coq-ide-server))
base-commit: b8858d8b1344525d0d7ac78d8fb9dc1a577b85d3
--
2.46.0