Quelle spawned.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Spawn

let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s
let prerr_endline s = if CDebug.(get_flag misc) then begin pr_err s end else ()

type chandescr = AnonPipe | Socket of string * int * int

let open_bin_connection h pr pw =
  let open Unix in
  let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in
  let cin, _ = open_connection (ADDR_INET (inet_addr_of_string h,pw)) in
  set_binary_mode_in cin true;
  set_binary_mode_out cout true;
  let cin = CThread.prepare_in_channel_for_thread_friendly_io cin in
  cin, cout

let controller h pr pw =
  prerr_endline "starting controller thread";
  let main () =
    let ic, oc = open_bin_connection h pr pw in
    let loop () =
      try
        match CThread.thread_friendly_input_value ic with
        | Hello _ -> prerr_endline "internal protocol error"; exit 1
        | ReqDie -> prerr_endline "death sentence received"; exit 0
      with
      | e ->
        prerr_endline ("control channel broken: " ^ Printexc.to_string e);
        exit 1 in
    loop () in
  ignore(CThread.create main ())

let main_channel = ref None
let control_channel = ref None

let channels = ref None

let init_channels () =
  if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice.");
  let () = match !main_channel with
  | None -> ()
  | Some (Socket(mh,mpr,mpw)) ->
    channels := Some (open_bin_connection mh mpr mpw);
  | Some AnonPipe ->
    let stdin = Unix.in_channel_of_descr (Unix.dup Unix.stdin) in
    let stdout = Unix.out_channel_of_descr (Unix.dup Unix.stdout) in
    Unix.dup2 Unix.stderr Unix.stdout;
    set_binary_mode_in stdin true;
    set_binary_mode_out stdout true;
    let stdin = CThread.prepare_in_channel_for_thread_friendly_io stdin in
    channels := Some (stdin, stdout);
  in
  match !control_channel with
  | None -> ()
  | Some (Socket (ch, cpr, cpw)) ->
    controller ch cpr cpw
  | Some AnonPipe ->
    CErrors.anomaly (Pp.str "control channel cannot be a pipe.")

let get_channels () =
  match !channels with
  | None ->
    Printf.eprintf "Fatal error: ideslave communication channels not set.\n";
    exit 1
  | Some(ic, oc) -> ic, oc

let process_id () =
  Printf.sprintf "%d:%s:%d" (Unix.getpid ())
    (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
     else "master")
    (Thread.id (Thread.self ()))

quality98%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.