Merge branch 'master' into mesa-updates

Change-Id: Ide02272218e76dfae6dc9f8748871c8d61704260

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")