diff options
| -rw-r--r-- | plugins/extraction/extract_env.ml | 32 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.mli | 4 | ||||
| -rw-r--r-- | plugins/extraction/g_extraction.ml4 | 4 |
3 files changed, 40 insertions, 0 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 7d69cbff1..f5aa5e6c3 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -685,3 +685,35 @@ let structure_for_compute c = let struc = optimize_struct (refs,[]) (mono_environment refs []) in let flatstruc = List.map snd (List.flatten (List.map snd struc)) in flatstruc, ast, mlt + +(* For the test-suite : + extraction to a temporary file + run ocamlc on it *) + +let compile f = + try + let args = ["ocamlc";"-I";Filename.dirname f;"-c";f^"i";f] in + let res = CUnix.sys_command (Envars.ocamlfind ()) args in + match res with + | Unix.WEXITED 0 -> () + | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n -> + CErrors.user_err + Pp.(str "Compilation of file " ++ str f ++ + str " failed with exit code " ++ int n) + with Unix.Unix_error (e,_,_) -> + CErrors.user_err + Pp.(str "Compilation of file " ++ str f ++ + str " failed with error " ++ str (Unix.error_message e)) + +let remove f = + if Sys.file_exists f then Sys.remove f + +let extract_and_compile l = + if lang () != Ocaml then + CErrors.user_err (Pp.str "This command only works with OCaml extraction"); + let f = Filename.temp_file "testextraction" ".ml" in + let () = full_extraction (Some f) l in + let () = compile f in + let () = remove f; remove (f^"i") in + let base = Filename.chop_suffix f ".ml" in + let () = remove (base^".cmo"); remove (base^".cmi") in + Feedback.msg_notice (str "Extracted code successfully compiled") diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index f289b63ad..e10dcd48b 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -17,6 +17,10 @@ val full_extraction : string option -> reference list -> unit val separate_extraction : reference list -> unit val extraction_library : bool -> Id.t -> unit +(* For the test-suite : extraction to a temporary file + ocamlc on it *) + +val extract_and_compile : reference list -> unit + (* For debug / external output via coqtop.byte + Drop : *) val mono_environment : diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 4372ea557..dba1e3444 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -65,6 +65,10 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY (* Monolithic extraction to a file *) | [ "Extraction" string(f) ne_global_list(l) ] -> [ full_extraction (Some f) l ] + +(* Extraction to a temporary file and OCaml compilation *) +| [ "Extraction" "TestCompile" ne_global_list(l) ] + -> [ extract_and_compile l ] END VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY |