From patchwork Sun Mar 29 10:06:34 2020 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: John Soo X-Patchwork-Id: 20941 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 8ECB627BBE4; Mon, 30 Mar 2020 03:37:15 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-2.8 required=5.0 tests=BAYES_00,DKIM_SIGNED, MAILING_LIST_MULTI,T_DKIM_INVALID,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.2 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id 06FD427BBEA for ; Mon, 30 Mar 2020 03:37:14 +0100 (BST) Received: from localhost ([::1]:43730 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1jIkIb-0005E6-Fm for patchwork@mira.cbaines.net; Sun, 29 Mar 2020 22:37:13 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:54751) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1jIkHk-0003Kc-0M for guix-patches@gnu.org; Sun, 29 Mar 2020 22:36:21 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1jIkHi-0003P1-D3 for guix-patches@gnu.org; Sun, 29 Mar 2020 22:36:19 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:48619) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1jIkHi-0003Ok-7A for guix-patches@gnu.org; Sun, 29 Mar 2020 22:36:18 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1jIkHi-0004fH-3n for guix-patches@gnu.org; Sun, 29 Mar 2020 22:36:18 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#40311] [PATCH] Update proof-general Resent-From: John Soo Resent-CC: guix-patches@gnu.org Resent-Date: Mon, 30 Mar 2020 02:36:17 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 40311 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 40311@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.158553573617460 (code B ref -1); Mon, 30 Mar 2020 02:36:17 +0000 Received: (at submit) by debbugs.gnu.org; 30 Mar 2020 02:35:36 +0000 Received: from lists.gnu.org ([209.51.188.17]:53884) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1jIUq4-0001NQ-3g for submit@debbugs.gnu.org; Sun, 29 Mar 2020 06:06:45 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:38143) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1jIUq2-00012D-GB for guix-patches@gnu.org; Sun, 29 Mar 2020 06:06:44 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1jIUq0-0000fH-1x for guix-patches@gnu.org; Sun, 29 Mar 2020 06:06:41 -0400 Received: from mail-pf1-x42f.google.com ([2607:f8b0:4864:20::42f]:38512) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1jIUpz-0000bQ-Id for guix-patches@gnu.org; Sun, 29 Mar 2020 06:06:40 -0400 Received: by mail-pf1-x42f.google.com with SMTP id c21so6405701pfo.5 for ; Sun, 29 Mar 2020 03:06:38 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=asu-edu.20150623.gappssmtp.com; s=20150623; h=from:to:subject:date:message-id:mime-version; bh=2yqpkx0T0CLoJrMOpXqUpU8yIbRUo3AqdLJmRN9f5Iw=; b=wWOjrKVi+nRdKUIHRXooTiTPpWom1VExbbr0zEPWvotw2CzjcjxLzYXDWC89lEOKl3 f7Jpc34YnowfrR1hcvIicLLlL583fKzX7iqkjr8+rXLjTsvgGQ8AhWfaz+6aAe85G3dH LsdP+cXh+pEagEqQ7FhyNHOZaIWAjW6u6TNN4Z3O/iVqY1gcdw4WWd1x3r9M5r/fP5T0 aum8saYm4sDABdNQsmNgPL1hW1HcgyxA2o5oktWYTEFroAf79fimRtRpbKzFYokUCZBQ zvbYtGX4lM1anGuBDRUbTk55xXpdxXPQWSd7/uY+JUsFO5Vg/ioTzYpLnNIVQkGykWZZ IfJA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:subject:date:message-id:mime-version; bh=2yqpkx0T0CLoJrMOpXqUpU8yIbRUo3AqdLJmRN9f5Iw=; b=aKS/35mCdMooktsYxYIZnSX0brZUhyV4qnRDXTLbRct2AprRtGsHNdzQjb7HZndi9k tJKYujymHWqbQUlEx7RjrMtYLq6g1CyTZCKhdOrBdbQk3dFxotIg8kT9OpHK+JbWfqBj Y+nZ/pTTy10DIPEw0zDbqNyxuUeaH7+tuzoTzYRjKvaW4qj7N7H0HMo7+unHtCcI/NhQ o6S9fUFOftN9t8ybkuCbdUqnxECejGO94Ip9dpncALRtBs4eswJK1eUTTTDXI/iGyeRb 03zdGZmQyI0orclxerRbXN681m9ccY1SUY5pWELNj54rbSFEb51P5s0prA7dygYMfSAW hBqw== X-Gm-Message-State: ANhLgQ1uoVU4L9kc3owHUrDw/IpwYOL00appNWDJ72DMPGn/X1ncU6o/ 61ROuoU1LYliSR+5scytfYjRUfoCt+I= X-Google-Smtp-Source: ADFU+vsJXrjo+iR5XCpwwOtyxCyCFdiN/0RYEedAojsbVmeQab5WgnI2TUjKmaotfTIKpzzXdvstJA== X-Received: by 2002:a62:1946:: with SMTP id 67mr8182932pfz.0.1585476397160; Sun, 29 Mar 2020 03:06:37 -0700 (PDT) Received: from ecenter ([2600:1700:83b0:8bd0::6c3]) by smtp.gmail.com with ESMTPSA id j65sm7465615pgc.16.2020.03.29.03.06.36 for (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Sun, 29 Mar 2020 03:06:36 -0700 (PDT) From: John Soo Date: Sun, 29 Mar 2020 03:06:34 -0700 Message-ID: <87iminpj9x.fsf@asu.edu> MIME-Version: 1.0 X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-List-Received-Date: Sun, 29 Mar 2020 10:06:45 -0000 X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches Hi Guix, In my effort to use strictly guix for my emacs package management, I found that proof-general was not working out of the box with guix.el. In the end I could not figure out how to make it work, but I did update proof-general to 4.4 and updated the home-page. proof-general puts its initialization file in %outputs/share/emacs/site-lisp/site-start.d/pg-init.el. I also see Tuareg puts the file there. Niether that path, nor any subdirectory of site-lisp is included by $EMACSLOADPATH or is autoloaded by guix.el. For the record, I added (load-file "~/.guix-profile/share/emacs/site-lisp/site-start.d/pg-init.el") to init.el as a workaround. Anyways, this should fix proof-general to work with the current version of coq at least and add some more newer niceties in recent versions. Thanks, as always! John >From bc79d139873c9a831f373dc7e92dacd96a80fecb Mon Sep 17 00:00:00 2001 From: John Soo Date: Sun, 29 Mar 2020 02:26:46 -0700 Subject: [PATCH 2/2] gnu: proof-general: Update home-page. * gnu/packages/coq.scm (proof-general):[home-page] update to proofgeneral.github.io --- gnu/packages/coq.scm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index 937e2cc20a..2a7fae2a74 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -196,7 +196,7 @@ It is developed using Objective Caml and Camlp5.") (substitute* "Makefile" ((" [^ ]*\\.pdf") "")) (apply invoke "make" "install-doc" make-flags)))))) - (home-page "http://proofgeneral.inf.ed.ac.uk/") + (home-page "https://proofgeneral.github.io/ ") (synopsis "Generic front-end for proof assistants based on Emacs") (description "Proof General is a major mode to turn Emacs into an interactive proof -- 2.26.0