From 33a1ee7f17338dbfa39bd00e449c667f345d41fa Mon Sep 17 00:00:00 2001 From: Jean-Pierre De Jesus DIAZ Date: Fri, 8 Sep 2023 12:34:21 +0200 Subject: [PATCH] gnu: Add coq-for-coqtail. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * gnu/packages/coq.scm (coq-for-coqtail): New variable. Signed-off-by: Ludovic Courtès Change-Id: I0c08a02f7937786b52039307c1019ae3474e625c --- 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")