System effects for Coq.
Coq Shell
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
src
.gitignore
LICENSE
Make
README.md
configure.sh

README.md

IO System

System effects for Coq. See also Coq.io.

Require Import Io.All.
Require Import Io.System.All.
Require Import ListString.All.

Import C.Notations.

Definition hello_world (argv : list LString.t) : C.t System.effect unit :=
  System.log (LString.s "Hello world!").

Install

Using OPAM for Coq:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-io-system

API

See the complete documentation online on v2.3.0.

Extraction

To run a program you can extract it to OCaml. Do:

Definition main := Extraction.launch hello_world.
Extraction "main" main.

You can now compile and execute main.ml:

ocamlbuild main.native -use-ocamlfind -package io-system
./main.native