1回答
当我在WP中使用Alt-ergo时，Frama-c按预期工作，但如果我尝试使用coq或coqide而不是Alt-ergo，那么对于Qed无法立即证明的每个目标，我都会得到以下错误： [wp] 13 goalsscheduled---------------------------------------------------需要注意的是，在显示错误之前
浏览 14提问于2019-03-08得票数 3
回答已采纳
我是对的-移动一个无符号整数，然后用&对它使用0b111，所以结果值必须在[0, 7]范围内。}
失败的断言发生在第我尝试了许多代码和ACSL
浏览 7提问于2022-03-11得票数 1
回答已采纳
现在，我已经从软件基金会( Software )开始工作了，那里的一切都是放在盘子里的，我很难弄清楚如何建立自己的项目。hello.vcoq_makefile -o Makefile.coq -f _CoqProject这会编译项目，但我无法让make
浏览 1提问于2019-08-18得票数 2
回答已采纳
我正在尝试浏览软件基础代码手册()，但是当我编译归纳.v(它看起来像)时，我得到了错误消息“错误:在当前环境中找不到参考”--甚至在编译Basics.v之后也是如此。你知道为什么吗？
浏览 0提问于2016-04-03得票数 6
CoqModel指令将每个属性的<input coq-model-attribute="...">附加到元素。CoqModelAttribute指令需要一个作为父对象的CoqModel来引用当前模型(这里是team1)，并将编译如下：
<div ng-controller="myController"><attribute_name>" coq-model-attribute="<attribute_na
浏览 1提问于2014-06-13得票数 1
1回答
我从命令行对这个简单的输入文件调用Coq：Theorem plus_O_n : (forall n, O + n = n).$ coqc ./AddingZero.v ; echo $?当我看到0输出时，我知道一切正常，所以我尝试通过执行以下操作来检查Coq的输出：但是我得到了一些二进制的胡言乱语。我做错了什么？谢谢!
浏览 11提问于2018-08-09得票数 0
回答已采纳
1回答
我编译Coq通常是为了测试一些更改，但是这个过程真的很慢，因为theories/中的标准库需要时间来编译。
是否有可能为实验生成一个“轻量级”的Coq版本？
浏览 3提问于2014-07-24得票数 4
回答已采纳
1回答
由于某些原因，我的Coq文件将不会编译。我在Windows 10上使用CoqIDE。当我使用Compile->Compile buffer工具时，另一方面，当我使用Compile->Make工具时，图片中给出了文件的全部代码。它也包括在下文。我兴高采烈地看了看，想得到一些关于发生了什么的解释。我发现的只是Coq 页面中的一条不祥的语句：
“在Windows上<e
浏览 0提问于2018-04-20得票数 0
错误:编译库Basics.vo对库Coq.Init.Notations做出了不一致的假设
当我使用CoqIDE_8.4pl5时，我在我的旧Macbook Air上没有遇到这个问题，但当我买了一个新的macbook但这次在macbook pro上，我使用了brew cask install coq来安装它……但它似乎不起作用，所以我从网站上下载了它，并将我的coqide路径设置为与我的旧macbook air中相同的路径当我尝试转发我<
浏览 2提问于2015-04-16得票数 9
我使用Coq8.4pl6，希望在Coq中编译Logic.v ( Coq标准库)，并将其输出作为模块编译和打印的示例，但失败了。我尝试的过程如下：
接下来，我试图通过运行coqc -nois Logic.v来使用空<e
浏览 2提问于2015-11-04得票数 2
1回答
当我使用Coq文件中的Extraction Language Haskell.将Coq解压缩/编译到Haskell并运行coqtop -compile mymodule.v > MyModule.hs时，我会得到一个以module Main where开头的Haskell模块。是否有选项可以设置生成的Haskell模块名称？我现在就像这样-
coqtop -compile mymodule.v | sed s/Main
浏览 1提问于2017-09-14得票数 7
回答已采纳
我使用的是自动Coq8.5 makefile生成器。此makefile以"Top.“作为所有模块的前缀。现在，假设您通过make运行了许多文件，然后希望在IDE中更改/调试某些文件。然后恼人的事实是，Coq抱怨它找不到编译的其他文件，因为在IDE中，它假定名称没有"Top“前缀。我试着调整makefile来去掉这个前缀。但我总是在make的错误消息中结
浏览 2提问于2017-03-31得票数 4
我成功地安装了coq 8.9.1和coq-Quickchick1.1.0和Opam2.0.4，我正在emacs 26.1上编程。但是，在运行QuickChick命令时，我收到以下错误：
知道我能做些什么吗？然而，没有取得任何成功，也没有提供任何有教育意义的信息。
浏览 2提问于2019-06-11得票数 2
我有两个短文件: cc_test由Lemma cc: 4 = 4. Proof. auto. Qed.提供，libtest由Require Import cc_test.ClosureLib -top ClosureLib cc_test /barry/svn/Coq/ coqc -R "/home/barry/svn/Coq/Closure_Calculus" ClosureLiblibtest _Calculus”和coqc -
浏览 3提问于2017-11-03得票数 3
1回答
我正在尝试跟踪，但是提供的源文件出现了错误，make失败了COQC src另外，只要调用cpdt/src文件的InductiveTypes.v并尝试逐行计算，我就会得到
Error: Cannot find a physical path bound to logical path我在我<
浏览 15提问于2022-05-19得票数 1
回答已采纳
3回答
我安装了Coq与opam，并想做一个Coq插件。我成功地使用coq_makefile编译了一些插件示例，但是如果我能够在vim中使用merlin来获得类型信息和Coq库的完成，那就太好了。我是否可以将Coq库添加到ocamlfind中？
浏览 9提问于2015-04-14得票数 5
回答已采纳
如果我执行像- From mathcomp Require Import ssreflect.这样的操作，它会给出以下错误。，它就会编译得很好。这可能是因为我安装了ssreflect，但并不完全是我想要的方式。
但问题是，我想要第一种工作方式，因为我有很多程序都是用这种方式编写的，而且似乎不符合逻辑地更改每个程序中的行。这是我的.emacs文件中的内容-(我想我可能需要添加类似于mathcomp/ssreflect的路径。&
浏览 15提问于2020-03-11得票数 0
回答已采纳
1回答
我有一个包含许多文件的Coq项目(比如x1.v，x2.v，...包括一个Makefile，存储在文件夹"C:\Users\WK\Desktop\Personal\ Coq -project“中，并且已经在我的Windows 7机器上安装了Coq 8.3的"C:\Coq”。Coq程序(文件)相互依赖。如何在Coq中执行单个程序(比如x1.v)？我想在Coq
浏览 6提问于2012-11-09得票数 2
1回答
我使用frama-C WP，并希望调试我的ACSL注释(以理解为什么验证者说我“不知道”)。我有一些绿色或橙色的结果。我打开why3集成开发环境，看到生成的脚本。然后，我从列表中选择一个理论/目标，并能够启动Alt-Ergo或Coq IDE。我想在Coq IDE中使用生成的代码。我看到一些公理，然后是定理WP，然后，举个例子：
intros a a_1 i_3 i_2 i_1 i t_2 t_1 t t_8
浏览 2提问于2017-08-26得票数 2
我真的不知道如何在Coq中实际使用多个文件。我是想跟着走。src/a.vsrc/b.vcoqc -R src "" src/a.v src/b.vuser@machine:~/code/coq$ coqc -R src "" src/a.v src&#x
浏览 19提问于2021-02-18得票数 0
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
