From debbugs-submit-bounces@debbugs.gnu.org Sat Dec 28 17:41:45 2019 Received: (at submit) by debbugs.gnu.org; 28 Dec 2019 22:41:45 +0000 Received: from localhost ([127.0.0.1]:59057 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ilKmH-0004lN-Du for submit@debbugs.gnu.org; Sat, 28 Dec 2019 17:41:45 -0500 Received: from lists.gnu.org ([209.51.188.17]:33471) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ilKmF-0004lF-P1 for submit@debbugs.gnu.org; Sat, 28 Dec 2019 17:41:44 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]:42402) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1ilKmE-0007Y7-Lz for guix-patches@gnu.org; Sat, 28 Dec 2019 17:41:43 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=-2.9 required=5.0 tests=ALL_TRUSTED,BAYES_00, URIBL_BLOCKED autolearn=disabled version=3.3.2 Received: from fencepost.gnu.org ([2001:470:142:3::e]:39242) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ilKmE-00039M-Hh for guix-patches@gnu.org; Sat, 28 Dec 2019 17:41:42 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48406 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ilKmD-0004MZ-Bl for guix-patches@gnu.org; Sat, 28 Dec 2019 17:41:42 -0500 From: Brett Gilio To: guix-patches@gnu.org Subject: [WIP 0/1] Add emacs-company-coq. Date: Sat, 28 Dec 2019 16:41:33 -0600 Message-ID: <87mubchy3m.fsf@gnu.org> MIME-Version: 1.0 Content-Type: text/x-patch Content-Disposition: inline; filename=0000-cover-letter.patch Content-Description: [WIP 0/1] Add emacs-company-coq. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: submit 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 (---) >From 944029c25a80505aaa5f19928e4911360d8505de Mon Sep 17 00:00:00 2001 From: Brett Gilio Date: Sat, 28 Dec 2019 16:39:14 -0600 Subject: [WIP 0/1] Add emacs-company-coq. To: guix-patches@gnu.org This is a WIP patch for adding emacs-company-coq. There is still more that needs to be done before this package is ready to be pushed to master. Such as getting the Coq-based test suite to run, ensuring that all of the cases usually covered by CASK are being covered by Guix, and getting the REFMAN to install properly. Brett Gilio (1): gnu: Add emacs-company-coq. gnu/packages/emacs-xyz.scm | 75 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) -- 2.24.1 From debbugs-submit-bounces@debbugs.gnu.org Sat Dec 28 17:43:16 2019 Received: (at 38784) by debbugs.gnu.org; 28 Dec 2019 22:43:16 +0000 Received: from localhost ([127.0.0.1]:59062 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ilKnj-0004oF-Rf for submit@debbugs.gnu.org; Sat, 28 Dec 2019 17:43:16 -0500 Received: from eggs.gnu.org ([209.51.188.92]:37455) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1ilKni-0004o2-2A for 38784@debbugs.gnu.org; Sat, 28 Dec 2019 17:43:14 -0500 Received: from fencepost.gnu.org ([2001:470:142:3::e]:39253) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1ilKnc-0001zk-Pa for 38784@debbugs.gnu.org; Sat, 28 Dec 2019 17:43:08 -0500 Received: from [2605:6000:1a0d:4c95::3d] (port=48410 helo=oryx) by fencepost.gnu.org with esmtpsa (TLS1.2:RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1ilKna-0004Qm-V0 for 38784@debbugs.gnu.org; Sat, 28 Dec 2019 17:43:08 -0500 From: Brett Gilio To: 38784@debbugs.gnu.org Subject: [WIP 1/1] gnu: Add emacs-company-coq. Date: Sat, 28 Dec 2019 16:43:15 -0600 Message-ID: <87imm0hy0s.fsf@gnu.org> MIME-Version: 1.0 Content-Type: text/x-patch Content-Disposition: inline; filename=0001-gnu-Add-emacs-company-coq.patch Content-Description: [WIP 1/1] gnu: Add emacs-company-coq. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Spam-Score: -2.3 (--) X-Debbugs-Envelope-To: 38784 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 (---) >From 944029c25a80505aaa5f19928e4911360d8505de Mon Sep 17 00:00:00 2001 From: Brett Gilio Date: Sat, 28 Dec 2019 16:38:24 -0600 Subject: [WIP 1/1] gnu: Add emacs-company-coq. To: guix-patches@gnu.org * gnu/packages/emacs-xyz.scm (emacs-company-coq): New variable. --- gnu/packages/emacs-xyz.scm | 75 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) diff --git a/gnu/packages/emacs-xyz.scm b/gnu/packages/emacs-xyz.scm index 06c8dc2016..b746e5a20a 100644 --- a/gnu/packages/emacs-xyz.scm +++ b/gnu/packages/emacs-xyz.scm @@ -92,6 +92,7 @@ #:use-module (gnu packages bash) #:use-module (gnu packages cmake) #:use-module (gnu packages code) + #:use-module (gnu packages coq) #:use-module (gnu packages cpp) #:use-module (gnu packages curl) #:use-module (gnu packages databases) @@ -20654,3 +20655,77 @@ buffer. It can be used to toggle an alternative mode-line, toggle its visibilit or simply disable the mode-line in buffers where it is not very useful.") (home-page "https://github.com/hlissner/emacs-hide-mode-line") (license license:expat))) + +(define-public emacs-company-coq + (let ((commit "6e8bc2e367e8184079b7f4b4ab359b64ab884d7c") + (revision "1") + (version "1.0.1")) + (package + (name "emacs-company-coq") + (version (git-version version revision commit)) + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/cpitclaudel/company-coq.git") + (commit commit))) + (sha256 + (base32 + "192vvz77yik0lx2g4yfjwx2himzzq4zhrc9mlyhdpwsmzwx7bf4r")) + (file-name (git-file-name name version)))) + (build-system emacs-build-system) + (arguments + `(;; NOTE: By default this package leverages CASK. We do not need + ;; this. Instead, we will leverage Guix to handle installation + ;; for us. + ;; FIXME: REFMAN needs to be installed properly. + #:phases + (modify-phases %standard-phases + (add-after 'unpack 'move-el + (lambda _ + (for-each (lambda (f) + (rename-file f (basename f))) + (find-files "./etc" ".*\\.el$")) + (for-each (lambda (f) + (rename-file f (basename f))) + (find-files "./experiments" ".*\\.el$")) + #t)) + (add-after 'move-el 'patch-proof-general + (lambda* (#:key inputs #:allow-other-keys) + ;; Patch and load required components for proof-general. + (let* ((generic "/share/emacs/site-lisp/ProofGeneral/generic") + (proof-site (string-append + (assoc-ref inputs "proof-general") + (string-append generic "/proof-site.el"))) + (proof-shell (string-append + (assoc-ref inputs "proof-general") + (string-append generic "/proof-shell.el")))) + (substitute* "rebuild-screenshots.el" + (("\\(require 'proof-site\\)") + (string-append + "(load-file \"" proof-site "\")"))) + (substitute* "company-coq.el" + (("\\(require 'proof-site\\ nil t)") + (string-append + "(load-file \"" proof-site "\")"))) + (substitute* "company-coq-trace.el" + (("\\(require 'proof-shell\\)") + (string-append + "(load-file \"" proof-shell "\")"))) + #t)))))) + (propagated-inputs + `(("emacs-company-math" ,emacs-company-math) + ("emacs-company" ,emacs-company) + ("emacs-yasnippet" ,emacs-yasnippet) + ("emacs-dash" ,emacs-dash) + ("emacs-noflet" ,emacs-noflet))) + (native-inputs + `(("python" ,python) + ("proof-general" ,proof-general))) + (home-page "https://github.com/cpitclaudel/company-coq") + (synopsis + "Collection of extensions for Proof General's Coq mode") + (description + "This package includes a collection of company-mode backends for +Proof-General's Coq mode, and many useful extensions to Proof-General.") + (license license:gpl3+)))) -- 2.24.1 From debbugs-submit-bounces@debbugs.gnu.org Tue Apr 12 06:46:15 2022 Received: (at 38784-done) by debbugs.gnu.org; 12 Apr 2022 10:46:15 +0000 Received: from localhost ([127.0.0.1]:47722 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1neE2J-0002ad-2g for submit@debbugs.gnu.org; Tue, 12 Apr 2022 06:46:15 -0400 Received: from mail-wr1-f52.google.com ([209.85.221.52]:46671) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1neE24-0002Za-9s for 38784-done@debbugs.gnu.org; Tue, 12 Apr 2022 06:46:00 -0400 Received: by mail-wr1-f52.google.com with SMTP id i20so13985270wrb.13 for <38784-done@debbugs.gnu.org>; Tue, 12 Apr 2022 03:46:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=from:to:cc:subject:references:date:in-reply-to:message-id :user-agent:mime-version; bh=UXKdA/6+Kv0Kv3MM+E+1oVtYOqAzBDElePBMhF6EsHw=; b=qnmw7Sp7/nsAPflJ3BjDDlOsQal491GIhwI55d/pff1NdsiO3bUeXhuFDSg8A+KHkW RZOdLBn2OyEz3yT7TJ/4Qg0n0GNYZw7yNEJFkrofxpTsP69rUciOY7MuJleEwrDJ7tJY glerYCK6Y1JMYt3qlgJygF3/2KK9yQwoC6Hh1u/Vs3gcg4YdVILM2Unbma3fq7Q8JPfK QRDIYkqJGKz4Gbg5FMY6YK1j+uiO+Q1VEwRrIu7RZaTrvs4JicGugxpZwtL+ARH3SLER RJf21GPvjWgzGx3Z+TgjE04phnWwqanAa6/QMayzvCiKghzrSDgPUliyhVoSVtHDSNVw dwyw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to :message-id:user-agent:mime-version; bh=UXKdA/6+Kv0Kv3MM+E+1oVtYOqAzBDElePBMhF6EsHw=; b=voGXpTVuOttyrLJacHMS3FRVB6eoj8i7H3yeEcnteRtzm5IJ1OudEtQNC9HYsFWcdt q9fBl0WlEj05W6yp/gcdBZo87a4/dO+ARRoWh8PtvB5jFqBJa9PJnODgSfsb0XGV2eyZ GVIJYT5UMRTmsyiB63JRtygw1DuA0RVa6osouz3SpXg/WXIVu7Q6iVKt6TWE0nY7h/vN 71y8WfP8hAsEtkm60rznMGdjHXRnQHLkWHRJjv+rlPV2U+HNZFLObPc3rgQ13FfCtXwQ ZH4y2kSTnCdH4zZX4ZLdSFlpVsbjlBuG1PURPVox2YMDGb2pAZRzf60Khb8WkkEPH8Wo quCA== X-Gm-Message-State: AOAM530+ZRfKZElSF3Witjf2PCOH4oxVQvcwdb1s6b4+nMfi89rXOFEY cARRt+oeBpGpErAmFcdsQliXig0GZ5w= X-Google-Smtp-Source: ABdhPJztJG2PKRukge3nNZkBUfXtIZY51bTd4/cWc4B1wgQy1CLQmKmiJ3ECzKdSFbI/7cllyazhzQ== X-Received: by 2002:a05:6000:1844:b0:207:9807:bc71 with SMTP id c4-20020a056000184400b002079807bc71mr16513150wri.551.1649760354634; Tue, 12 Apr 2022 03:45:54 -0700 (PDT) Received: from lili (roam-nat-fw-prg-194-254-61-46.net.univ-paris-diderot.fr. [194.254.61.46]) by smtp.gmail.com with ESMTPSA id w4-20020a7bc104000000b0038eba17a797sm1974713wmi.31.2022.04.12.03.45.54 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 12 Apr 2022 03:45:54 -0700 (PDT) From: zimoun To: Brett Gilio Subject: Re: bug#38784: [WIP 0/1] Add emacs-company-coq. References: <87mubchy3m.fsf@gnu.org> <87imm0hy0s.fsf@gnu.org> Date: Tue, 12 Apr 2022 12:45:34 +0200 In-Reply-To: <87imm0hy0s.fsf@gnu.org> (Brett Gilio's message of "Sat, 28 Dec 2019 16:43:15 -0600") Message-ID: <861qy237ht.fsf_-_@gmail.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/27.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 38784-done Cc: 38784-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: -1.0 (-) Hi, Thanks for your submission. On Sat, 28 Dec 2019 at 16:43, Brett Gilio wrote: > * gnu/packages/emacs-xyz.scm (emacs-company-coq): New variable. > --- > gnu/packages/emacs-xyz.scm | 75 ++++++++++++++++++++++++++++++++++++++ > 1 file changed, 75 insertions(+) [...] > +(define-public emacs-company-coq > + (let ((commit "6e8bc2e367e8184079b7f4b4ab359b64ab884d7c") > + (revision "1") > + (version "1.0.1")) > + (package > + (name "emacs-company-coq") [...] > + (license license:gpl3+)))) --8<---------------cut here---------------start------------->8--- f931d46ce3e342f53dee926d3cff70b081f58e5f Author: John Soo AuthorDate: Mon Mar 30 14:36:38 2020 +0200 Commit: Nicolas Goaziou CommitDate: Mon Mar 30 14:37:41 2020 +0200 gnu: Add emacs-company-coq. * gnu/packages/emacs-xyz.scm (emacs-company-coq): New variable. 1 file changed, 37 insertions(+) gnu/packages/emacs-xyz.scm | 37 +++++++++++++++++++++++++++++++++++++ --8<---------------cut here---------------end--------------->8--- Therefore, closing! Cheers, simon From unknown Tue Aug 19 21:03:31 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Tue, 10 May 2022 11:24:09 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator