问题标签 [proof-general]

我在 Ubuntu 12.04 LTS 上有 emacs 23.3.1，并带有一般证明 4.2。在“coq Holes”模式下编辑 coq 文件时（这是我破解 coq 时的默认设置），我无法使用选项卡。这样做会产生错误

错误类型参数 integer-or-marker-p nil proof general

在小缓冲区中。我该如何解决这个问题？

每次我在 Emacs 缓冲区中打开一个 .csv 文件时，Proof General 都会启动（除非它已经启动）并重置我的窗口。这真的让我的 Emacs 无法正常工作，需要停下来。

我的 init.el 中唯一处理 Proof General 的部分是：

当我在窗口模式下使用 emacs 时，一切似乎都很好。但是，在终端中，Proof General 的光标（指示它在代码中的位置）覆盖了它所在行的前两个字符。

这看起来像一个错误，但也许它是某种设置？有没有人遇到过这个？

我一直在尝试学习使用 Isabelle 2016。虽然原则上我喜欢异步证明检查的想法，但我不喜欢 Isabelle/jEdit 的原因有很多，其中最严重的是它使用了太多内存（为了我）。

如果我可以在 Isabelle 2016 中使用旧的 Proof General，那就太好了。我将变量设置isa-isabelle-command为指向bin/isabelleIsabelle 分发目录下的文件。当我使用 Proof General 的菜单启动 Isabelle 时，Emacs 挂起，当我用 中断它时，我在缓冲区C-g中得到以下内容。*isabelle*

我知道该站点上的旧帖子表明 Proof General 用于与定理证明器通信的 Isabelle 组件已被删除。2016 年的伊莎贝尔 (Isabelle) 是否（仍然）如此？如何在新版本的 Isabelle 中使用 Proof General？

与 Agda 不同，Coq 倾向于将证明与函数分开。Coq 给出的策略非常适合编写证明，但我想知道是否有一种方法可以复制一些 Agda 模式的功能。

具体来说，我想：

• 相当于 Agda?或 Haskell 的_，我可以在编写函数时省略部分函数，​​并且（希望）让 Coq 告诉我需要放在那里的类型
• 相当于 Agda 模式 (reify) 中的 Cc Cr，您可以在其中?使用函数填充块，它会?为所需的参数创建新块
• 当我match在一个函数中执行一个函数时，让 Coq 自动编写扩展可能的分支（如 Agda 模式中的 Cc Ca）

在 CoqIde 或 Proof General 中这可能吗？

可能是一个coq新手问题，但我找不到现成的解决方案，所以我会在这里询问以供参考。cocq版本是8.5pl2

我试图构建 coqfj。第一次make尝试失败，在第 37 行出现了一些错误src/FJ/ClassTable.v。这个问题与那个错误无关。

仔细一看，我ClassTable.v在 emacs proofgeneral 中打开并按下C-c C-n，或者运行coqc src/FJ/ClassTable.v。结果是第 1 行中的错误：

似乎require import FJ.Lists无法解析导入（尽管 FJ 用作前缀，而不是后缀）。我注意到make已经创建了一个编译文件src/Lists.vo，应该由 coqc 获取。

*.vo如何通过查看文件夹中的or*.v文件来告诉 coqc 它应该解决这个“后缀” src？

这个问题是询问有关使用 deepmind 开源库的方向/建议/帮助：https ://github.com/deepmind/lab或https://www.tensorflow.org/在 Python 中。

考虑到我是深度学习和人工智能等概念的新手。

问题是：

• 是否有使用 Deepmind 或 Tensorflow 解决我需要观察值并采取行动的数学问题的示例？

基于观察、行动、奖励等，使用类似于本页 ( https://deepmind.com/blog/open-sourcing-deepmind-lab/ ) 中描述的方法，我想调用学习代理在一些值中进行选择。我在想这样的事情：

• 输入：元组列表的列表（列表将在每一步更改）
• 行动：从输入中获取一个值（基于经验）
• 奖励：如果它返回的值对于我正在实施的算法的其余部分是好是坏，我将奖励深度学习代理。

补充说明：

• 我无法提前训练算法

输入是这样的（只有数字）：

这个想法是使用与 deepmind 玩游戏相同的方法，但不是分析像素并使用 pad（上、下、左、右、火、跳跃），而是让学习代理分析一些数学值，并且，作为唯一的动作，选择其中之一。

是否有其他方法或库/框架来解决此类问题？

似乎 PG 不允许同时运行 2 个脚本。尝试执行此操作的那一刻，Emacs 将提示并要求收回另一个文件。有时，重新运行脚本并非易事。有没有办法在单个 Emacs 实例中实际运行 2 个（或更多）脚本？我不认为 coq 附带的 coqide gui 没有这样的问题。

我正在用 emacs 研究 Coq。我把emacs窗口垂直溢出了，左边是文档，右边是代码编辑区。当我解释 Coq 程序时，结果将显示在左侧窗口中并覆盖文档。这让我很困扰。是否有这样一种方法可以将代码编辑区域水平分割，并且解释结果显示在右下角？

为了尝试理解如何OrderedType在 Coq 中定义我自己的，我正在研究（此处）OrderedType中标准库中给出的 s示例。截至目前，我只关心前几个模块：Coq.Structures.OrderedTypeEx

当我在 Proof General 中自己逐步完成此操作时，Error: Proof editing in progress.当我到达最后一行时出现错误。看来它希望我lt_trans在它接受模块结束之前证明它。这很公平。但是，如果没有证据，这如何作为标准库的一部分工作呢？它是否以我不理解的方式隐含地引用了一些先前的证据？另外，如果我确实Proof. Admitted.能够跳过引理证明，那么它需要一个Definition compare x y : Compare lt eq x y.. 为什么它会要求一个定义的证明？