gnu: Add coq-for-coqtail.

* gnu/packages/coq.scm (coq-for-coqtail): New variable.

Signed-off-by: Ludovic Courtès <ludo@gnu.org>
Change-Id: I0c08a02f7937786b52039307c1019ae3474e625c

1 files changed, 27 insertions, 0 deletions

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 @@
   #: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 @@ multi-precision arithmetic.  It also supports efficient numerical computations
 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")