TakeV
/
guix
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

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
This commit is contained in:
Jean-Pierre De Jesus DIAZ 2023-09-08 12:34:21 +02:00 committed by Ludovic Courtès
parent ff8e8d2f1e
commit 33a1ee7f17
No known key found for this signature in database
GPG Key ID: 090B11993D9AEBB5
1 changed files with 27 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
gnu/packages/coq.scm
View File

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