From 21327e39ef6c6e04569bf8f138d242819139964d Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Tue, 4 Jul 2017 23:15:38 +0200
Subject: Extraction TestCompile foo : a new command for extraction + ocamlc

  Extraction TestCompile foo

 is equivalent to:

  Extraction "/tmp/testextraction1234.ml" foo
  ocamlfind ocamlc -I /tmp -c /tmp/testextraction1234.mli /tmp/testextraction1234.ml

 This command isn't meant for the end user, but rather as an helper
 for test-suite scripts. It only works with extraction to OCaml,
 and the generated code should be standalone.
---
 plugins/extraction/extract_env.ml   | 32 ++++++++++++++++++++++++++++++++
 plugins/extraction/extract_env.mli  |  4 ++++
 plugins/extraction/g_extraction.ml4 |  4 ++++
 3 files changed, 40 insertions(+)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 79d602dbe..45f8d32a3 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -686,3 +686,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 0629a84a0..276c4099d 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -18,6 +18,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 2fa453e53..f4b110253 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -66,6 +66,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
-- 
cgit v1.2.3