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

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

[Jean-Pierre De Jesus DIAZ via Guix-patches via]

This patch series adds vim-vader and vim-coqtail, plugins for testing
Vim plugins and for Coq interactive proof development, respectively.

Also added a hidden coq-for-coqtail package due to the inner workings of
vim-coqtail which expects coqc and coqidetop to be in the same bin
folder, this is only for testing.

For normal day to day usage of the plugin it will automatically find
coqc and coqidetop in the user's profile, or the user can manually
configure the Coq path if necessary.

Decided to add vim-vader and test vim-coqtail properly to start looking
into how a vim-build-system would in the future.  Probably needs more
package with tests before making a common build system for all of the
Vim plugin packages.

Jean-Pierre De Jesus DIAZ (3):
  gnu: Add vim-vader.
  gnu: Add coq-for-coqtail.
  gnu: Add vim-coqtail.

 gnu/packages/coq.scm |  27 ++++++++++
 gnu/packages/vim.scm | 114 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 141 insertions(+)


base-commit: d4645d5d25c9de0def9745c48a96504e500ec850
-- 
2.34.1

[bug#65820] [PATCH 1/3] gnu: Add vim-vader.

[Jean-Pierre De Jesus DIAZ via Guix-patches via]

* gnu/packages/vim.scm (vim-vader): New variable.

Signed-off-by: Jean-Pierre De Jesus DIAZ <jean@foundationdevices.com>
---
 gnu/packages/vim.scm | 50 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

diff --git a/gnu/packages/vim.scm b/gnu/packages/vim.scm
index 122f0f8ee7..e7c51c1c2d 100644
--- a/gnu/packages/vim.scm
+++ b/gnu/packages/vim.scm
@@ -14,6 +14,7 @@
 ;;; Copyright © 2021 Foo Chuan Wei <chuanwei.foo@hotmail.com>
 ;;; Copyright © 2022, 2023 Luis Henrique Gomes Higin65820@debbugs.gnu.orgo <luishenriquegh2701@gmail.com>
 ;;; Copyright © 2023 Charles Jackson <charles.b.jackson@protonmail.com>
+;;; Copyright © 2023 Foundation Devices, Inc. <hello@foundationdevices.com>
 ;;;
 ;;; This file is part of GNU Guix.
 ;;;
@@ -1479,3 +1480,52 @@ (define-public vim-nerdcommenter
 operations and styles which are invoked via key mappings and a menu.  These
 operations are available for most filetypes.")
     (license license:cc0)))
+
+(define-public vim-vader
+  (let ((revision "0")
+        (commit "6fff477431ac3191c69a3a5e5f187925466e275a"))
+    (package
+      (name "vim-vader")
+      (version (git-version "0.4.0" revision commit))
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://github.com/junegunn/vader.vim")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "179dbbqdyl6qf6jdb6kdazn3idz17m1h2n88rlggb1wnly74vjin"))))
+      (build-system copy-build-system)
+      (arguments
+       '(#:install-plan
+             '(("autoload" "share/vim/vimfiles/")
+               ("doc" "share/vim/vimfiles/")
+               ("ftdetect" "share/vim/vimfiles/")
+               ("ftplugin" "share/vim/vimfiles/")
+               ("plugin" "share/vim/vimfiles/")
+               ("syntax" "share/vim/vimfiles/"))
+         #:phases
+         (modify-phases %standard-phases
+           (add-before 'install 'check
+             (lambda* (#:key tests? #:allow-other-keys)
+               (when tests?
+                 ;; FIXME: suite1.vader fails with an unknown reason,
+                 ;; lang-if.vader requires Python and Ruby.
+                 (substitute* "test/vader.vader"
+                   (("Include.*feature/suite1.vader.*$") "")
+                   (("Include.*feature/lang-if.vader.*$") ""))
+
+                 (display "Running Vim tests\n")
+                 (with-directory-excursion "test"
+                   (setenv "VADER_TEST_VIM" "vim -E")
+                   (invoke "bash" "./run-tests.sh"))))))))
+      (native-inputs (list vim))
+      (home-page "https://github.com/junegunn/vader.vim")
+      (synopsis "Test framework for Vimscript")
+      (description "Vader is a test framework for Vimscript designed to
+simplify the process of writing and running unit tests.  Vader.vim provides an
+intuitive test syntax for defining test cases and expectations, it also can
+be integrated with @acronym{CI, Continuous Integration} pipelines to
+automate testing and is compatible with Vim and Neovim.")
+      (license license:expat)))) ;; Specified in README.md.
-- 
2.34.1

[bug#65820] [PATCH 2/3] gnu: Add coq-for-coqtail.

[Jean-Pierre De Jesus DIAZ via Guix-patches via]

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

Signed-off-by: Jean-Pierre De Jesus DIAZ <jean@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

[bug#65820] [PATCH 3/3] gnu: Add vim-coqtail.

[Jean-Pierre De Jesus DIAZ via Guix-patches via]

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

Signed-off-by: Jean-Pierre De Jesus DIAZ <jean@foundationdevices.com>
---
 gnu/packages/vim.scm | 64 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

diff --git a/gnu/packages/vim.scm b/gnu/packages/vim.scm
index e7c51c1c2d..957b0d4f2e 100644
--- a/gnu/packages/vim.scm
+++ b/gnu/packages/vim.scm
@@ -49,7 +49,9 @@ (define-module (gnu packages vim)
   #:use-module (gnu packages attr)
   #:use-module (gnu packages autotools)
   #:use-module (gnu packages base)
+  #:use-module (gnu packages check)
   #:use-module (gnu packages code)
+  #:use-module (gnu packages coq)
   #:use-module (gnu packages enlightenment)
   #:use-module (gnu packages fontutils)
   #:use-module (gnu packages gawk)
@@ -463,6 +465,68 @@ (define-public vim-context-filetype
       (home-page "https://github.com/Shougo/context_filetype.vim")
       (license license:expat)))) ; ??? check again
 
+(define-public vim-coqtail
+  (let ((commit "dfe3939c9caff69d9af76bfd74f1a40fb7dc5609")
+        (revision "0"))
+    (package
+      (name "vim-coqtail")
+      (version (git-version "1.7.0" revision commit))
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://github.com/whonore/Coqtail")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "0av2m075n6z05ah9ndrgnp9s16yrz6n2lj0igd9fh3c5k41x5xks"))))
+      (build-system copy-build-system)
+      (arguments
+       '(#:install-plan
+         '(("autoload" "share/vim/vimfiles/")
+           ("doc" "share/vim/vimfiles/")
+           ("ftdetect" "share/vim/vimfiles/")
+           ("ftplugin" "share/vim/vimfiles/")
+           ("indent" "share/vim/vimfiles/")
+           ("python" "share/vim/vimfiles/")
+           ("syntax" "share/vim/vimfiles/"))
+         #:phases
+         (modify-phases %standard-phases
+           (add-before 'install 'check
+             (lambda* (#:key inputs native-inputs tests? #:allow-other-keys)
+               (when tests?
+                 (display "Running Python unit tests.\n")
+                 (setenv "PYTHONPATH" (string-append (getcwd) "/python"))
+                 (invoke "pytest" "-q" "tests/unit")
+
+                 (display "Running Python Coq tests.\n")
+                 (invoke "pytest" "-q" "tests/coq")
+
+                 (display "Running Vim unit tests.\n")
+                 (let* ((vim-vader (assoc-ref (or native-inputs inputs)
+                                              "vim-vader"))
+                        (vader-path (string-append vim-vader
+                                                   "/share/vim/vimfiles")))
+                   (with-directory-excursion "tests/vim"
+                     (setenv "VADER_PATH" vader-path)
+                     (invoke "vim" "-E" "-Nu" "vimrc"
+                             "-c" "Vader! *.vader")))
+
+                 ;; Remove __pycache__ files generated during testing so that
+                 ;; they don't get installed.
+                 (delete-file-recursively "python/__pycache__")))))))
+      (native-inputs
+       (list coq-for-coqtail
+             python-pytest
+             vim-full ;; Plugin needs Python 3.
+             vim-vader))
+      (propagated-inputs (list coq coq-ide-server))
+      (synopsis "Interactive Coq proofs in Vim")
+      (description "Coqtail enables interactive Coq proof development in Vim
+similar to CoqIDE or ProofGeneral.")
+      (home-page "https://github.com/whonore/Coqtail")
+      (license license:expat))))
+
 (define-public vim-fugitive
   (package
     (name "vim-fugitive")
-- 
2.34.1

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

[Ludovic Courtès]

Hello,

Jean-Pierre De Jesus DIAZ <jean@foundationdevices.com> skribis:

>   gnu: Add vim-vader.
>   gnu: Add coq-for-coqtail.
>   gnu: Add vim-coqtail.

Finally applied.  Thanks for the patches and for the explanations!

Ludo’.