Library of Unix 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!"). Using OPAM for Coq:
opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-io-system See http://coq.io/.
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