GNU bug report logs - #65820
[PATCH 0/3] gnu: Add vim-coqtail.

Previous Next

Full log

Message #11 received at 65820 <at> debbugs.gnu.org (full text, mbox):

From: Jean-Pierre De Jesus DIAZ <jean <at> foundationdevices.com>
To: 65820 <at> debbugs.gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundationdevices.com>
Subject: [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 <at> 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

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.