diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-04 16:50:55 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-04 16:50:55 +0000 |
commit | a99c0dfe6cc3baabc6f4a61103322e1740b020d9 (patch) | |
tree | 7d791b251b5437329db35d7435b3ca239c086e41 /lib/system.ml | |
parent | 1b97f8039cb5fbead0de28425e989345c87ebed4 (diff) |
Ajout d'un processus de communication entre Coq et un outil externe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6677 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/system.ml')
-rw-r--r-- | lib/system.ml | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/lib/system.ml b/lib/system.ml index bbcc9742a..237c9848f 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -182,6 +182,43 @@ let extern_intern magic suffix = in (extern_state,intern_state) +(* Communication through files with another executable *) + +let connect writefun readfun com = + let name = Filename.basename com in + let tmp_to = Filename.temp_file ("coq-"^name^"-in") ".xml" in + let tmp_from = Filename.temp_file ("coq-"^name^"-out") ".xml" in + let ch_to_in,ch_to_out = + try open_in tmp_to, open_out tmp_to + with Sys_error s -> error ("Cannot set connection to "^com^"("^s^")") in + let ch_from_in,ch_from_out = + try open_in tmp_from, open_out tmp_from + with Sys_error s -> + close_out ch_to_out; close_in ch_to_in; + error ("Cannot set connection from "^com^"("^s^")") in + let pid = + let ch_to' = Unix.descr_of_in_channel ch_to_in in + let ch_from' = Unix.descr_of_out_channel ch_from_out in + try Unix.create_process com [||] ch_to' ch_from' Unix.stdout + with Unix.Unix_error (err,_,_) -> + close_in ch_to_in; + close_out ch_to_out; + close_in ch_from_in; + close_out ch_from_out; + error ("Cannot execute "^com^"("^(Unix.error_message err)^")") in + writefun ch_to_out; + close_out ch_to_out; + close_in ch_to_in; + close_out ch_from_out; + (match snd (Unix.waitpid [] pid) with + | Unix.WEXITED 127 -> error (com^": cannot execute") + | Unix.WEXITED 0 -> () + | _ -> error (com^" exited abnormally")); + let a = readfun ch_from_in in + close_in ch_from_in; + unlink tmp_from; + unlink tmp_to; + a (* Time stamps. *) |