Следвах урок за 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, последвах readme в 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, но без успех. Някакви насоки?
