Add mode to forward stdin and stdout to RunIO scripts

README.md

@@ -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
@@ -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/`.

plugin/coqsimpleio.mlg.cppo

@@ -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
@@ -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

plugin/iOLib.ml

@@ -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 *)
 
@@ -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
@@ -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
 
@@ -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

plugin/iOLib.mli

@@ -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

test/argv/dune

@@ -7,7 +7,3 @@
 (test
  (name main)
  (flags :standard -w -33-39-67))
-
-(rule
- (alias runtest)
- (action (diff main.expected main.output)))

test/example/dune

@@ -7,7 +7,3 @@
 (test
  (name main)
  (flags :standard -w -33-39-67))
-
-(rule
- (alias runtest)
- (action (diff main.expected main.output)))

test/extraction/dune

@@ -9,7 +9,3 @@
  (name main)
  (libraries unix)
  (flags :standard -w -33-39-67))
-
-(rule
- (alias runtest)
- (action (diff main.expected main.output)))

test/forward/dune

@@ -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})))))

test/forward/main.expected

@@ -0,0 +1,2 @@
+this is
+a test

test/forward/main.v

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

test/pervasives/dune

@@ -7,7 +7,3 @@
 (test
  (name main)
  (flags :standard -w -33-39-67))
-
-(rule
- (alias runtest)
- (action (diff main.expected main.output)))