CODEWITHSUNDEEP
coqopam
thor
thor

Reputation: 22480

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

I was following a coq HelloWorld tutorial (code below), and couldn't get the program to compile. I followed the installation steps and installed opam install coq:io:system. My opam installation is at the default location ~/.opam. But still, I got an error about 

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

This is with either emacs/proofgeneral or coqide (8.4pl6, ubuntu 14.04). Does any one know how to fix the issue?

Here's the code which I copied into a file called hello_world.v and loaded into 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!").

-- Update ---

@gtzinos, I followed the readme in https://github.com/clarus/coq-hello-world. This time there was no complaint about System.effects, but there was a new error about Extraction.launch not found. I tried:

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

and got:

"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.

I tried also to make in the extraction folder, but without success. Any pointers?

Upvotes: 1

Views: 711

Answers (1)

Clarus
Clarus

Reputation: 178

New versions of the coq:io and coq:io:system libraries were just released. Run:

opam update
opam upgrade

to make sure you have coq:io:system in version at least 2.3.0. Now Extraction.launch should be available. System.effects has been replaced by System.effect.

Upvotes: 2

Related Questions