From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.0 required=5.0 tests=DNS_FROM_RFC_ABUSE, NO_REAL_NAME autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 9D456BBAF for ; Thu, 30 Jul 2009 16:56:21 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgEDANdRcUqGdRUV/2dsb2JhbACZDro/hBEF X-IronPort-AV: E=Sophos;i="4.43,295,1246831200"; d="scan'208";a="44154381" Received: from pegasus.math.carleton.ca ([134.117.21.21]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 30 Jul 2009 16:56:21 +0200 Received: from pegasus.carleton.ca (pegasus.carleton.ca [127.0.0.1]) by pegasus.math.carleton.ca (Postfix) with ESMTP id 642CE7FCB8C for ; Thu, 30 Jul 2009 10:56:17 -0400 (EDT) Received: from 134.117.101.64 (SquirrelMail authenticated user kcheung) by pegasus.carleton.ca with HTTP; Thu, 30 Jul 2009 10:56:17 -0400 (EDT) Message-ID: <51472.134.117.101.64.1248965777.squirrel@pegasus.carleton.ca> Date: Thu, 30 Jul 2009 10:56:17 -0400 (EDT) Subject: HOL Light on ocamlnat From: kcheung@math.carleton.ca To: caml-list@inria.fr User-Agent: SquirrelMail/1.4.8-4.0.1.el4 MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Priority: 3 (Normal) Importance: Normal X-Spam: no; 0.00; speedup:01 computations:01 carleton:98 carleton:98 cheung:98 preliminary:03 experiments:03 loading:05 hol:10 hol:10 announce:12 www:84 observed:18 light:19 light:19 I am pleased to announce that experiments on loading HOL Light in ocamlnat have been successful. A 4x to 10x speedup on various computations has been observed. A preliminary how-to guide is available at: http://www.math.carleton.ca/~kcheung/holnat.html Kevin Cheung.