coq Hello World 示例（带有 opam）找不到库

Question

我正在跟踪 coq HelloWorld tutorial（下面的代码），但无法编译程序。我按照安装步骤安装了opam install coq:io:system。我的 opam 安装在默认位置 ~/.opam。但是，我仍然收到关于

的错误

Toplevel input, characters 53-67:
Error: The reference System.effects was not found in the current environment.

这是 emacs/proofgeneral 或 coqide (8.4pl6, ubuntu 14.04)。有人知道如何解决这个问题吗？

这是我复制到名为 hello_world.v 并加载到 emacs/coqide 的文件中的代码：

Require Import Coq.Lists.List.
Require Import Io.All.
Require Import Io.System.All.
Require Import ListString.All.

Import ListNotations.
Import C.Notations.

(** The classic Hello World program. *)
Definition hello_world (argv : list LString.t) : C.t System.effects unit :=
  System.log (LString.s "Hello world!").

-- 更新 ---

@gtzinos，我遵循了 https://github.com/clarus/coq-hello-world 中的自述文件。这次没有关于 System.effects 的投诉，但是出现了关于 Extraction.launch not found 的新错误。我试过了：

git clone https://github.com/clarus/coq-hello-world.git
cd coq-hello-world
./configure.sh && make

并得到：

"coqc"  -q  -R src HelloWorld   src/Main
File "/.../coq-hello-world/src/Main.v", line 32, characters 19-36:
Error: The reference Extraction.launch was not found in the current
environment.

我也尝试在 extraction 文件夹中 make，但没有成功。有什么指点吗？

Answer 1

coq:io 和 coq:io:system 库的新版本刚刚发布。运行:

opam update
opam upgrade

确保您的 coq:io:system 版本至少为 2.3.0。现在 Extraction.launch 应该可用了。 System.effects 已替换为 System.effect。

coq Hello World 示例（带有 opam）找不到库

coq Hello World example (with opam) can't find libraries

coq

opam