From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp10.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms0.migadu.com with LMTPS id yC/eJIZq2GGYbwEAgWs5BA (envelope-from ) for ; Fri, 07 Jan 2022 17:29:58 +0100 Received: from aspmx1.migadu.com ([2001:41d0:2:4a6f::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp10.migadu.com with LMTPS id 8FpgHYZq2GH8egEAG6o9tA (envelope-from ) for ; Fri, 07 Jan 2022 17:29:58 +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 31DD312BA2 for ; Fri, 7 Jan 2022 17:29:58 +0100 (CET) Received: from localhost ([::1]:37522 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1n5s7o-0003qQ-Ra for larch@yhetil.org; Fri, 07 Jan 2022 11:29:56 -0500 Received: from eggs.gnu.org ([209.51.188.92]:34210) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1n5s7K-0003qB-86 for emacs-orgmode@gnu.org; Fri, 07 Jan 2022 11:29:26 -0500 Received: from [2a00:1450:4864:20::533] (port=45911 helo=mail-ed1-x533.google.com) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1n5s7A-0005g1-6a for emacs-orgmode@gnu.org; Fri, 07 Jan 2022 11:29:17 -0500 Received: by mail-ed1-x533.google.com with SMTP id j6so24017382edw.12 for ; Fri, 07 Jan 2022 08:29:14 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=date:from:to:subject:message-id:mime-version:content-disposition :content-transfer-encoding; bh=Q6nB0CpMc+sNyiXHYZlgW/AmXF0pQuW6rAksEPeUOn4=; b=JFoLZvRudR2m2A4cnM8iugce3EbysTCLxxxEmesD+6iei0VlTt0ETshQmycC6AzwR6 JL0Jxjxfp1m7T2GseQnxTkfhj2aaJnnxK6qT1PAOkxnjARBcuxXaaAUDlANbL0RhZMUq fEy71i5kpt/bIKAb7FjxdtchK13JDjV8uOTNMid9FFkVxED9yXvrtHXLpw4Xn08T8MCt gaGs3cZTKGQWwPsMk0B9mm5ld7QoQac0Et53AlTZxTQWrIGIxjnAMVEbYk4Va7qD38Kf GuVpoS8nzVlcB+4yUj2k+p8LfHmb8PvETigvvngpG4HZyTTk45CSi14Xcfu50I4rvDKf ibFw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:subject:message-id:mime-version :content-disposition:content-transfer-encoding; bh=Q6nB0CpMc+sNyiXHYZlgW/AmXF0pQuW6rAksEPeUOn4=; b=rQAw0/zfHIrZHYeu6IjOW2N4XwZBBgQl4KO5EXcASxGbeGOpAsYm3mY2xLoKfVNVdM sWDCVmofvghJlpUUycdT8Z1x2mWUsPppA8jOISefH7Ga8U3X24/MuV99+XCL5okEHgsu Eta4EzTH/V6hV8LgPdsqtOZo7vE/sp+LOZDeZDDv68gZ7G7k2AN951rYOzwf3s0BeodJ HTLO7EmA5pJ+TNdjA4AVFYFThhSliJg/4L4/K0TpGcmDWqzXj+NH5LLLKzxw48HekGxw aMDJtStzxMBCFKmtZuusYsmoLBKQbrTG1Ifk4L8v3Lz3oWp60yJAMUt6r1UQv0Dcc0Lw zyPQ== X-Gm-Message-State: AOAM530UHC85ZBJfkkxDoGus/Fbi9/qHZcXxwWoWLLpdbo3NkAmyxSew N79v6Fr4wVoEkKaiwt2FnrRdo7lRBts= X-Google-Smtp-Source: ABdhPJwDNAb6sj0Wm+e7Msf6xFjLHYjVkryBxOZ3PcZ3SY0xYMcQoIZhhpIxPKgDMplnjyC4OekjMg== X-Received: by 2002:a17:907:3d94:: with SMTP id he20mr48867487ejc.14.1641572953752; Fri, 07 Jan 2022 08:29:13 -0800 (PST) Received: from a.localdomain ([88.237.65.72]) by smtp.gmail.com with ESMTPSA id i9sm1545654ejw.170.2022.01.07.08.29.13 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 07 Jan 2022 08:29:13 -0800 (PST) Date: Fri, 7 Jan 2022 19:29:12 +0300 From: abdullah uyu To: emacs-orgmode@gnu.org Subject: coq related error when exporting to latex. Message-ID: MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Disposition: inline Content-Transfer-Encoding: 8bit X-Host-Lookup-Failed: Reverse DNS lookup failed for 2a00:1450:4864:20::533 (failed) Received-SPF: pass client-ip=2a00:1450:4864:20::533; envelope-from=abdullahuyu@gmail.com; helo=mail-ed1-x533.google.com X-Spam_score_int: 1 X-Spam_score: 0.1 X-Spam_bar: / X-Spam_report: (0.1 / 5.0 requ) BAYES_05=-0.5, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_NONE=-0.0001, RDNS_NONE=0.793, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=no autolearn_force=no X-Spam_action: no action 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=1641572998; 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: content-transfer-encoding:content-transfer-encoding:list-id:list-help: list-unsubscribe:list-subscribe:list-post:dkim-signature; bh=Q6nB0CpMc+sNyiXHYZlgW/AmXF0pQuW6rAksEPeUOn4=; b=kKfN8wFvgc8hHg0008SSwKP1OCIKyv0jRou0ncNBL58mmD/VeaZquJ+GDEMylEixrmeOOp C7R2MQEhPWr1wUSrNDCnWrkVfhrtiL27Xh0XFwiDIbE2CAash9M+v6laRho76kcpCHwh1c RDOJ20w+7iJZvleFhkeoS28fopnnK87XjVn6Hsnr3yYkNHWFPXv1MJH2GKlhSSTs3Dib1C BHdOWiuuMPBMjfpAkevFG+4ifiUQ3pssXuntS3bLJ75IV6JqTyDbUyiAoxYREHAXFA6NIY vSAxAm0zO/rFk3Til5NI2dw1V9hgofQC+qRAVejNnWINXuWlxYBvxiDrIBZBaw== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1641572998; a=rsa-sha256; cv=none; b=VOs5qhpi5rUQYMaAE+bqTuzO+w1eJOhsEEjiCNPjS2EvDk/bZV+oYKmASLYQ22yRJUO9uH Gok/qpxad0KXZjiSIULtwcKdA2A0DjPLgumHKakRFqe8KUUJuVFT5zB/Fj/I3A8AmeLg77 7HEihM4vKhxTRc3jq5jtzy5AsanX/XsGMYPbcEF4XU1vrnvogcYYTgCmP70fFKNfBAp3m7 i5Au8dyZVOO/mtqVwloiWlEHvcdl6JPcgEm0YY1QL9VvYI+x6a//Uz0ydd+qr/PhxvRRYf 0006QmvdRyU+S+M1RJaiD1a106YTNk7AAUsafONYTEHiR2/Abq0t8GrNf+x4AA== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=pass header.d=gmail.com header.s=20210112 header.b=JFoLZvRu; dmarc=pass (policy=none) header.from=gmail.com; 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: -8.90 Authentication-Results: aspmx1.migadu.com; dkim=pass header.d=gmail.com header.s=20210112 header.b=JFoLZvRu; dmarc=pass (policy=none) header.from=gmail.com; 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: 31DD312BA2 X-Spam-Score: -8.90 X-Migadu-Scanner: scn0.migadu.com X-TUID: mRQ9XvTTyJaM 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?