CWCompileAndRun (initial implementation)

Author: monadius

README.md

@@ -51,7 +51,7 @@ Run `make .merlin` to create the `.merlin` file.
 
    Test cases cannot be nested.
 
-- `CWEndTest`.
+- `CWEndTest`
 
    Ends a test case. This command is optional before `CWTest` and `CWEndGroup`.
 

src/coq_cw.ml

@@ -1,6 +1,8 @@
 open Pp
 
 let solution_file = "/workspace/Solution.v"
+let ocaml_compiler = "ocamlopt"
+let driver_file = "driver.ml"
 
 let format_msg =
   let re = Str.regexp_string "\n" in
@@ -134,3 +136,21 @@ let test_file_regex ?(fname = solution_file) match_flag regex =
     failed "Bad match";
     CErrors.user_err (str "Bad match")
   end
+
+let run_system_command args =
+  let cmd = String.concat " " args in
+  Printf.printf "Running: %s" cmd;
+  match Unix.system cmd with
+  | Unix.WEXITED 0 -> passed "OK"
+  | _ -> failed "Failed"
+
+let write_file fname str =
+  let oc = open_out fname in
+  Printf.fprintf oc "%s" str;
+  close_out oc
+
+let compile_and_run files ?(options = "") driver_code =
+  write_file driver_file driver_code;
+  run_system_command ([ocaml_compiler; options] @ files @ [driver_file]);
+  run_system_command ["./a.out"];
+  passed "OK"

src/coq_cw.mli

@@ -6,6 +6,8 @@ val test_file_size : ?fname:string -> int -> unit
 
 val test_file_regex : ?fname:string -> bool -> string -> unit
 
+val compile_and_run : string list -> ?options:string -> string -> unit
+
 val begin_group : string -> string -> unit
 
 val end_group : string -> unit

src/g_coq_cw.ml4

@@ -54,4 +54,10 @@ VERNAC COMMAND EXTEND CWFileNegMatch CLASSIFIED AS QUERY
 | [ "CWFile" string_opt(fname) "Does" "Not" "Match" string(regex)] -> [ 
         Coq_cw.test_file_regex ?fname false regex
     ]
-END
+END
+
+VERNAC COMMAND EXTEND CWCompileAndRun CLASSIFIED AS SIDEFF
+| [ "CWCompileAndRun" string_list(files) "Options" string_opt(options) "Driver" string(driver) ] -> [
+        Coq_cw.compile_and_run files ?options driver
+    ]
+END