Skip to content

Commit

Permalink
Add mode to forward stdin and stdout to RunIO scripts (#78)
Browse files Browse the repository at this point in the history
  • Loading branch information
Lysxia authored Dec 11, 2024
1 parent de32ccf commit 59ca9ed
Show file tree
Hide file tree
Showing 11 changed files with 107 additions and 22 deletions.
28 changes: 28 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -128,6 +128,29 @@ Definition main : IO unit :=
RunIO main.
```

### Run as a command-line script

You can run a `.v` file from the command line with `coqc`.
To forward stdin and stdout to your `RunIO` scripts,
set the option `RunIO IOMode Forward`.

```coq
From SimpleIO Require Import SimpleIO.
Import IO.Notations.
RunIO IOMode Forward.
Definition cat : IO unit :=
_ <- catch_eof
(IO.fix_io (fun f _ =>
input <- read_line ;;
print_endline input ;;
f tt :> IO unit) tt) ;;
IO.ret tt.
RunIO cat.
```

### Configuration

```coq
Expand Down Expand Up @@ -163,6 +186,11 @@ RunIO Smart On.
RunIO Smart Off.
```

New `RunIO` options may be added in the future.
To avoid risks of future collisions with the main `RunIO` command,
use names with a lower case initial (like `RunIO main`),
or put the action name in parentheses (like `RunIO (Builder)` to run the `IO` action `Builder`).

## Library organization

The source code can be found under `src/`.
Expand Down
6 changes: 4 additions & 2 deletions plugin/coqsimpleio.mlg.cppo
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,8 @@ let run c =
#else
let opaque_access = () in
#endif
Feedback.msg_info (Pp.str ("Running " ^ string_of_constr_expr c ^ " ..."));
run ~plugin_name:"coq_simple_io" ~opaque_access
let name = string_of_constr_expr c in
run ~plugin_name:"coq_simple_io" ~opaque_access ~name
(CAst.make @@ apply_constr run_ast [c])

let string_unopt = function
Expand All @@ -37,4 +37,6 @@ VERNAC COMMAND EXTEND RunIO CLASSIFIED AS SIDEFF
| ["RunIO" "Smart" "On"] -> { smart_mode := true }
| ["RunIO" "Smart" "Off"] -> { smart_mode := false }
| ["RunIO" "Reset"] -> { IOLib.reset () }
| ["RunIO" "IOMode" "Repl"] -> { io_mode := Repl }
| ["RunIO" "IOMode" "Forward"] -> { io_mode := Forward }
END
38 changes: 35 additions & 3 deletions plugin/iOLib.ml
Original file line number Diff line number Diff line change
Expand Up @@ -34,12 +34,22 @@ let add_module_to_open s = modules_to_open := s :: !modules_to_open
let smart_mode : bool ref =
Summary.ref ~name:"runio_smart_mode" true

type io_mode
= Repl
(** Default mode compatible with interactive Coq sessions *)
| Forward
(** Forward stdin,stdout,stderr to the child processes running the extracted
programs. This option lets you run [RunIO] scripts from the command line. *)

let io_mode = Summary.ref ~name:"runio_io_mode" Repl

let reset () =
builder := Ocamlfind "";
extra_dir := [];
extra_pkg := [];
modules_to_open := [];
smart_mode := true
smart_mode := true;
io_mode := Repl

(** * General helper functions *)

Expand Down Expand Up @@ -261,7 +271,7 @@ let compile dir mlif mlf =
dir execn opts);
dir </> "_build/default" </> execn ^ ".exe"

let run_exec execn =
let run_exec_repl execn =
let (p_out, _, p_err) as process = Unix.open_process_full execn (Unix.environment ()) in
let rec process_otl_aux () =
let e = input_line p_out in
Expand All @@ -279,6 +289,22 @@ let run_exec execn =
| Unix.WSTOPPED i -> err (Printf.sprintf "Stopped (%d)" i)
end

let run_exec_forward execn =
let pid = Unix.create_process execn [|execn|] Unix.stdin Unix.stdout Unix.stderr in
let _, status = Unix.waitpid [] pid in
let err descr = CErrors.user_err (str (execn ^ ": " ^ descr) ++ fnl ()) in
begin match status with
| Unix.WEXITED 0 -> ()
| Unix.WEXITED i -> err (Printf.sprintf "Exited with status %d" i)
| Unix.WSIGNALED i -> err (Printf.sprintf "Killed (%d)" i)
| Unix.WSTOPPED i -> err (Printf.sprintf "Stopped (%d)" i)
end

let run_exec execn =
match !io_mode with
| Repl -> run_exec_repl execn
| Forward -> run_exec_forward execn

let compile_and_run dir mlif mlf =
compile dir mlif mlf |> run_exec

Expand Down Expand Up @@ -309,7 +335,13 @@ let define_and_run ~plugin_name ~opaque_access env evd term =
let term = define env evd term in
extract_and_run ~plugin_name ~opaque_access term

let run ~plugin_name ~opaque_access term =
let chatty () =
match !io_mode with
| Repl -> true
| Forward -> false

let run ~plugin_name ~opaque_access ~name term =
if chatty () then Feedback.msg_info (Pp.str ("Running " ^ name ^ " ..."));
let env = Global.env () in
let evd = Evd.from_env env in
let (term,_) = interp_constr env evd term in
Expand Down
14 changes: 13 additions & 1 deletion plugin/iOLib.mli
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,23 @@ val add_module_to_open : string -> unit
(* Automatically insert common dependencies (zarith, coq-simple-io.extraction).
[true] by default. *)
val smart_mode : bool ref

(** Option for handling standard input and output *)
type io_mode
= Repl
(** Default mode compatible with interactive Coq sessions *)
| Forward
(** Forward stdin,stdout,stderr to the child processes running the extracted
programs. This option lets you run [RunIO] scripts from the command line. *)

(** See [type io_mode] above. *)
val io_mode : io_mode ref

val reset : unit -> unit

val apply_constr : constr_expr -> constr_expr list -> constr_expr_r
val mk_ref : string -> constr_expr
val string_of_constr_expr : constr_expr -> string
val define_and_run : plugin_name:string -> opaque_access:Compat.indirect_accessor ->
Environ.env -> Evd.evar_map -> Evd.econstr -> unit
val run : plugin_name:string -> opaque_access:Compat.indirect_accessor -> constr_expr -> unit
val run : plugin_name:string -> opaque_access:Compat.indirect_accessor -> name:string -> constr_expr -> unit
4 changes: 0 additions & 4 deletions test/argv/dune
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,3 @@
(test
(name main)
(flags :standard -w -33-39-67))

(rule
(alias runtest)
(action (diff main.expected main.output)))
4 changes: 0 additions & 4 deletions test/example/dune
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,3 @@
(test
(name main)
(flags :standard -w -33-39-67))

(rule
(alias runtest)
(action (diff main.expected main.output)))
4 changes: 0 additions & 4 deletions test/extraction/dune
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,3 @@
(name main)
(libraries unix)
(flags :standard -w -33-39-67))

(rule
(alias runtest)
(action (diff main.expected main.output)))
11 changes: 11 additions & 0 deletions test/forward/dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
(rule
(alias runtest)
(action (diff main.expected main.output)))

(rule
(deps (package coq-simple-io))
(action
(with-stdout-to main.output
(pipe-stdout
(run echo "this is\na test")
(run %{bin:coqc} -I ../../plugin -Q ../../src SimpleIO %{dep:main.v})))))
2 changes: 2 additions & 0 deletions test/forward/main.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
this is
a test
14 changes: 14 additions & 0 deletions test/forward/main.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
From SimpleIO Require Import SimpleIO.
Import IO.Notations.

RunIO IOMode Forward.

Definition cat : IO unit :=
_ <- catch_eof
(IO.fix_io (fun f _ =>
input <- read_line ;;
print_endline input ;;
f tt :> IO unit) tt) ;;
IO.ret tt.

RunIO cat.
4 changes: 0 additions & 4 deletions test/pervasives/dune
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,3 @@
(test
(name main)
(flags :standard -w -33-39-67))

(rule
(alias runtest)
(action (diff main.expected main.output)))

0 comments on commit 59ca9ed

Please sign in to comment.