问题标签 [coqide]

我想检索文件编译的结果。v 来自 coqide 或 coqc 用于用 java 处理，而不是我处理自动机，我想在 java 中构建这个自动机的图形界面。

感谢您的答复。

我正在尝试使用我在此页面上找到的 CoqIDE for vim 插件。

我将 coq_IDE.vim 文件放在 ~/.vim/ftplugin 文件夹中。我当前的 .vimrc 文件是：

但是当我启动 vim 时，CoqIDE 不会自动加载（与普通 vim 相比，我没有看到任何变化，所以我认为没有）。当我尝试通过命令手动加载它时:source coq_IDE.vim，我收到以下错误消息：

这个错误的根源可能是什么？

以下是一些可能相关的附加信息：

1) 我正在运行 Ubuntu 14.04。

:version2）我在 vim 中检查了它+perl。

2）我从终端运行vim，而不是gvim。

3) 我尝试删除并重新安装不同版本的 vim (vim, vim-gtk, vim-gnome)

4) CoqIDE 安装指南说coqtop.opt应该可以通过PATH变量访问。由于我什至不确定这意味着什么，这可能是这里的问题，但这似乎不太可能。据我了解，vim 在尝试读取时会出错coq_IDE.vim，所以它甚至没有到达它正在寻找的部分coqtop.opt。

5) 我从 Ubuntu 软件中心安装了 CoqIDE。

6）:echo &runtimepath我得到：~/.vim,/var/lib/vim/addons,/usr/share/vim/vimfiles,/usr/share/vim/vim74,/usr/share/vim/vimfiles/after,/var/lib/vim/addons/after,~/.vim/after

我一直在 Linux 机器上使用Vim 的 CoqIDE 插件来编辑 Coq 文件。现在我正在尝试在 Windows 8 上安装它。但是当我尝试获取插件时，我得到了

这很奇怪，因为:version我清楚地看到了+perl/dyn包括在内。这与+perl我需要的不同吗？

我听说你需要在 Vim 之前安装 Perl 才能获得支持 Perl 的 Vim，所以我也尝试了。我卸载了 Vim，安装了Strawberry Perl 5.18.2.2 (64bit)，然后重新安装了 Vim。还是同样的问题。

如果解决方案涉及手动编译二进制文件，我将非常感谢详细的说明，因为我没有任何经验。

我正在尝试使CoqIDE Vim 插件在 Windows 8.1 上运行。当我从 Vim 获取插件时，我收到以下错误消息：

所以我查阅了插件文档，发现了似乎相关的部分：

我不确定这意味着什么，但我猜测有一些名为coqtop的文件或目录必须对 vim 可见。所以我打开了我的 Coq 安装目录并搜索了coqtop. 搜索结果是：

这里明显的第一个候选人是coqtop. 当我单击它时，它会打开一个交互式 Coq 控制台。但是当我使用let CoqIDE_coqtop命令将此文件链接到 Vim 并再次加载插件时，我得到：

看起来有问题的另一件事是文件类型。正如您从上面的错误消息中看到的，该coqtop文件具有.exe特定于 MS-DOS 和 Windows 的扩展名。但我不认为该插件是为处理.exe文件而编写的......

我还尝试使用所有其他搜索命中 as coqtop，但无济于事。

这是否意味着该插件在 Windows 上无用？如果有人可以确认我会放弃并使用其他 IDE。但如果可能的话，我真的，真的很想继续使用 Vim。

rlwrapREPL是一个在循环中处理箭头键的好程序。在大多数情况下，它都有效。例如rlwrap sbcl、rlwrap sml等。但是当涉及到 时rlwrap coqtop，它失败了。错误信息如下。 rlwrap: error: Couldn't read completions from /usr/local/Cellar/rlwrap/0.41/share/rlwrap/completions/coqtop: No such file or directory

我coqide从 coq 网站下载，并rlwrap使用homebrew. 该文件/usr/local/Cellar/rlwrap/0.41/share/rlwrap/completions/coqtop位于正确的位置。那么，有什么线索可以解决这个问题吗？或者那里有替代软件？

我是一名 Coq 新手，因此为了提高我对证明检查的理解，我正在尝试使用 Ssreflect 库。

我已经在终端上运行的 Mac OS v 10.10.3 ( Yosemite ) 上安装了 Ssreflect v 1.5。

但是，当我尝试使用以下命令将库加载到 CoqIDE 8.4p15 中时：

我得到错误：

我试过使用：

当前设置了 SSRCOQ_LIB 的位置，但出现错误：

感谢从 CoqIDE 中加载 ssreflect 库的任何帮助。

在大多数 IDE 或文本编辑器中，您可以右键单击一个术语，然后它会将您带到定义该术语的文件。CoqIDE 似乎没有，所以我一直在做coqdoc myfile.v --html，然后转到生成的 HTML 文档。但该文件中唯一可点击的术语是针对 Coq 标准库的。ssreflect 定义的术语（例如）不可点击。

在 Coq 文件中，是否有一种标准方法可以快速查找定义某些术语/标识符的位置（及其源代码）？在 CoqIDE 或 emacs + ProofGeneral 中（我正在使用 CoqIDE，但如果 emacs/ProofGeneral 有这种能力，我会切换）。

还是为您使用的每个 Coq 项目和依赖项生成文档的标准方法？

当我在 CoqIDE 中执行以下命令时：

我收到以下错误：

如果我尝试改为：

我得到错误：

我正在为 MacOSX 使用 CoqIDE 8.5beta3。

我怎样才能解决这个问题？如何在没有权限问题的情况下通过 CoqIDE 进行提取？

在我的CoqIDE交互式会话中既不Reset <sectionname>.也不工作。消息是Reset <globalconstant>.Reset Initial.

Reset我见过的唯一工作是Reset Extraction Blacklist.和Reset Extraction Inline.。以下是帮助 > 关于中的一些信息的副本。提前感谢您的任何想法

我安装了 Coqide 8.5 w/ nix。不幸的是，所有面板中的文本都是空白的；没有任何形式的语法突出显示（否则，8.5 似乎比我安装的 8.4 有了很大改进）。我还得到以下信息：

的输出cat ~/.nix-profile/share/coq/coq_style.xml：

鉴于第一个警告，我想应该有别的东西而不是"classic"但是什么