From unknown Sat Aug 09 01:29:05 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#65820] [PATCH 0/3] gnu: Add vim-coqtail. Resent-From: Jean-Pierre De Jesus DIAZ Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Fri, 08 Sep 2023 10:33:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 65820 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 65820@debbugs.gnu.org Cc: Jean-Pierre De Jesus DIAZ X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.169416918013456 (code B ref -1); Fri, 08 Sep 2023 10:33:01 +0000 Received: (at submit) by debbugs.gnu.org; 8 Sep 2023 10:33:00 +0000 Received: from localhost ([127.0.0.1]:42269 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qeYnM-0003Uw-E8 for submit@debbugs.gnu.org; Fri, 08 Sep 2023 06:33:00 -0400 Received: from lists.gnu.org ([2001:470:142::17]:41602) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qeYnI-0003Uf-6z for submit@debbugs.gnu.org; Fri, 08 Sep 2023 06:32:59 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1qeYn8-0003mn-QH for guix-patches@gnu.org; Fri, 08 Sep 2023 06:32:46 -0400 Received: from mail-wm1-x333.google.com ([2a00:1450:4864:20::333]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1qeYn6-0008FA-CN for guix-patches@gnu.org; Fri, 08 Sep 2023 06:32:46 -0400 Received: by mail-wm1-x333.google.com with SMTP id 5b1f17b1804b1-3ff1c397405so22072915e9.3 for ; Fri, 08 Sep 2023 03:32:42 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=foundationdevices.com; s=google; t=1694169161; x=1694773961; darn=gnu.org; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=4Cj9HIlwSZI/Dztr8jTULucaKPGjaYJauIORD1XWajI=; b=KurHMPutxuELWc5+a9Q8jW5ZSGkBVEZpkL/EXtgzanBMEocTBJl5XiCGYcM0AUjyyX j7Crf8N8hSK+cxNDiLIPT1WblRSfkZMEVeicbgkErcR+HaSa9LmqStMTA5lapBxDy8hb JqifxM3UOOxx6UXMtADNLKWT14CVcCUnvUtTTRpFzejxUQMA29cNo2h8rCNaJuqCgfAs 8F1aBquXk1v7OIWQKUWxaeGAqa73Q6XZ4TNXVbZpwsLNF3SQlRmZWxuAFFV7w9Mn3nQZ lGf9Tn8r8qHRtoKCZtMShqFDt1JjOu1tPcGl8f3/je+zOdaYkwJuIQql8UE7PpESWPCS UUqA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1694169161; x=1694773961; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=4Cj9HIlwSZI/Dztr8jTULucaKPGjaYJauIORD1XWajI=; b=tVuk0xShSBoFFvDbGrRFw4A8i+iQuHjFD8fImvr6ztWQeOTGf8GkrGMyAFXVk+TuzG w2roICXmE5MdZXsadApmcOuGhVbcSQR8omITOCzMT/f7yCO/RNgXcQqkBhwRTHIT308n K6iFWJ+vaesj+nczAlQIFb2U1qLKEy8RnMARQWJl8ObZPPlLPEeXJ2rELQHhbmkFZ6qO 102Xr9XJ54lKCkoHjZBb38LivHy+XqSaF8LkQSx/coO5HD2fgqRvfI/WUXQsPSx8fuWr UM0Qco6CvhV2VwF0RnVaxyX63mbVvBUKVEEwdGMOKbPSXPyX1Dg0Pmxbl0ggbQEPAEdN YMsQ== X-Gm-Message-State: AOJu0YwQguZBQ29IMmRq6PkezBiQqvZr2R0hqhO73fWGm1Y0Ow/oTuJm LCl7w47HVAkv2z6zqcXUv2E0GoJlcXCwVhf+CAphiw== X-Google-Smtp-Source: AGHT+IGbTTHceqrZgvj34ykBvKdWh964Lb2Rioj3ye3CocwtbHcQ53DP20yizhgorW2UyTIxXqiDyA== X-Received: by 2002:a7b:c445:0:b0:3fe:18a3:b3c with SMTP id l5-20020a7bc445000000b003fe18a30b3cmr1781049wmi.12.1694169161233; Fri, 08 Sep 2023 03:32:41 -0700 (PDT) Received: from omen15.home ([89.131.29.87]) by smtp.gmail.com with ESMTPSA id h5-20020adffd45000000b0031c5d74ecd8sm1746126wrs.84.2023.09.08.03.32.40 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 08 Sep 2023 03:32:40 -0700 (PDT) From: Jean-Pierre De Jesus DIAZ Date: Fri, 8 Sep 2023 12:32:24 +0200 Message-Id: <20230908103223.21492-1-jean@foundationdevices.com> X-Mailer: git-send-email 2.34.1 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit Received-SPF: pass client-ip=2a00:1450:4864:20::333; envelope-from=jean@foundationdevices.com; helo=mail-wm1-x333.google.com X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: 1.0 (+) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) 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 From unknown Sat Aug 09 01:29:05 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#65820] [PATCH 1/3] gnu: Add vim-vader. References: <20230908103223.21492-1-jean@foundationdevices.com> In-Reply-To: <20230908103223.21492-1-jean@foundationdevices.com> Resent-From: Jean-Pierre De Jesus DIAZ Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Fri, 08 Sep 2023 10:35:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 65820 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 65820@debbugs.gnu.org Cc: Jean-Pierre De Jesus DIAZ Received: via spool by 65820-submit@debbugs.gnu.org id=B65820.169416928813652 (code B ref 65820); Fri, 08 Sep 2023 10:35:02 +0000 Received: (at 65820) by debbugs.gnu.org; 8 Sep 2023 10:34:48 +0000 Received: from localhost ([127.0.0.1]:42274 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qeYp5-0003Y7-UL for submit@debbugs.gnu.org; Fri, 08 Sep 2023 06:34:48 -0400 Received: from mail-wm1-x331.google.com ([2a00:1450:4864:20::331]:62609) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qeYp2-0003Xt-EQ for 65820@debbugs.gnu.org; Fri, 08 Sep 2023 06:34:46 -0400 Received: by mail-wm1-x331.google.com with SMTP id 5b1f17b1804b1-401d2e11dacso19947185e9.0 for <65820@debbugs.gnu.org>; Fri, 08 Sep 2023 03:34:42 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=foundationdevices.com; s=google; t=1694169276; x=1694774076; darn=debbugs.gnu.org; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=odHDJip+0UJQ89Fpblqy23/hK3FyYRmpQ+jZsLftRh0=; b=WUiqbSoLzRB4o5nIx04Wpq7jjE21kGGcxlhqF1OWoQKaVGCwDZQSfH8PJq8zKBJ0Se nubUaGXWNbUi9vc2dCxp2wOXQGurpfHxDcnRTbguTwintunGbIMQZ348/6u9em7Gm2nc fH2jzu8Yc19nXMakzbsL+iEO/2Jlpnug7xQEWpdG3G8HoH+qz40yD7zbfaADZD3O6Emy sBngb72KBFnQNSFdDAwc0m0xIYZlknUrFa9wIFwZ69IkWOwtzQrf3R5YW06BAj1S+6Bz AQd+y5XRT2otnATYLu1WSpRIjRb5zfaN7jhvM8OV7/dlifv1Ey/rs912MLlPqTOeyY6D hujA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1694169276; x=1694774076; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=odHDJip+0UJQ89Fpblqy23/hK3FyYRmpQ+jZsLftRh0=; b=xAzc4U7/DBIGlKIna62Vq/JX/LtwmRLF7Y87ghst4SaDl76/IbNke7SQvIyWgsuiS5 Q9R6r7jLw28iCFWcjhlzX7HkslQDCcmmhqNqym6Sq7ywIWEpOjDd4XcsFBUZxbzyyYZj XJgJA5kDa7VCxN9faw/uBD2HI0+CJZH2wupX/UdCMdpCeCT73Fy2E7DiJLxlryZeQ6hE Jiw0Ozuo9yb75j34tVOh76fTg7bw0uhtS84pPwRwxUXoqsTjBDd8dccQ2o8HeaiV0kId 1EUmnpKUS1e6UiDRYbdEjmJkJApij2unYwZ2DUlZQozeF0hQhq5RdbC5ILTWGcxESB13 SnpA== X-Gm-Message-State: AOJu0YycuKGURQKauFeHUQQ+ci0O/84TN/3XV4zEU3pAVr367HmXKldb rnXzKmKt85JQGDVjOYk0XZs7eo+yw/Ry+KwbaWd+dA== X-Google-Smtp-Source: AGHT+IGQh4s+RXJkihonKqpZ59xsELyOnVgY3PrK5XCsuTXxJZ+0iSodGMYN2VdZa9zdFX2mhHO00w== X-Received: by 2002:a05:600c:5127:b0:402:f91e:df80 with SMTP id o39-20020a05600c512700b00402f91edf80mr842543wms.3.1694169275678; Fri, 08 Sep 2023 03:34:35 -0700 (PDT) Received: from omen15.home ([89.131.29.87]) by smtp.gmail.com with ESMTPSA id l40-20020a05600c1d2800b00402f7b50517sm1442102wms.40.2023.09.08.03.34.34 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 08 Sep 2023 03:34:35 -0700 (PDT) From: Jean-Pierre De Jesus DIAZ Date: Fri, 8 Sep 2023 12:34:19 +0200 Message-Id: <20230908103419.21662-1-jean@foundationdevices.com> X-Mailer: git-send-email 2.34.1 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * gnu/packages/vim.scm (vim-vader): New variable. Signed-off-by: Jean-Pierre De Jesus DIAZ --- 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 ;;; Copyright © 2022, 2023 Luis Henrique Gomes Higin65820@debbugs.gnu.orgo ;;; Copyright © 2023 Charles Jackson +;;; Copyright © 2023 Foundation Devices, Inc. ;;; ;;; 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 From unknown Sat Aug 09 01:29:05 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#65820] [PATCH 2/3] gnu: Add coq-for-coqtail. Resent-From: Jean-Pierre De Jesus DIAZ Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Fri, 08 Sep 2023 10:35:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 65820 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 65820@debbugs.gnu.org Cc: Jean-Pierre De Jesus DIAZ Received: via spool by 65820-submit@debbugs.gnu.org id=B65820.169416929913676 (code B ref 65820); Fri, 08 Sep 2023 10:35:02 +0000 Received: (at 65820) by debbugs.gnu.org; 8 Sep 2023 10:34:59 +0000 Received: from localhost ([127.0.0.1]:42277 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qeYpH-0003YV-CT for submit@debbugs.gnu.org; Fri, 08 Sep 2023 06:34:59 -0400 Received: from mail-wm1-x32c.google.com ([2a00:1450:4864:20::32c]:46177) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qeYpE-0003YI-P4 for 65820@debbugs.gnu.org; Fri, 08 Sep 2023 06:34:57 -0400 Received: by mail-wm1-x32c.google.com with SMTP id 5b1f17b1804b1-40037db2fe7so20313755e9.0 for <65820@debbugs.gnu.org>; Fri, 08 Sep 2023 03:34:54 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=foundationdevices.com; s=google; t=1694169288; x=1694774088; darn=debbugs.gnu.org; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:from:to:cc:subject:date :message-id:reply-to; bh=likTLAVy4m2thwcPyzFS2S3Fmviwvjj+nKuqok3GFqg=; b=LF0OrIhu7RYYGIYpJAMVTSx0VeRU/hJWP/UySlnF0ag2fVkFFjLRQIPvrCD0S82QUq ZUctTAuYwlMiPs/rPA7bn8nvliU7x/GTFz4c3LzLF33+ET00PgNFEYK9M8H3MrgnDn1R wn+unTU8g70acvounz7fC243CX+fqEWpmxKMdoVVHtjPI1NzTsp2blzJMc5Uff4RdZc+ nmuU+RM7u5CHjPoBBu1Xie9WtguPYl5ZrEzxOfAd8r31qj5d/bcAxxocYLbtISrrdfyn wO/n74ug9XVEXwV23GpJHuQ6OhGwAqlYWCQewYPOSHD7FFzYCv5hBacyOj90+XpiWa5F 8dkA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1694169288; x=1694774088; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=likTLAVy4m2thwcPyzFS2S3Fmviwvjj+nKuqok3GFqg=; b=mWeO4VlBnGizlsNtEgINi0UthTdyWfCjiotRNZoS8qwlLvrT3qyAvn9A1ALDUh3f/p 1jvbrOHKsoT6EmZ0KG8pDKAfDkzeKXaM8/oFwqVfGxxn9y1NkYztS1ddCmZEahNKxJhU qPz1UQsCHxnxa823zjRTdvJSWxO/WJo/PIbNN1WClNPQOeMROdVfo1vnVsiBr+2STNA6 8WnEEuQv+VlJMqPiaLZkz0va2r6R/pCOmqQoxgRNH4OcyKZr59+xq6tvKkGK8eIampR1 OCNW0SR/dbQktUHLLZ7yI2vmk493Yu0K8OCtwjnz2/lQLCsvXkSlacvzO2XzfG44W23T RP7g== X-Gm-Message-State: AOJu0Yxji0kdL2NjEvayHLKi8UfhYbYA/Gpm2nJbAGOqXnpOiRea9tH2 whFuZl+l7GtWB3IKNz6P9MsO3Iz18O2FLN9LQ5dTDA== X-Google-Smtp-Source: AGHT+IHbhL4AjrFZc7dQW6OkcvrqK/cy3PPwWkWwsBQheHCXPlzzE4kBPqnTIagmiTyXwz7faFwTEw== X-Received: by 2002:a05:600c:2295:b0:401:aa8f:7562 with SMTP id 21-20020a05600c229500b00401aa8f7562mr1791528wmf.11.1694169288553; Fri, 08 Sep 2023 03:34:48 -0700 (PDT) Received: from omen15.home ([89.131.29.87]) by smtp.gmail.com with ESMTPSA id l40-20020a05600c1d2800b00402f7b50517sm1442102wms.40.2023.09.08.03.34.47 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 08 Sep 2023 03:34:48 -0700 (PDT) From: Jean-Pierre De Jesus DIAZ Date: Fri, 8 Sep 2023 12:34:21 +0200 Message-Id: <20230908103419.21662-2-jean@foundationdevices.com> X-Mailer: git-send-email 2.34.1 In-Reply-To: <20230908103419.21662-1-jean@foundationdevices.com> References: <20230908103419.21662-1-jean@foundationdevices.com> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * gnu/packages/coq.scm (coq-for-coqtaill): New variable. Signed-off-by: Jean-Pierre De Jesus DIAZ --- 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 From unknown Sat Aug 09 01:29:05 2025 X-Loop: help-debbugs@gnu.org Subject: [bug#65820] [PATCH 3/3] gnu: Add vim-coqtail. Resent-From: Jean-Pierre De Jesus DIAZ Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Fri, 08 Sep 2023 10:36:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 65820 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 65820@debbugs.gnu.org Cc: Jean-Pierre De Jesus DIAZ Received: via spool by 65820-submit@debbugs.gnu.org id=B65820.169416932113753 (code B ref 65820); Fri, 08 Sep 2023 10:36:02 +0000 Received: (at 65820) by debbugs.gnu.org; 8 Sep 2023 10:35:21 +0000 Received: from localhost ([127.0.0.1]:42282 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qeYpc-0003Zl-OP for submit@debbugs.gnu.org; Fri, 08 Sep 2023 06:35:21 -0400 Received: from mail-wm1-x32a.google.com ([2a00:1450:4864:20::32a]:45403) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qeYpZ-0003ZU-E8 for 65820@debbugs.gnu.org; Fri, 08 Sep 2023 06:35:18 -0400 Received: by mail-wm1-x32a.google.com with SMTP id 5b1f17b1804b1-40061928e5aso21234015e9.3 for <65820@debbugs.gnu.org>; Fri, 08 Sep 2023 03:35:15 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=foundationdevices.com; s=google; t=1694169309; x=1694774109; darn=debbugs.gnu.org; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:from:to:cc:subject:date :message-id:reply-to; bh=NFGKG0nzc/mz9hYSud8JVtEjb0yH6VvwMoGqjN1m3RU=; b=FvdutfY/rbFOoKNQUkQTNcHwvNxC7rIrFVCjd0vGjjRR6heBSwLSEDX5AHxunHbayZ jc5SwmJYYOHUK+Od/edmkZu5JIgHm9HSlYwC3hDKLH5CAQRdmEGnMtjYlD5BFkAc7CFD jQUHTXt+L6Lole4gG8DhBMBEgmbOWrJ/l33ksP1HRQSi7VjyTK8EuxVAoTkS1i6hTTld KuyKpzoJaL/dfLLia584MjUweLQEXS0czFIinZLhxTAeRb4kfSCvp68oF+gvxdrU+Cmc xVGz8Ck4iJNDp92Bfe+3hwwOHV0J0pRV4MQZ4lR1yRVmgJGlpOAwTNlCR+C9nYGOAurq whMA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1694169309; x=1694774109; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=NFGKG0nzc/mz9hYSud8JVtEjb0yH6VvwMoGqjN1m3RU=; b=JJd1hynJMFs08WNjVVmzgnVIqDRwJqBm4YA5jxc3wYBLrV8R7XFY1t0Czh16Fb1Bzy KQbxBNv+uatYth5OtYHlPVIg/JCMcOhN1ztUaYxHcjAWCgtCPniqtE4s19QJ+CV/txKG rU0hk4fx7Miy3vAYs85XwuXEBj8dT/2QhV9QMsQ1ex8mLkEXtAem/DO0uoEnTpcsDSmC bya1JoRn9Oay+ChOJ6VX76I2RHVhn3SZUsSU7lftvAOzM1Aww0jbQjK1fh+wTk1Phd4Z qgjJ9DTKZIf0P5Z9TUr7WBB/wz5tSjhaJalPSiJo5mCajVm6m5/8V/ga2Oo5iu39gFMj yJdw== X-Gm-Message-State: AOJu0YzQZKf3LPNCoos7prcJs2AEKqz579o4aPFRlHP1xgT2rZfxdq6J 8tRv9i+Dd/mwgYcpiW9MRAMwucmGkZE/TGLr0ojDGw== X-Google-Smtp-Source: AGHT+IF41AWWVzYs16Htz8eC7pNIRKcrx+mh3cIzttD1A4jGuylpqS5K7eC1FqUDDEbJOEQuuIuqDA== X-Received: by 2002:a05:600c:218e:b0:3fe:4e4e:bedb with SMTP id e14-20020a05600c218e00b003fe4e4ebedbmr1772411wme.4.1694169309054; Fri, 08 Sep 2023 03:35:09 -0700 (PDT) Received: from omen15.home ([89.131.29.87]) by smtp.gmail.com with ESMTPSA id l40-20020a05600c1d2800b00402f7b50517sm1442102wms.40.2023.09.08.03.35.08 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 08 Sep 2023 03:35:08 -0700 (PDT) From: Jean-Pierre De Jesus DIAZ Date: Fri, 8 Sep 2023 12:34:23 +0200 Message-Id: <20230908103419.21662-3-jean@foundationdevices.com> X-Mailer: git-send-email 2.34.1 In-Reply-To: <20230908103419.21662-1-jean@foundationdevices.com> References: <20230908103419.21662-1-jean@foundationdevices.com> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) * gnu/packages/vim.scm (vim-coqtail): New variable. Signed-off-by: Jean-Pierre De Jesus DIAZ --- 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 From unknown Sat Aug 09 01:29:05 2025 MIME-Version: 1.0 X-Mailer: MIME-tools 5.505 (Entity 5.505) X-Loop: help-debbugs@gnu.org From: help-debbugs@gnu.org (GNU bug Tracking System) To: Jean-Pierre De Jesus DIAZ Subject: bug#65820: closed (Re: [bug#65820] [PATCH 0/3] gnu: Add vim-coqtail.) Message-ID: References: <87bkbkeozw.fsf@gnu.org> <20230908103223.21492-1-jean@foundationdevices.com> X-Gnu-PR-Message: they-closed 65820 X-Gnu-PR-Package: guix-patches X-Gnu-PR-Keywords: patch Reply-To: 65820@debbugs.gnu.org Date: Thu, 23 Nov 2023 10:36:02 +0000 Content-Type: multipart/mixed; boundary="----------=_1700735762-1501-1" This is a multi-part message in MIME format... ------------=_1700735762-1501-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" Your bug report #65820: [PATCH 0/3] gnu: Add vim-coqtail. which was filed against the guix-patches package, has been closed. The explanation is attached below, along with your original report. If you require more details, please reply to 65820@debbugs.gnu.org. --=20 65820: https://debbugs.gnu.org/cgi/bugreport.cgi?bug=3D65820 GNU Bug Tracking System Contact help-debbugs@gnu.org with problems ------------=_1700735762-1501-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at 65820-done) by debbugs.gnu.org; 23 Nov 2023 10:35:51 +0000 Received: from localhost ([127.0.0.1]:60711 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1r673n-0000Nm-0M for submit@debbugs.gnu.org; Thu, 23 Nov 2023 05:35:51 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:58480) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1r673k-0000NS-KK for 65820-done@debbugs.gnu.org; Thu, 23 Nov 2023 05:35:49 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1r673W-0002XH-96; Thu, 23 Nov 2023 05:35:38 -0500 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=gnu.org; s=fencepost-gnu-org; h=MIME-Version:Date:References:In-Reply-To:Subject:To: From; bh=C3/3hKb7VYcANbBtO6MwsX8pN1L4iUjU4ks2fL5AIso=; b=c5MI42ZNFpqVJK0UB4od jSC7H4EQKKvvViZuMYPW4gxS/S3p8t6eYRSEC8wNVFITRPfN6DZUYlVmYw9y1uLKvLqvIpLzpvwJM 0ga/LvSZdBqSb2BHWjB7vJcKmKVeL6qeoMt6v906HZGgmQSou52q5LQfhNnoTTGN8+klQMrTS/zdG nQPbmQDHUe5+5zjbA7UVLqXPhe0FF4tNUxIxdYG+SBLmJ2QZJmu0fvy2YLZw91qsdO34YPKFCK2Ir OHto/0gktro/YTJpK8fNaapZoPYdV5wgq2OooCVlxdMjSpd7t9xGJBUpRIJyJb7fkmDxdHDwige8a ERQmErJUjA2Sjw==; From: =?utf-8?Q?Ludovic_Court=C3=A8s?= To: Jean-Pierre De Jesus DIAZ Subject: Re: [bug#65820] [PATCH 0/3] gnu: Add vim-coqtail. In-Reply-To: <20230908103223.21492-1-jean@foundationdevices.com> (Jean-Pierre De Jesus DIAZ's message of "Fri, 8 Sep 2023 12:32:24 +0200") References: <20230908103223.21492-1-jean@foundationdevices.com> Date: Thu, 23 Nov 2023 11:35:31 +0100 Message-ID: <87bkbkeozw.fsf@gnu.org> User-Agent: Gnus/5.13 (Gnus v5.13) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 65820-done Cc: 65820-done@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -3.3 (---) Hello, Jean-Pierre De Jesus DIAZ 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=E2=80=99. ------------=_1700735762-1501-1 Content-Type: message/rfc822 Content-Disposition: inline Content-Transfer-Encoding: 7bit Received: (at submit) by debbugs.gnu.org; 8 Sep 2023 10:33:00 +0000 Received: from localhost ([127.0.0.1]:42269 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qeYnM-0003Uw-E8 for submit@debbugs.gnu.org; Fri, 08 Sep 2023 06:33:00 -0400 Received: from lists.gnu.org ([2001:470:142::17]:41602) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qeYnI-0003Uf-6z for submit@debbugs.gnu.org; Fri, 08 Sep 2023 06:32:59 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1qeYn8-0003mn-QH for guix-patches@gnu.org; Fri, 08 Sep 2023 06:32:46 -0400 Received: from mail-wm1-x333.google.com ([2a00:1450:4864:20::333]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1qeYn6-0008FA-CN for guix-patches@gnu.org; Fri, 08 Sep 2023 06:32:46 -0400 Received: by mail-wm1-x333.google.com with SMTP id 5b1f17b1804b1-3ff1c397405so22072915e9.3 for ; Fri, 08 Sep 2023 03:32:42 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=foundationdevices.com; s=google; t=1694169161; x=1694773961; darn=gnu.org; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=4Cj9HIlwSZI/Dztr8jTULucaKPGjaYJauIORD1XWajI=; b=KurHMPutxuELWc5+a9Q8jW5ZSGkBVEZpkL/EXtgzanBMEocTBJl5XiCGYcM0AUjyyX j7Crf8N8hSK+cxNDiLIPT1WblRSfkZMEVeicbgkErcR+HaSa9LmqStMTA5lapBxDy8hb JqifxM3UOOxx6UXMtADNLKWT14CVcCUnvUtTTRpFzejxUQMA29cNo2h8rCNaJuqCgfAs 8F1aBquXk1v7OIWQKUWxaeGAqa73Q6XZ4TNXVbZpwsLNF3SQlRmZWxuAFFV7w9Mn3nQZ lGf9Tn8r8qHRtoKCZtMShqFDt1JjOu1tPcGl8f3/je+zOdaYkwJuIQql8UE7PpESWPCS UUqA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1694169161; x=1694773961; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=4Cj9HIlwSZI/Dztr8jTULucaKPGjaYJauIORD1XWajI=; b=tVuk0xShSBoFFvDbGrRFw4A8i+iQuHjFD8fImvr6ztWQeOTGf8GkrGMyAFXVk+TuzG w2roICXmE5MdZXsadApmcOuGhVbcSQR8omITOCzMT/f7yCO/RNgXcQqkBhwRTHIT308n K6iFWJ+vaesj+nczAlQIFb2U1qLKEy8RnMARQWJl8ObZPPlLPEeXJ2rELQHhbmkFZ6qO 102Xr9XJ54lKCkoHjZBb38LivHy+XqSaF8LkQSx/coO5HD2fgqRvfI/WUXQsPSx8fuWr UM0Qco6CvhV2VwF0RnVaxyX63mbVvBUKVEEwdGMOKbPSXPyX1Dg0Pmxbl0ggbQEPAEdN YMsQ== X-Gm-Message-State: AOJu0YwQguZBQ29IMmRq6PkezBiQqvZr2R0hqhO73fWGm1Y0Ow/oTuJm LCl7w47HVAkv2z6zqcXUv2E0GoJlcXCwVhf+CAphiw== X-Google-Smtp-Source: AGHT+IGbTTHceqrZgvj34ykBvKdWh964Lb2Rioj3ye3CocwtbHcQ53DP20yizhgorW2UyTIxXqiDyA== X-Received: by 2002:a7b:c445:0:b0:3fe:18a3:b3c with SMTP id l5-20020a7bc445000000b003fe18a30b3cmr1781049wmi.12.1694169161233; Fri, 08 Sep 2023 03:32:41 -0700 (PDT) Received: from omen15.home ([89.131.29.87]) by smtp.gmail.com with ESMTPSA id h5-20020adffd45000000b0031c5d74ecd8sm1746126wrs.84.2023.09.08.03.32.40 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 08 Sep 2023 03:32:40 -0700 (PDT) From: Jean-Pierre De Jesus DIAZ To: guix-patches@gnu.org Subject: [PATCH 0/3] gnu: Add vim-coqtail. Date: Fri, 8 Sep 2023 12:32:24 +0200 Message-Id: <20230908103223.21492-1-jean@foundationdevices.com> X-Mailer: git-send-email 2.34.1 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit Received-SPF: pass client-ip=2a00:1450:4864:20::333; envelope-from=jean@foundationdevices.com; helo=mail-wm1-x333.google.com X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: 1.0 (+) X-Debbugs-Envelope-To: submit Cc: Jean-Pierre De Jesus DIAZ X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.0 (/) 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 ------------=_1700735762-1501-1--