From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp1 ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id kN5vOoknw2ClXwAAgWs5BA (envelope-from ) for ; Fri, 11 Jun 2021 11:06:17 +0200 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp1 with LMTPS id EJ+iNYknw2DsUQAAbx9fmQ (envelope-from ) for ; Fri, 11 Jun 2021 09:06:17 +0000 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 6DD7713A7B for ; Fri, 11 Jun 2021 11:06:17 +0200 (CEST) Received: from localhost ([::1]:52438 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1lrd7I-0003Pm-8g for larch@yhetil.org; Fri, 11 Jun 2021 05:06:16 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:40916) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1lrd74-0003Mj-EI for guix-patches@gnu.org; Fri, 11 Jun 2021 05:06:02 -0400 Received: from debbugs.gnu.org ([209.51.188.43]:54820) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1lrd74-0006TS-5Y for guix-patches@gnu.org; Fri, 11 Jun 2021 05:06:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1lrd73-0003f1-U6 for guix-patches@gnu.org; Fri, 11 Jun 2021 05:06:01 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#48947] [PATCH] gnu: proof-general: Update to 4.4-0.bc86736. Resent-From: Xinglu Chen Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Fri, 11 Jun 2021 09:06:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 48947 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: zimoun Cc: 48947@debbugs.gnu.org Received: via spool by 48947-submit@debbugs.gnu.org id=B48947.162340233514037 (code B ref 48947); Fri, 11 Jun 2021 09:06:01 +0000 Received: (at 48947) by debbugs.gnu.org; 11 Jun 2021 09:05:35 +0000 Received: from localhost ([127.0.0.1]:38133 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lrd6c-0003eK-UH for submit@debbugs.gnu.org; Fri, 11 Jun 2021 05:05:35 -0400 Received: from h87-96-130-155.cust.a3fiber.se ([87.96.130.155]:59116 helo=mail.yoctocell.xyz) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1lrd6Z-0003e3-73 for 48947@debbugs.gnu.org; Fri, 11 Jun 2021 05:05:33 -0400 From: Xinglu Chen DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=yoctocell.xyz; s=mail; t=1623402323; bh=JORdAIrE6GH2Be8Ee2beXr0DI1FzfJH1awUnE2MAqEA=; h=From:To:Cc:Subject:In-Reply-To:References:Date; b=UCGAfbXbBoCMIUHH56ex2liiO0nOe/yC1AOJOfP7YNKpy7EHFdiRNksY51drOdTsC 0IOJ34h1T+IalmZnbC7ytgIymEftYhWvUi2LbwxVq0lWkCMWKBQ/WRLpblAtbmD51E 8ZgU5byqv+fUj9Gqtz6dGTW+KisVi71F27Mxad4A= In-Reply-To: References: <287f5f7500552106833f349c1f9493ab89470b39.1623331764.git.public@yoctocell.xyz> Date: Fri, 11 Jun 2021 11:05:02 +0200 Message-ID: <87pmwsbwld.fsf@yoctocell.xyz> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha256; protocol="application/pgp-signature" X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: "Guix-patches" X-Migadu-Flow: FLOW_IN ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1623402377; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type:resent-cc:resent-from:resent-sender: resent-message-id:in-reply-to:in-reply-to:references:references: list-id:list-help:list-unsubscribe:list-subscribe:list-post: dkim-signature; bh=rrFlfb/yAKM4MxframkUHCH+EXMK3fV38ESD0yQ0XEs=; b=hxwn6E2aR0+NHChV0Pnu+kZY8CpqHTvjymphb8QE4SFTOi8IX7IIQRNbz3FuLp+L2u7mA5 BT2B0YtdTDmVPrZqJMfRgBdHbQJUTLTuxmmXkMHtJqREzoiOjqah0xP4hfTsRmV+C0Kr6w /aZ6UgmoXXKsOL0GvrL35AqNo2giXnI/wD/hz3yp95+KG3xdIxNapkb1YFL4Ru51NOKReD NGwqKu5GvVFLJUy4rn+w4aj32XjfrsCjK8fPLe3rHvv8wijrJDzjNoApf0SvY9Gmmc++mr NmBrBe/QVZHbQ4QwQosL9FKCFipmrGxWI13Wg4PkE7YD+E2Nx8ZyZJCb1uM6PA== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1623402377; a=rsa-sha256; cv=none; b=sT6AMh9yxkF/h6VWo56aHh/hkHK6982TewiXWfLsCf3VF7QOJDLwflMTAQ5w0RzJXz6Ruv 6kzay1qcdXYsJyc2Ztx0Re511XPl8OIvaqsBN9dd9CZxUfCKrSjgDz9HYQjcweDmuYGcRw QXIiEkDH91ZLOHGMHu7T0KcaGL/rHYpSZOWzvC2YAAuaPR0IimvMxSl/P1MtqFZ1rxhz/b ZXvCVQay6RkflHykLa1UxRQbni2cOuvHOTNo8G+RJWWQtCziidaj/qXZNY2Z5jibKHjZLR Tl86nuYRQ62JDWxj3rXCr9gZQUCbxCumzJfDyEmsXtTYKiQFsn3f/4c4XPWO0A== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=yoctocell.xyz header.s=mail header.b=UCGAfbXb; dmarc=fail reason="SPF not aligned (relaxed)" header.from=yoctocell.xyz (policy=none); spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Spam-Score: -3.42 Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=yoctocell.xyz header.s=mail header.b=UCGAfbXb; dmarc=fail reason="SPF not aligned (relaxed)" header.from=yoctocell.xyz (policy=none); spf=pass (aspmx1.migadu.com: domain of guix-patches-bounces@gnu.org designates 209.51.188.17 as permitted sender) smtp.mailfrom=guix-patches-bounces@gnu.org X-Migadu-Queue-Id: 6DD7713A7B X-Spam-Score: -3.42 X-Migadu-Scanner: scn0.migadu.com X-TUID: /4d1umkz8EKE --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable On Thu, Jun 10 2021, zimoun wrote: > Hi, > > On Thu, 10 Jun 2021 at 15:31, Xinglu Chen wrote: >> >> There hasn=E2=80=99t been a new release since 2016 and there has been mo= re than 450 >> new commits since then. > > Cool! > > Does this patch fix the bug#46016? > > I didn=E2=80=99t know about this bug report, but I did notice that Emacs wa= sn=E2=80=99t able to load the Elisp files (M-x coq-mode didn=E2=80=99t work). Proof General generates a pg-init.el file in /path/to/guix-profile/share/emacs/site-lisp/ProofGeneral/site-start.d, Emacs isn=E2=80=99t able to find that file, so doing (require 'proof-site) doesn=E2=80=99t work. Relevant part of the Makefile =2D-8<---------------cut here---------------start------------->8--- ELISPP=3Dshare/${EMACS}/site-lisp/ProofGeneral ELISP_START=3D${PREFIX}/share/${EMACS}/site-lisp/site-start.d [...] install-init: mkdir -p ${ELISP_START} echo ';;; pg-init.el --- setup for Proof General' > ${ELISP_START}/pg-init= .el echo "(setq load-path (append load-path '(\"${DEST_ELISP}/generic\")))" >>= ${ELISP_START}/pg-init.el echo "(require 'proof-site)" >> ${ELISP_START}/pg-init.el =2D-8<---------------cut here---------------end--------------->8--- With this patch, I set the ELISP_START variable to the same value os ELISPP, now the pg-init.el file ends up in the ProofGeneral directory, and Emacs is now able to find it. Doing (require 'proof-site) worked, and M-x coq-mode created a splash screen, so it seems to work (I just starting looking into Coq). --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQJJBAEBCAAzFiEEAVhh4yyK5+SEykIzrPUJmaL7XHkFAmDDJz4VHHB1YmxpY0B5 b2N0b2NlbGwueHl6AAoJEKz1CZmi+1x5ThsP/inqkyFcjhjKnOpf+l2XQ7hKmUfM 42jvKCIcnlHsxpK0zpsc+aTIX/1o9XFDoBkPfvISG65GqAujiiJgI++pVHH5ebfD pX42arbu785xD024XWdKIcR5mNG45Ct/wotRDiQuMUkgzmnWyA8KD+jLB7wqRha4 KLt+IUKzHmc6k1qG1JNiPM+knQ6LYs08kRIWwXDK+sIa19A3oUNGBPGF3KVW1Dyr j1y8RGJaFzV6kRFj8yzkmCbRD24MXSJGX9qdbbi4lNAgXIOpcctGU2keUCGtsl9G ZAUdU0eqca8gNHfactPX25tEFrSHrsEp02dMmG4ZYX1v3psO0r28iOCrRTTNCHVv qUWQlPYVHre6XGLvwlSAi0e5KV/0SAIewsdNcVr/k4ZTfJ4BipJZmSQqETibMlhC AgygFXzsgFUtaPtGw0HbzGbu9PWgLgRyuuFPEhx7i2KfPYU4jyXKIvWTX+fJ2wtQ i8c9Us65a6MKPPkFNrQhdEGPJUU6/PTjCfHGVNL1iFoWgJ5OE/W6GTgcuFeT0rei WFcxFGqiPBuktEwphpYPajh5jnBQnnnJ/iROXggarHMoC7yRbzE70HP90fXplAXZ M0qcuvG2MIJZl1QmdYG1YNVY65w3WebXU/SOusSt99DyItx+3eQjlL+SRX2+fDZG DQtILkOvyAHi2qiG =Gf/G -----END PGP SIGNATURE----- --=-=-=--