From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp10.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms5.migadu.com with LMTPS id SMhHEW2ic2KIlgAAbAwnHQ (envelope-from ) for ; Thu, 05 May 2022 12:09:49 +0200 Received: from aspmx1.migadu.com ([2001:41d0:2:bcc0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp10.migadu.com with LMTPS id qPpCEG2ic2IzcgAAG6o9tA (envelope-from ) for ; Thu, 05 May 2022 12:09:49 +0200 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 D520F9528 for ; Thu, 5 May 2022 12:09:48 +0200 (CEST) Received: from localhost ([::1]:58288 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1nmYQd-0000xp-Ts for larch@yhetil.org; Thu, 05 May 2022 06:09:47 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]:50522) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1nmYOC-0000sx-QI for emacs-orgmode@gnu.org; Thu, 05 May 2022 06:07:16 -0400 Received: from mail-pj1-x1032.google.com ([2607:f8b0:4864:20::1032]:43542) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1nmYO6-0000FX-Tj for emacs-orgmode@gnu.org; Thu, 05 May 2022 06:07:16 -0400 Received: by mail-pj1-x1032.google.com with SMTP id j8-20020a17090a060800b001cd4fb60dccso3679589pjj.2 for ; Thu, 05 May 2022 03:07:09 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=from:to:cc:subject:in-reply-to:references:date:message-id :mime-version:content-transfer-encoding; bh=8BDmhSGTrnJZL3sPyC4fKbkHirCzsXTm1Ny5MiDkdRE=; b=CsojS8/5Zbvd8uISdLWypSFv47t/EaX5TgvnAOFZ9BI0Ba9MjRMKsjfMQnSUUBaHUa NXOTUYQJ6UynsETE6+XX+Aqog2o3Bf0hMl6Uf2UY30pX9v62BRgp+cSdmMw3zX6Xn+P0 AONdTbBpqs50LCcOdx8jdb3UdCN77imfRcHZbAE7Sc4TZecH1dio0509H3wbZTdN69So 1FO8gJ39QZreB2Pv947KkBreEs0u4rx2tK+htWtm582cnMbQcnza3/PL2mHokxvYbpZW t0SW2w5WcJLk1RAvl5L+YR1drPjVyS8OTNESSHBDqo0n1Pjp+0qLiKtE79D9KhaSHCoN Le0g== 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:in-reply-to:references:date :message-id:mime-version:content-transfer-encoding; bh=8BDmhSGTrnJZL3sPyC4fKbkHirCzsXTm1Ny5MiDkdRE=; b=vn/0M4pxV2TU6AEZNXJAq/8hpTc64hUpTOUPrZpuTLO7FzgdQJIL9vVILE23nbhBDP smj4qoJYKBNri50Tjin+bLMJC/FQYThMie1lHekjI4lbkk2YZTNQPG8OQbRIFJZ9vfHk 0N1gbWsncckYxXydqoIhpXeYbU35wcUaxL+ntqvWbDF7vmCRzp380uIUsLfbbnKbPKaD XKbxTZAA4Mx0utlvHxw3qAHijiFCvH8ECc/JOG8reEOgGv+qWqjwSEhLavnki8hi7lM4 o86V0qvhfZ6rP/oMhQ4DKgsY+une0ZLPYvSf5swYlla2fYe9CU6hNmn98kuD6uA11tZ7 0TRA== X-Gm-Message-State: AOAM530KwWWBj15LygPdIpAWzaxwDmfx1arYVr9cCZfAxJJfnrklN2gi NOKihFer/bztQwsk321Nl/k= X-Google-Smtp-Source: ABdhPJxkJwjRDKYVWFgedChkRSMcY4EmgAHbEutNsOr2skJYngQUumERrXqBeUBqXxm4bUl0xsp6lg== X-Received: by 2002:a17:902:7586:b0:15e:c2fe:bad0 with SMTP id j6-20020a170902758600b0015ec2febad0mr8640076pll.72.1651745228367; Thu, 05 May 2022 03:07:08 -0700 (PDT) Received: from localhost ([66.115.157.242]) by smtp.gmail.com with ESMTPSA id nl11-20020a17090b384b00b001cd4989ff65sm1151026pjb.44.2022.05.05.03.07.06 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 05 May 2022 03:07:07 -0700 (PDT) From: Ihor Radchenko To: abdullah uyu Cc: emacs-orgmode@gnu.org Subject: Re: coq related error when exporting to latex. In-Reply-To: References: Date: Thu, 05 May 2022 18:07:51 +0800 Message-ID: <87ee188f7s.fsf@localhost> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Received-SPF: pass client-ip=2607:f8b0:4864:20::1032; envelope-from=yantar92@gmail.com; helo=mail-pj1-x1032.google.com X-Spam_score_int: -18 X-Spam_score: -1.9 X-Spam_bar: - X-Spam_report: (-1.9 / 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, FREEMAIL_ENVFROM_END_DIGIT=0.25, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham 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-To: larch@yhetil.org X-Migadu-Country: US ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1651745389; 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: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references:list-id:list-help: list-unsubscribe:list-subscribe:list-post:dkim-signature; bh=8BDmhSGTrnJZL3sPyC4fKbkHirCzsXTm1Ny5MiDkdRE=; b=ErAAfervNCcc6l3zvZpr4+E7MI7RmLPoe3sML/CityyMHUSuLBzjl6XUj4ge3RADq/hK0N PCgm8cJ/brW0KV6/Q0NjJRfYubwwjJa8vf01KALQHR6n6S04OOL/GUfzeY0ODEu8UgqJKd OwVg0aBU++joL+ednZxzB/rZdQVBW7hw7ORiAZMP5lFigelf+626xAA8ZZgEkBNcUQIMZB dYoBUP0jCwxb0MHhZif5M/oqWJ5CfIbZs1Z3lyVTaRFzNLEltNIZmbiaGlzxdNeZlSc1Ar xxGtrmk+Q+FyqJbUcUWnFReQm6XiLrfvFSJ4cKa4GpIqGY6xJVLQ1SLHTDh89g== ARC-Seal: i=1; s=key1; d=yhetil.org; t=1651745389; a=rsa-sha256; cv=none; b=i8zrV6zIgc3nyl46jHQ1YK4b00OSZpE631VugLaq5M9+sgNcJtkNRC547AyDL2MzuGeUQo 5GLHy0gP8NlknM26LGmKNIyPJqX62ze0qQcbGEeY8cBbbW7DhCujpmm5iRrK7h7MKCdavL wv9NUQj2qMJli/oQNgvU1hR87HIv1f8gZaSxT8gDzvC4ljNKWCiGf9pnpKWv8pw4hDz6wb DJBer48YH0mhPazdXZ/kxbOJSDAUHCjHaVY2ZggUKIpqI8NXhFFPaMmOi7uVi0ij2ICom0 FOmcpnc/fxEl+30ip7l6lQMTuvvM4gh9KKQUBqY2yeqFK1Zb7jauHcJqsNoU4g== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=pass header.d=gmail.com header.s=20210112 header.b="CsojS8/5"; 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: -3.49 Authentication-Results: aspmx1.migadu.com; dkim=pass header.d=gmail.com header.s=20210112 header.b="CsojS8/5"; 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: D520F9528 X-Spam-Score: -3.49 X-Migadu-Scanner: scn0.migadu.com X-TUID: HK/PtNkdKR3y abdullah uyu writes: > i get the following error when i try to export to latex: > > org-babel-coq-initiate-session: =E2=80=98run-coq=E2=80=99 not defined, lo= ad > coq-inferior.el Most likely, ob-coq expects you to have coq major-mode installed. Note that ob-coq is currently not maintained and might be outdated. Best, Ihor