From c34154086b3ab19f8f7ab613f42b0333bf90d7d0 Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Mon, 9 Dec 2024 21:47:15 +0100 Subject: [PATCH 1/3] Add IOMode option to forward standard input and output to child process --- plugin/coqsimpleio.mlg.cppo | 6 ++++-- plugin/iOLib.ml | 38 ++++++++++++++++++++++++++++++++++--- plugin/iOLib.mli | 14 +++++++++++++- test/forward/dune | 11 +++++++++++ test/forward/main.expected | 2 ++ test/forward/main.v | 14 ++++++++++++++ 6 files changed, 79 insertions(+), 6 deletions(-) create mode 100644 test/forward/dune create mode 100644 test/forward/main.expected create mode 100644 test/forward/main.v diff --git a/plugin/coqsimpleio.mlg.cppo b/plugin/coqsimpleio.mlg.cppo index 1aae199..33ed6c3 100644 --- a/plugin/coqsimpleio.mlg.cppo +++ b/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 diff --git a/plugin/iOLib.ml b/plugin/iOLib.ml index 3afe8de..cbcbfc8 100644 --- a/plugin/iOLib.ml +++ b/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 diff --git a/plugin/iOLib.mli b/plugin/iOLib.mli index f00e642..38b46d5 100644 --- a/plugin/iOLib.mli +++ b/plugin/iOLib.mli @@ -13,6 +13,18 @@ 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 @@ -20,4 +32,4 @@ 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 diff --git a/test/forward/dune b/test/forward/dune new file mode 100644 index 0000000..be58957 --- /dev/null +++ b/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}))))) diff --git a/test/forward/main.expected b/test/forward/main.expected new file mode 100644 index 0000000..6ba581b --- /dev/null +++ b/test/forward/main.expected @@ -0,0 +1,2 @@ +this is +a test diff --git a/test/forward/main.v b/test/forward/main.v new file mode 100644 index 0000000..215a324 --- /dev/null +++ b/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. From 4785a57c085e60a5b411343e8ad122d1d5328969 Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Mon, 9 Dec 2024 22:01:33 +0100 Subject: [PATCH 2/3] Remove redundant test rules --- test/argv/dune | 4 ---- test/example/dune | 4 ---- test/extraction/dune | 4 ---- test/pervasives/dune | 4 ---- 4 files changed, 16 deletions(-) diff --git a/test/argv/dune b/test/argv/dune index 7a0c4d5..b309dc2 100644 --- a/test/argv/dune +++ b/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))) diff --git a/test/example/dune b/test/example/dune index 8bcac26..9d433ff 100644 --- a/test/example/dune +++ b/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))) diff --git a/test/extraction/dune b/test/extraction/dune index 602d86b..8b695bc 100644 --- a/test/extraction/dune +++ b/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))) diff --git a/test/pervasives/dune b/test/pervasives/dune index 2a57265..977f24c 100644 --- a/test/pervasives/dune +++ b/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))) From 59fc33632e2409efaf80928dc36cab11d9bec1a7 Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Mon, 9 Dec 2024 22:27:56 +0100 Subject: [PATCH 3/3] README: Update --- README.md | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/README.md b/README.md index 8d4544f..9753a6f 100644 --- a/README.md +++ b/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/`.