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, убунту 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 были только что выпущены. Run:

opam update 
opam upgrade 

, чтобы убедиться, что у вас есть coq:io:system в версии 2.3.0, по крайней мере. Теперь должно быть доступно Extraction.launch. System.effects был заменен на System.effect.