From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 20493BBA7 for ; Sun, 5 Feb 2006 20:09:34 +0100 (CET) Received: from vms042pub.verizon.net (vms042pub.verizon.net [206.46.252.42]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k15J9XoU021973 for ; Sun, 5 Feb 2006 20:09:33 +0100 Received: from Nodens ([71.255.34.244]) by vms042.mailsrvcs.net (Sun Java System Messaging Server 6.2-4.02 (built Sep 9 2005)) with ESMTPA id <0IU800JULAJS2PB8@vms042.mailsrvcs.net> for caml-list@yquem.inria.fr; Sun, 05 Feb 2006 13:09:32 -0600 (CST) Date: Sun, 05 Feb 2006 14:09:37 -0500 From: "Stephen Brackin" Subject: Sharing time between two computations? To: Message-id: <0IU800JUPAJW2PB8@vms042.mailsrvcs.net> MIME-version: 1.0 X-MIMEOLE: Produced By Microsoft MimeOLE V6.00.2900.2180 X-Mailer: Microsoft Office Outlook, Build 11.0.6353 Content-type: multipart/alternative; boundary="----=_NextPart_000_0000_01C62A5D.CCA701E0" Thread-index: AcYqh7TmbkQUz8NVTJ+3PUCyR1MpqQ== X-Miltered: at concorde with ID 43E64D6D.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; computations:01 ocaml:01 computations:01 more-or-less:01 ocaml:01 more-or-less:01 computed:01 computed:01 verizon:98 iym:98 theorem:01 theorem:01 expression:01 expression:01 computation:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.8 required=5.0 tests=DNS_FROM_RFC_ABUSE, DNS_FROM_RFC_POST,HTML_50_60,HTML_MESSAGE autolearn=disabled version=3.0.3 This is a multi-part message in MIME format. ------=_NextPart_000_0000_01C62A5D.CCA701E0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Xavier Leroy showed me how to set things up so that an OCaml computation is interrupted after a pre-set time limit to ask the user how long to continue. Now I'd like to do the same thing for two parallel computations that I'd like to have share the time available more-or-less evenly. (I'm writing OCaml code for automatically proving results in the HOL Light theorem prover, and I have a situation where the code needs to prove that a value is positive or prove that it's negative, but the code doesn't know which, if either, it will be able to prove.) Can this be done? If so, then what's the easiest way to do it? As a special case of this question, for an expression of the form "let x,y = f(args1),g(args2)", how does the system allocate time between the computation of x and y? (If it's more-or-less equally, then that solves my problem; if one of x or y is computed first, then the other, then I've still got a problem.) Steve Brackin ------=_NextPart_000_0000_01C62A5D.CCA701E0 Content-Type: text/html; charset="us-ascii" Content-Transfer-Encoding: quoted-printable

Xavier Leroy showed me how = to set things up so that an OCaml computation is interrupted after a pre-set = time limit to ask the user how long to continue. Now I’d like to do the = same thing for two parallel computations that I’d like to have share = the time available more-or-less evenly. (I’m writing OCaml code for = automatically proving results in the HOL Light theorem prover, and I have a situation = where the code needs to prove that a value is positive or prove that = it’s negative, but the code doesn’t know which, if either, it will be = able to prove.) Can this be done? If so, then what’s the easiest way to do = it? As a special case of this question, for an expression of the form = “let x,y =3D f(args1),g(args2)”, how does the system allocate time between the computation of x and y? (If it’s more-or-less equally, then that = solves my problem; if one of x or y is computed first, then the other, then = I’ve still got a problem.)

Steve = Brackin

------=_NextPart_000_0000_01C62A5D.CCA701E0--