[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[bug#65820] [PATCH 2/3] gnu: Add coq-for-coqtail.
From: |
Jean-Pierre De Jesus DIAZ |
Subject: |
[bug#65820] [PATCH 2/3] gnu: Add coq-for-coqtail. |
Date: |
Fri, 8 Sep 2023 12:34:21 +0200 |
* gnu/packages/coq.scm (coq-for-coqtaill): New variable.
Signed-off-by: Jean-Pierre De Jesus DIAZ <jean@foundationdevices.com>
---
gnu/packages/coq.scm | 27 +++++++++++++++++++++++++++
1 file changed, 27 insertions(+)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 09ca4030ea..f30f231f3b 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -42,6 +42,7 @@ (define-module (gnu packages coq)
#:use-module (gnu packages texinfo)
#:use-module (guix build-system dune)
#:use-module (guix build-system gnu)
+ #:use-module (guix build-system trivial)
#:use-module (guix download)
#:use-module (guix gexp)
#:use-module (guix git-download)
@@ -285,6 +286,32 @@ (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")
--
2.34.1