问题标签 [coq-extraction]

我正在尝试提取一些我用 Coq 编写的文件系统代码。我想FileIO用 Haskell 的Monad 替换我的IOMonad。我的代码如下所示：

替换sync没问题，但是当我尝试替换FileIO时IO出现以下错误：

这个错误是什么意思，我该如何解决？

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

我收到以下错误：

如果我尝试改为：

我得到错误：

我正在为 MacOSX 使用 CoqIDE 8.5beta3。

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

当我在 Coq 文件中提取/编译 Coq 到 HaskellExtraction Language Haskell.并运行coqtop -compile mymodule.v > MyModule.hs时，我得到一个以module Main where.

是否有设置生成的 Haskell 模块名称的选项？

我目前像这样通过管道传输到 sed -

但我正在寻找更清洁的解决方案。

我知道可以将 Coq 程序提取到 Haskell 和 OCaml 程序中。有没有办法用C来做到这一点？

我正在想象一个模拟 C 语言的库。也许这样的库将包含一组关于 C 构造如何与进程内存交互的公理，以及关于 IEEE 浮点数的公理和定理。然后它将能够在 Coq 中构建一个 C 程序以及关于该程序的定理。

例如，我会使用这样的库来构建一个 C 快速排序算法，该算法适用于 GCC 可编译的浮点数组。

I am using the XML Protocol from Coq 8.6.1. When I tried the PrintAst call, I failed to get an AST, but got an "todo" instead. Is this a malfunction or did I do something wrong? How should I get an AST from a print AST call?

Here is my case: I used coqtop -toploop coqidetop -main-channel stdfds to open an ideslave process, an then input the Coq code from coq-8.6.1/theories/FSets/FSetCompat.v.

Here I use "<<<<<<<" to enclose some detailed procedures if you would like to repeat my experiment.

<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<

First, I input

then

then

and finally

<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<

At this time, I called <call val="PrintAst"><state_id val="5"/></call>, which I expect to return the AST of

To my disappointment, I got

By pretty printing it is

But this is merely a copy of the code! It even didn't apply a lexer... Why would this happen? Could somebody help? Thank you so much!

我一直在努力寻找关于 Coq Contexts、evars、e* 策略等的好的指南/阅读/练习集。

理想情况下，我想构建一个包含一些抽象变量的 Coq 上下文，稍后我将在 OCaml 或 Haskell 提取中填写这些内容。这可能吗？阅读有关定理漏洞以及如何在 Coq 证明中填充它们的最佳位置是什么？

我正在使用 Coq 的 ideslave（又名 XML 协议）。通过调用<call val="Goal"><unit/></call>，典型的反馈看起来像

我已将此反馈格式化为 AST：

如您所见（如您所知），“目标”标签下有四个列表。Coq 文档给了它们四个名称（当前目标、背景目标、搁置目标和废弃目标）。

我的问题：

1. 后三个目标类别是什么：背景目标、搁置目标和废弃目标？我找不到关于“搁置”和“放弃”目标的文档。

2. 三者在哪些方面有所不同？他们的名字很相似。

3. 为什么我们要pair在背景下列出目标（即第二个列表），然后在 下再次列出，pair然后才是实际目标？pair第一个和第二个下的背景目标之间有区别pair吗？

感谢您的帮助！

EvalOp 的定义在compcert.backend.SplitLongproof：

这个定义的奇怪之处在于将andcoqdoc --html识别为两个单独的标记：EvalOp

为什么 Coq 允许在中间没有分隔符（空格）的两个标记？或者这是一个错误coqdoc？感谢您的帮助！

在看QuickChick项目的时候，遇到了一句Require Import Ltac.我不知道这是做什么的，Ltac模块在哪里。我找到了一个文件plugins/ltac/Ltac.v，但这不可能是那个文件，因为这个文件是空的（顺便说一句，包含一个空文件的目的是什么？）。我试过了，Locate Ltac.但我得到了Error: Syntax error: [constr:global] expected after 'Ltac' (in [locatable]).，这更令人困惑。

模块做什么Ltac，文件在哪里Ltac.v，为什么Loacte在这种情况下命令不起作用？谢谢！

我正在从 Coq 提取到 Haskell，这需要在 Haskell 端导入几个模块。是否有任何 Coq 提取功能可以让您自动执行此操作？我知道我可以写一个脚本来做到这一点，但如果有必要我宁愿不要重新发明轮子。