diff options
| author | Prashanth Mundkur | 2018-05-21 15:24:18 -0700 |
|---|---|---|
| committer | Prashanth Mundkur | 2018-05-21 18:00:03 -0700 |
| commit | b55481d0bafff8520ff6872dbca4ca616bce41ac (patch) | |
| tree | 89182de9bea9e46c9997e3a7cb09899f80b5bd7b /src | |
| parent | 1eb48633540df90e8f357ccc00039062ddea3ae1 (diff) | |
Add an -ocaml-nobuild option to avoid building the generated ocaml by default (off by default).
Diffstat (limited to 'src')
| -rw-r--r-- | src/ocaml_backend.ml | 14 | ||||
| -rw-r--r-- | src/sail.ml | 4 |
2 files changed, 13 insertions, 5 deletions
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 4a1007c3..91cd288b 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -58,6 +58,8 @@ module Big_int = Nat_big_num (* Option to turn tracing features on or off *) let opt_trace_ocaml = ref false +(* Option to not build generated ocaml by default *) +let opt_ocaml_nobuild = ref false type ctx = { register_inits : tannot exp list; @@ -709,10 +711,12 @@ let ocaml_compile spec defs = let out_chan = open_out "main.ml" in output_string out_chan (ocaml_main spec sail_dir); close_out out_chan; - system_checked "ocamlbuild -use-ocamlfind main.native"; - let _ = Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec) in - () + if not !opt_ocaml_nobuild then ( + system_checked "ocamlbuild -use-ocamlfind main.native"; + ignore (Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec)) + ) end - else - system_checked ("ocamlbuild -use-ocamlfind " ^ spec ^ ".cmo"); + else (if not !opt_ocaml_nobuild then + system_checked ("ocamlbuild -use-ocamlfind " ^ spec ^ ".cmo") + ); Unix.chdir cwd diff --git a/src/sail.ml b/src/sail.ml index f459d774..5f9b0f05 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -60,6 +60,7 @@ let opt_print_verbose = ref false let opt_print_lem_ast = ref false let opt_print_lem = ref false let opt_print_ocaml = ref false +let opt_ocaml_nobuild = ref false let opt_print_c = ref false let opt_print_latex = ref false let opt_print_coq = ref false @@ -88,6 +89,9 @@ let options = Arg.align ([ ( "-ocaml", Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen], " output an OCaml translated version of the input"); + ( "-ocaml-nobuild", + Arg.Set Ocaml_backend.opt_ocaml_nobuild, + " do not build generated ocaml"); ( "-ocaml_trace", Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen; Arg.Set Ocaml_backend.opt_trace_ocaml], " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml"); |