From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by sympa.inria.fr (Postfix) with ESMTPS id 3EA727EEAF for ; Thu, 17 Jan 2013 20:36:07 +0100 (CET) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of benedikt.meurer@googlemail.com) identity=pra; client-ip=209.85.214.51; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="benedikt.meurer@googlemail.com"; x-sender="benedikt.meurer@googlemail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail4-smtp-sop.national.inria.fr: domain of benedikt.meurer@googlemail.com designates 209.85.214.51 as permitted sender) identity=mailfrom; client-ip=209.85.214.51; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="benedikt.meurer@googlemail.com"; x-sender="benedikt.meurer@googlemail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-bk0-f51.google.com) identity=helo; client-ip=209.85.214.51; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="benedikt.meurer@googlemail.com"; x-sender="postmaster@mail-bk0-f51.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap4BAC9R+FDRVdYzjWdsb2JhbABFvioWDgEBAQEJCQsJEgYjgh4BAQQBQAEtCwEDAQsGBQspEiETAQUBHAYTiAYBAwkGBAidS48vhQMKQA2ILAEFDIt8hE9hA5Q2gVaLN4MxP4QY X-IronPort-AV: E=Sophos;i="4.84,486,1355094000"; d="scan'208";a="168841299" Received: from mail-bk0-f51.google.com ([209.85.214.51]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 17 Jan 2013 20:34:14 +0100 Received: by mail-bk0-f51.google.com with SMTP id ik5so1595245bkc.24 for ; Thu, 17 Jan 2013 11:34:14 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=x-received:content-type:mime-version:subject:from:in-reply-to:date :cc:content-transfer-encoding:message-id:references:to:x-mailer; bh=q6H6iRVtpATxw+3mwYVL3ZqI8xbyHPlQMs6bwE7e9VE=; b=U7gLUB2JWAf1ZRKHFTT4sdQaGswt5HkwaWcM/cqhX4shIeZjiJeyalN5343O8IQVYM gOqd3+S6qLfuE+cBkjHozY1F/o6MAxVk8eAeatdDEMvtxwFLD2xuNOvLsFfUyiGtaGac T1s5uYvmFHOWedit6jbE5J/tXn712FpDy8xwEfekaf1b3nDZ0LcJp8F9TWmmoBsd4s3O Y6f9BehSUIjsIVMz+brTNUOF419tSk3qOjDJcU8cTdtF5lljhzKLlEXR2/6TcpToNgW1 3zY7kNCELQXsNdxubvMyMoS1IKGbwKQWZQ4RWy9VoA4j1qHJGrQs7hzUPeQZJ293TTGV QBjg== X-Received: by 10.204.127.27 with SMTP id e27mr1865947bks.126.1358451254145; Thu, 17 Jan 2013 11:34:14 -0800 (PST) Received: from tatooine.in.benediktmeurer.de (sign-4db6a4ec.pool.mediaWays.net. [77.182.164.236]) by mx.google.com with ESMTPS id c10sm2321921bkw.1.2013.01.17.11.34.12 (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Thu, 17 Jan 2013 11:34:13 -0800 (PST) Content-Type: text/plain; charset=iso-8859-1 Mime-Version: 1.0 (Mac OS X Mail 6.2 \(1499\)) From: Benedikt Meurer In-Reply-To: Date: Thu, 17 Jan 2013 20:34:11 +0100 Cc: Benedikt Meurer , Basile Starynkevitch , Gerd Stolpmann , Francois Berenger , caml-list@inria.fr Content-Transfer-Encoding: quoted-printable Message-Id: <15399729-F0F8-49B8-B1DD-D06F127F8E78@gmail.com> References: <43fbc889-f7fc-4bd6-949b-634d478326f6@googlegroups.com> <50F66B57.3070601@riken.jp> <1358326866.28639.13@samsung> <20130116094800.GA9538@ours.starynkevitch.net> <610FAC34-EFC6-411F-87B7-03CA021E5C8E@gmail.com> To: Gabriel Scherer X-Mailer: Apple Mail (2.1499) Subject: Re: [Caml-list] ocamlc compiles hello world, ocamlopt not On Jan 17, 2013, at 0:17 , Gabriel Scherer wrot= e: > Benedikt, let me jump on the occasion to provide more pointers you > might be interested in: >=20 > - Rapha=EBl Amiard, a student at Paris 6 university, recently worked on > translating OCaml byte into LLVM: > https://github.com/raph-amiard/CamllVM ; I have not seen a definite > comparison with Colin's and Benoit's work, but they appear to hit the > same kind of issues (performance degradation of exceptions, handling > GC roots that are passed in registers) Yeah, I've seen that earlier on the mailinglist. > - VeriML is a research language for writing tactics and proof > assistants; developed at Yale during Antonis Stampoulis recently > finished thesis ( http://www.cs.yale.edu/homes/stampoulis/ ); they > have a HOL-like mode of interaction, where the user-interface to the > prover is directly a toplevel (forked from OCaml's toplevel), and they > use OCamlJIT2 to provide good performances within this model. That sounds interesting. And it would certainly benefit from a trace-based = JITter. :-) Benedikt=