程序员经验分享-hwhale

Coqide 错误：编译的库 Basics.vo 对库做出了不一致的假设

2024-02-20

我在 mac os X 上使用 CoqIDE_8.4pl5。 当 CoqIDE 转发到此命令时，会弹出此错误消息：需要导入基础知识。

错误：编译的库 Basics.vo 对库做出了不一致的假设 Coq.Init.Notifications

当我使用 CoqIDE_8.4pl5 时，我在旧的 Macbook Air 上没有遇到这个问题，但是当我有了新的 MacBook Pro 时，我从同一个网站再次下载了它。 但这一次在这台 macbook pro 上，我使用了brew cask install coq 来安装它......但它似乎不起作用，所以我从网站下载了它并将我的 coqide 路径设置为与我的旧 macbook 中的路径相同空气..当我尝试转发我的作业时，我遇到了这个问题。有没有什么办法解决这一问题？或者我必须删除 coq 并复制并重新安装它？


这通常是 Coq 告诉您 Basics.v (Basics.vo) 的编译版本是使用与您当前使用的版本不同的 Coq 版本编译的。

出于安全原因，Coq 的每个版本只希望使用用同一版本编译的文件。

修复方法通常是删除有罪的 Basics.vo 文件并重现创建它的编译步骤。

如果错误再次发生，则可能是您的系统安装了两个版本的 Coq，其中一个版本由您的构建脚本访问，而另一个版本由 CoqIDE 使用。

本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)

coq

Coqide 错误：编译的库 Basics.vo 对库做出了不一致的假设 的相关文章

  • 如何在 Coq 中使用归纳类型来处理案例

    我想使用destruct通过案例来证明陈述的策略 我在网上读了几个例子 但我很困惑 有人可以更好地解释一下吗 这是一个小例子 还有其他方法可以解决它 但尝试使用destruct Inductive three zero one two Le

  • 如何证明 Coq 中的两个 Fibonacci 实现相等？

    我有两个斐波那契实现 如下所示 我想证明它们在功能上是等效的 我已经证明了自然数的性质 但是这个练习需要另一种我无法弄清楚的方法 我使用的教科书介绍了 Coq 的以下语法 因此应该可以使用这种表示法来证明相等性

  • 如何在 Coq 中自动证明实数的简单相等？

    我正在寻找的是auto类似的策略可以证明简单的等式 例如 1 2 2 4 到目前为止 我手动尝试过的是使用ring simplify and field simplify来证明等式 即使这样效果也不好 Coq 8 5b3 下面的例子有效 R

  • 当 Coq 中使用自己的可判定性时，评估计算不完整

    The Eval compute命令并不总是计算为简单表达式 考虑代码 Require Import Coq Lists List Require Import Coq Arith Peano dec Import ListNotation

  • Coq 中归纳集的归纳子集

    我有一个用三个构造函数构建的归纳集 Inductive MF Set D MF cn MF gt MF gt MF dn Z gt MF gt MF 我想以某种方式定义一个新的归纳集 B 使得 B 是 MF 的子集 仅包含从 D 和 dn

  • 归纳命题在 Coq 中如何运作？

    我正在阅读软件基础中的 IndProp 和 Adam Chlipala 的第 4 章书 但我在理解归纳命题时遇到了困难 为了运行示例 让我们使用 Inductive ev nat gt Prop ev 0 ev 0 ev SS forall

  • Coq Proof Assistant 中依赖类型的问题

    考虑以下简单的表达语言 Inductive Exp Set EConst nat gt Exp EVar nat gt Exp EFun nat gt list Exp gt Exp 及其格式良好的谓词 Definition Env lis

  • 证明唯一的零长度向量为零

    我有一个类型定义为 Inductive bits nat gt Set bitsNil bits 0 bitsCons forall l bool gt bits l gt bits S l 我试图证明 Lemma emptyIsAlway

  • Ltac：通过回溯重复策略 n 次

    假设我有一个像这样的策略 取自 HaysTac 它搜索一个参数来专门化一个特定的假设 Ltac find specialize in H multimatch goal with v gt specialize H v end 然而 我想写

  • Coq：将信息保存在匹配语句中

    我正在构建一个递归函数match在清单上l 在里面cons分支我需要使用以下信息l cons a l 为了证明递归函数终止 但是 当我使用match l信息丢失 我该如何使用match保留信息 这是函数 drop and drop lemm

  • 对术语...进行抽象会导致术语...类型错误

    这是我想证明的 A Type i nat index f nat nat n nat ip n lt i partial index f nat option nat L partial index f index f n Some n V

  • coqide - 无法从同一文件夹加载模块

    我无法加载 CoqIde 中同一文件夹中的模块 我正在尝试从 Software Foundations 加载源代码 我正在包含 SF 源代码的文件夹中运行 coqidecoqide or coqide 然后打开并运行该文件后 我收到此错误

  • 在 Coq 中，重写适用于 = 但不适用于 <-> (iff)

    我在证明期间有以下内容 我需要替换normal form step t with value t因为有一个已证明的定理存在等价 H1 t1 gt t1 normal form step t1 t2 tm H2 t2 gt t2 normal

  • 如何将假设中的具体变量更改为存在量化变量？

    假设我有一个这样的假设 FooProp a b 我想将假设改为这种形式 exists a FooProp a b 我怎样才能做到这一点 我知道我能做到assert exists a FooProp a b by eauto但我试图找到一个不

  • Coqide 错误：编译的库 Basics.vo 对库做出了不一致的假设

    我在 mac os X 上使用 CoqIDE 8 4pl5 当 CoqIDE 转发到此命令时 会弹出此错误消息 需要导入基础知识 错误 编译的库 Basics vo 对库做出了不一致的假设 Coq Init Notifications 当我

  • 在 Coq 中证明可逆列表是回文

    这是我对回文的归纳定义 Inductive pal X Type list X gt Prop pal0 pal pal1 forall x X pal x pal2 forall x X l list X pal l gt pal x l

  • 依赖类型的 Church 编码：从 Coq 到 Haskell

    在 Coq 中 我可以为长度为 n 的列表定义 Church 编码 Definition listn A Type nat gt Type fun m gt forall X nat gt Type X 0 gt forall m A gt

  • Coq QArith 除以零就是零，为什么？

    我注意到在 Coq 的有理数定义中 零的倒数被定义为零 通常 除以零是没有明确定义 合法 允许的 Require Import QArith Lemma inv zero is zero 0 0 Proof unfold Qeq refle

  • Coq：多个构造函数的单一表示法

    是否可以在 Coq 中为多个构造函数定义单一符号 如果构造函数的参数类型不同 则可以从中推断出它们 一个最小的 非 工作示例 Inductive A Set a b c C gt A d D gt A with C Set c1 c2 wi

  • Coq：承认断言

    有没有办法在 Coq 中承认断言 假设我有一个这样的定理 Theorem test forall m n nat m n n m Proof intros n m assert H1 m m n m S n Admitted Abort 上

随机推荐

  • QTableView - 限制所选项目的数量？

    问题就在标题里 没有函数 QTableView set Max Number SelectedItems int 当所选项目的数量为 2 时 我想禁用项目选择 Thanks 您可以通过以下方式禁用选择 connect ui gt table

  • 如何在碰撞后实现超时/冷却

    我一直在做一个pygame两名玩家尝试将球击入网中的游戏 我的游戏中有一个增强功能 但是 我想要一些增强垫 当它们被收集时 我会获得 3 增强 在我下面的代码中 有一个巨大的黄色物体 当有人将鼠标悬停在它上面时 他们会得到提升 但他们可以永

  • 从 URL 安装 conda 包

    在康达 有没有办法直接从 URL 安装包 如下所示 conda install url https anaconda org conda forge pytest 3 4 0 download linux 64 pytest 3 4 0 p

  • 如何让日期时间对象感知（而不是幼稚）

    我需要做什么 我有一个不了解时区的日期时间对象 我需要向其中添加一个时区 以便能够将其与其他时区感知的日期时间对象进行比较 我不想在不知道这一遗留情况的情况下将整个应用程序转换为时区 我尝试过的 首先 演示一下问题 Python 2 6 1

  • Liquibase 无法启动，因为在“迁移文件：类路径”中找不到更改日志

    当我启动应用程序时 它失败并显示以下消息 指出更改日志文件的类路径不存在 Description Liquibase failed to start because no changelog could be found at Migrat

  • 获取今天的 NSDate，时间为 00:00:00

    我正在 Xcode 中编写一个类别 它将扩展当前的 NSDate 类 我想添加两种我经常使用的方法 但不知何故我无法让它们正常工作 目前我有这个代码 NSDate today NSCalendar gregorian NSCalendar

  • Spring Boot中如何设置嵌入式tomcat的日志级别？

    Spring Boot中如何设置嵌入式tomcat的日志级别 特别是我需要查看tomcat集群相关的日志 我将以下行添加到 application properties 中 但 tomcat 似乎只记录 INFO 级别日志 logging

  • Flutter调试release模式，release模式下启用日志

    根据文档我知道 调试信息被删除 调试已禁用 但是我们可以以某种方式强制打印日志 或者在发布模式下进行调试吗 生产应用程序 我正在使用 Android Studio 例如 在 AS 中开发 Android 应用程序时 我们可以打印日志 and

  • PHP lambda 函数和范围

    下面的函数接受一个数组并检查其键和值是否与指定的数据类型匹配 我似乎对之前工作的内部 lambda 函数遇到了一些问题 我正在运行 PHP v5 3 6 他们最后在 v5 3 4 下工作 他们抱怨未传递的变量不在范围内 如果我将该变量重述为

  • 如何使用 uiview 和 uibutton 检测对 Uitableview 单元格的点击？

    我创建了一个表视图 并将自定义 uiview 添加到单元格的内容视图中 uiview 有一个 uibutton 但是 我可以在创建单元格时将 uibutton 添加到内容视图中 我想获取桌面视图上的点击事件来执行某些操作 我还希望 uibu

  • 如何映射或嵌套 Python 2.7 函数生成器？

    如果我在 Python 2 7 中有一个非常简单 尽管可能非常复杂 的函数生成器 如下所示 def accumulator x yield 0 while True x yield x 可以这样使用 gt gt gt a accumulat

  • 如何在firebird sql语句中使用非ascii字符串文字？

    我想在 firebird sql 查询中使用非 ascii 字符串文字 所以我用了火焰知更鸟首先看看它是否有效 我用过这样的东西 SELECT NAME FROM TABLE1 WHERE NAME 我也尝试过 SELECT NAME FR

  • 在 C++ 中传递变量“名称”

    我目前仅使用以下模板作为检查 NULL 指针的方法 如果为 NULL 则将错误消息打印到日志文件 然后返回 false template lt typename T gt static bool isnull T t std string

  • 关于“Hello World”Android 教程的菜鸟问题

    刚刚开始学习 Android 开发和 Java 所以 这是我正在使用的代码 package com example helloandroid import android app Activity import android os Bun

  • 如何让 Eclipse 运行我的所有 Groovy 单元测试？

    我有一个 Eclipse 项目 其中有许多用 Groovy 编写的单元测试 我可以使用 Eclipse 的 GUnit 运行配置在每个单独的类中运行测试 我打开此配置 选择 运行单个测试 单选按钮 然后选择我要运行其测试的类 这工作正常 但

  • Doxygen 速度慢

    Doxygen 在我们的代码库上运行大约需要 12 小时 这主要是因为有大量代码需要处理 约 150 万行 然而 我们很快就无法进行夜间文档更新 因为它们花费的时间太长 我们已经不得不减少图表深度以将其缩短至 12 小时 我已经尝试过标准方

  • 如何在nodejs中将UUID存储为字母数字

    Node uuid提供了一个优秀的包来生成uuid https github com broofa node uuid https github com broofa node uuid Generate a v4 random id uu

  • 是否可以提交一系列不同的工作来进行 slurm ？

    例如 我有一个名为myScript那个过程one输入文件 我有一个文件名列表 也就是说 我需要运行 myScript

  • 我可以在每次除法发生时禁用检查零除法吗？

    为了更好地理解 Rust 的恐慌 异常机制 我编写了以下代码 feature libc extern crate libc fn main let mut x i32 unsafe x libc getchar let y x 65 pri

  • Coqide 错误：编译的库 Basics.vo 对库做出了不一致的假设

    我在 mac os X 上使用 CoqIDE 8 4pl5 当 CoqIDE 转发到此命令时 会弹出此错误消息 需要导入基础知识 错误 编译的库 Basics vo 对库做出了不一致的假设 Coq Init Notifications 当我

热门标签