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 6D2C7BBC4 for ; Fri, 20 Jan 2006 21:19:55 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0KKJsfd002155 for ; Fri, 20 Jan 2006 21:19:55 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id VAA02810 for ; Fri, 20 Jan 2006 21:19:54 +0100 (MET) Received: from orsfmr002.jf.intel.com (fmr17.intel.com [134.134.136.16]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k0KKJp6J002147 for ; Fri, 20 Jan 2006 21:19:53 +0100 Received: from orsfmr101.jf.intel.com (orsfmr101.jf.intel.com [10.7.209.17]) by orsfmr002.jf.intel.com (8.12.10/8.12.10/d: major-outer.mc,v 1.1 2004/09/17 17:50:56 root Exp $) with ESMTP id k0KKJo8i004882; Fri, 20 Jan 2006 20:19:50 GMT Received: from orsmsxvs041.jf.intel.com (orsmsxvs041.jf.intel.com [192.168.65.54]) by orsfmr101.jf.intel.com (8.12.10/8.12.10/d: major-inner.mc,v 1.2 2004/09/17 18:05:01 root Exp $) with SMTP id k0KKJBNk011826; Fri, 20 Jan 2006 20:19:50 GMT Received: from orsmsx332.amr.corp.intel.com ([192.168.65.60]) by orsmsxvs041.jf.intel.com (SAVSMTP 3.1.7.47) with SMTP id M2006012012194910539 ; Fri, 20 Jan 2006 12:19:49 -0800 Received: from orsmsx409.amr.corp.intel.com ([192.168.65.58]) by orsmsx332.amr.corp.intel.com with Microsoft SMTPSVC(6.0.3790.211); Fri, 20 Jan 2006 12:19:49 -0800 X-MimeOLE: Produced By Microsoft Exchange V6.5 Content-class: urn:content-classes:message MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable Subject: RE: [Caml-list] toplevel with pre-installed printers Date: Fri, 20 Jan 2006 12:19:48 -0800 Message-ID: <196F1D996F92CD46A542EA519DB8CE4702F0D2D7@orsmsx409> Thread-Topic: [Caml-list] toplevel with pre-installed printers Thread-Index: AcYdYXaF7Sj0HNb7TumiE7b8AI0o5gAm6f5Q From: "Harrison, John R" To: "skaller" Cc: "Caml list" X-OriginalArrivalTime: 20 Jan 2006 20:19:49.0748 (UTC) FILETIME=[DD3FC340:01C61DFE] X-Scanned-By: MIMEDefang 2.52 on 10.7.209.17 X-Miltered: at concorde with ID 43D145EA.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43D145E7.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 toplevel:01 johnh:01 variants:01 bytecode:01 theorems:01 bytecode:01 theorems:01 marshalling:01 restructure:98 proofs:01 data:02 ichips:02 tightly:02 latter:03 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 | Under "Linux" ckpt is not available. I tried this, since HOL Light takes | ages to load. I even tried to build ckpt from source with no luck. | Maybe it works for x86 .. but I'm running an x86_64. I wasn't aware of that problem. It works fine on 32-bit x86, though there are some peculiarities of certain Linux variants. I'll look into this, since I suppose I'll want it myself one day. | Is there some reason HOL Light doesn't load bytecode? It's not so much the code (of automated proof procedures etc.) that slows the load down, but actually running the proofs to arrive at the basic core of theorems. Loading as bytecode won't help that significantly. It would be possible to restructure the code to completely separate data (theorems) from code (proof procedures), load the former via marshalling and the latter as bytecode. But it's not very natural to do so, since one often wants to introduce theorems and proof procedures in a tightly interleaved manner. John.