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的新錯誤。我想：

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文件夾，但沒有成功。任何指針？

Answer 1

新版本的coq:io和coq:io:system庫剛剛發佈。兼營：

opam update 
opam upgrade 

，以確保您的版本至少2.3.0有coq:io:system。現在應該有Extraction.launch。 System.effects已被System.effect所取代。