From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp11.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id 0ErOAqsU2WFlqAAAgWs5BA (envelope-from ) for ; Sat, 08 Jan 2022 05:35:55 +0100 Received: from aspmx1.migadu.com ([2001:41d0:8:6d80::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp11.migadu.com with LMTPS id aJQcAKsU2WEUigAA9RJhRA (envelope-from ) for ; Sat, 08 Jan 2022 05:35:55 +0100 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 C278F2F8C3 for ; Sat, 8 Jan 2022 05:35:54 +0100 (CET) Received: from localhost ([::1]:37264 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1n63SL-0004Qp-Qj for larch@yhetil.org; Fri, 07 Jan 2022 23:35:53 -0500 Received: from eggs.gnu.org ([209.51.188.92]:56422) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1n5roU-0001Ez-12 for emacs-orgmode@gnu.org; Fri, 07 Jan 2022 11:09:59 -0500 Received: from tilde.club ([142.44.150.184]:43422) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1n5roN-0001Jt-40 for emacs-orgmode@gnu.org; Fri, 07 Jan 2022 11:09:57 -0500 Received: by tilde.club (Postfix, from userid 4408) id E2176222546F5; Fri, 7 Jan 2022 16:09:45 +0000 (UTC) DKIM-Filter: OpenDKIM Filter v2.11.0 tilde.club E2176222546F5 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=tilde.club; s=mail; t=1641571785; bh=lO8lh4xQRy/Zk0UKhVb0sub+H76TdxJyEkbY/+bxEcs=; h=Date:From:To:Subject:From; b=R8LYdDDVp2usdRUuF3VgyPGIh4ROEhXUpXyc+r2q97aufkZXrQhk2alBg7NqpVp7p C4o1I7CPfTA3IhHAv81dF6Vco02bFaEmeypklHbwkQU9EtTHb1WI1w+zQ+dqm5Atq4 9anN6Bf3ZKo8RfBjN5qrpVIopiB78HNCurR3mpgQ= Received: from localhost (localhost [127.0.0.1]) by tilde.club (Postfix) with ESMTP id E09F9228AF0E9 for ; Fri, 7 Jan 2022 16:09:45 +0000 (UTC) Date: Fri, 7 Jan 2022 16:09:45 +0000 (UTC) From: aby@tilde.club To: emacs-orgmode@gnu.org Subject: coq related error when exporting to latex. Message-ID: MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="747550870-292115932-1641571785=:3100149" Received-SPF: pass client-ip=142.44.150.184; envelope-from=aby@tilde.club; helo=tilde.club 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, SPF_HELO_PASS=-0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-Mailman-Approved-At: Fri, 07 Jan 2022 23:34:52 -0500 X-BeenThere: emacs-orgmode@gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: "General discussions about Org-mode." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: emacs-orgmode-bounces+larch=yhetil.org@gnu.org Sender: "Emacs-orgmode" X-Migadu-Flow: FLOW_IN X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1641616554; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:mime-version:mime-version: content-type:content-type:list-id:list-help:list-unsubscribe: list-subscribe:list-post:dkim-signature; bh=UIBq6VcD6EGK/pCCXkc9PxLIMPjFwBLBeKSrf29Gnmo=; b=UOxjwIC9M9lNuNXkc4pWCx/+3z+9f725tmzA/GK9/tL2fj7DTdhofnMAjfsD2w7lJZ35Si 1Bp6/bmzi+HAYRxj4J1FQU3NXcMwcuAP0Eh3QNXxka4On6N7WPjnbbIhNXLgc/xUxmsJQQ /p/OHUVDYdfSkS24VNiPwbpeTcc84sLgu1n5+8TfmjSHxSyhMIFhpnKvloY3ksHZaAkLz2 VHK5OfRdvX2H3HAOxn4Z9yRq7BUwTwiC56nBfiQzDOy4DJGWL54s1KDFeY4FIau2/bcuAT SrPrhY7TI4YbP0bsrc3FCdEbfsTcYPQ6s0oDYtloNRaeZ549PSr7qJ8rehbWLQ== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1641616554; a=rsa-sha256; cv=none; b=YlGB+UQIMZz7w1TimPhf5tAI+j4vOgPzs4OqkTQpcOKYwO98D+MNzTBVv7d5IPtj4PwuGT PzvqZED7L+EqfOz4kWvL86k2LtcCBE2cdXprIKGnIYLOcaI/kycO2LCRuF0+AOfrbKL+7F dbTSKDbOuLsiM5TDOVBV3pQug9WslNF+PDT+hrOBolt6wzqcsE3wS8PnUuzbNE3u5ORxhh lM7UjfnggU8HmAGr8SZATwPz/UyTRwWZD0ZNe0bujjpXqubTxhVFFWjoKFXJHkj7/OmUMD f3/HTA6tgsTbVb+KzR2ZB9KMXRuS0BL9FQJcl4wDOL89FAY6yKo7v95ZE8SNrw== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=pass header.d=tilde.club header.s=mail header.b=R8LYdDDV; dmarc=pass (policy=none) header.from=tilde.club; spf=pass (aspmx1.migadu.com: domain of "emacs-orgmode-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="emacs-orgmode-bounces+larch=yhetil.org@gnu.org" X-Migadu-Spam-Score: -3.30 Authentication-Results: aspmx1.migadu.com; dkim=pass header.d=tilde.club header.s=mail header.b=R8LYdDDV; dmarc=pass (policy=none) header.from=tilde.club; spf=pass (aspmx1.migadu.com: domain of "emacs-orgmode-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="emacs-orgmode-bounces+larch=yhetil.org@gnu.org" X-Migadu-Queue-Id: C278F2F8C3 X-Spam-Score: -3.30 X-Migadu-Scanner: scn1.migadu.com X-TUID: UF9okgbWLt4B This message is in MIME format. The first part should be readable text, while the remaining parts are likely unreadable without MIME-aware tools. --747550870-292115932-1641571785=:3100149 Content-Type: text/plain; format=flowed; charset=ISO-8859-7 Content-Transfer-Encoding: 8BIT i get the following error when i try to export to latex: org-babel-coq-initiate-session: ¡run-coq¢ not defined, load coq-inferior.el i've searched for the error on the internet, found out that the file "coq-inferior.el" exists: https://github.com/maximedenes/native-coq/blob/master/tools/coq-inferior.el i've downloaded the file and tried to manually load it, got: eval-buffer: Cannot open load file: No such file or directory, coq turned out i had to move my cursor to one of the coq source blocks. even then, in first try, i got: let: Symbol¢s function definition is void: coq-mode-variables and in second try, it successfully exports. this process above is consistent. it exactly follows those steps everytime. i've thought of adding some hooks but then found the idea very messy. besides, my elisp skills fail me in that case. i can export, in the end but, how can i resolve this neatly? --747550870-292115932-1641571785=:3100149--