aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-26 14:32:59 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-26 14:32:59 +0200
commita0214d53a9a7fa1dc47375c7f048a15bed5dc523 (patch)
treeea0d69995fb8f4fc5ee9865e24afd513e4222dae
parentc50f5c4655e29989fb4b15c7e391bfb38785b251 (diff)
parent21327e39ef6c6e04569bf8f138d242819139964d (diff)
Merge PR #859: Extraction TestCompile
-rw-r--r--plugins/extraction/extract_env.ml32
-rw-r--r--plugins/extraction/extract_env.mli4
-rw-r--r--plugins/extraction/g_extraction.ml44
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