1

我正在关注一个coq HelloWorld 教程（下面的代码），但无法编译该程序。我按照安装步骤安装了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未找到的新错误。我试过了：

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.

我也尝试make在extraction文件夹中，但没有成功。任何指针？

4

1 回答 1

2

coq:io和coq:io:system库的新版本刚刚发布。跑：

opam update
opam upgrade

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

于 2015-06-14T19:43:55.223 回答