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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id ECD737EE4B for ; Wed, 2 Oct 2013 20:53:17 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of david.mentre@gmail.com) identity=pra; client-ip=74.125.82.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="david.mentre@gmail.com"; x-sender="david.mentre@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of david.mentre@gmail.com designates 74.125.82.181 as permitted sender) identity=mailfrom; client-ip=74.125.82.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="david.mentre@gmail.com"; x-sender="david.mentre@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-we0-f181.google.com) identity=helo; client-ip=74.125.82.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="david.mentre@gmail.com"; x-sender="postmaster@mail-we0-f181.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8BAOVqTFJKfVK1m2dsb2JhbABZgz/DEBYOAQEBAQEGCwsJFCiCJQEBBAE4CAE3AQEDAQsBBQUhFg8JAwIBAgENFQEFARwGDQEHAQGHcAMJBgSfM49chEEnDYlkAQUMk28Djk6KYoUGiV9BgWOCbQ X-IPAS-Result: Ao8BAOVqTFJKfVK1m2dsb2JhbABZgz/DEBYOAQEBAQEGCwsJFCiCJQEBBAE4CAE3AQEDAQsBBQUhFg8JAwIBAgENFQEFARwGDQEHAQGHcAMJBgSfM49chEEnDYlkAQUMk28Djk6KYoUGiV9BgWOCbQ X-IronPort-AV: E=Sophos;i="4.90,1020,1371074400"; d="scan'208";a="35305912" Received: from mail-we0-f181.google.com ([74.125.82.181]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 02 Oct 2013 20:53:16 +0200 Received: by mail-we0-f181.google.com with SMTP id p61so1419748wes.26 for ; Wed, 02 Oct 2013 11:53:17 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=sender:message-id:date:from:user-agent:mime-version:to:cc:subject :references:in-reply-to:content-type:content-transfer-encoding; bh=RORm8rgWPSskIrS0A+CvedFAbMUmj0RnMhRLMMPHLpQ=; b=ZgO/HPQMoByhpY2qzARpjj5TaBooflRfuhiUdpn5+15KdUOwXYPgtxWpoQts10YltC J6Os89P2nQuEwxQ3y7/tpYlLJePLydNFEj+ZkoH1eA1yc7z+UefYU18zHgUsE13UvLE/ rWNZgK/LLOc0E+boRMr95BTJ3t6nzCS+Jwdx0MkDaAXaL0OKUxYQnzu6wQbxTc72qYVz PpL65LvYctyFr+ZpDYsq0N5i4qfmEbvbins/TURLp6bJz/CAPcXV9/1DgTVGrdnpFJO7 B6ZUs+2WA4gUtzxznOgRPE2kPTRVV33Ve68DNCuDJxw/plYB1sTn2pgh+LB4E4W0hw3E e9gw== X-Received: by 10.180.72.148 with SMTP id d20mr3382833wiv.21.1380739997180; Wed, 02 Oct 2013 11:53:17 -0700 (PDT) Received: from [192.168.0.20] (abo-223-43-68.mts.modulonet.fr. [85.68.43.223]) by mx.google.com with ESMTPSA id mw9sm7918845wib.0.1969.12.31.16.00.00 (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Wed, 02 Oct 2013 11:53:16 -0700 (PDT) Sender: David MENTRE Message-ID: <524C6B99.5040806@linux-france.org> Date: Wed, 02 Oct 2013 20:53:13 +0200 From: =?ISO-8859-1?Q?David_MENTR=C9?= User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0 MIME-Version: 1.0 To: Gabriel Scherer CC: caml users References: In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] OCaml editor running tests or other tasks in background? Hello, 2013-10-02 19:06, Gabriel Scherer: > I think the most advanced project regarding IDE integration nowadays is > Merlin ( https://github.com/def-lkb/merlin ), which gives direct > feedback on syntax and typing errors. It doesn't have any knowledge of > unit tests or coverage checking, but it would probably be the right tool > to start with to integrate such a feature. Thanks for the pointer. > Note that there has been a bit of back-and-forth on the instant feedback > feature. Previous iterations were deemed a bit too visually invasive, > and some people don't like to risk being interrupted by their IDE while > they think about their code. I think it's always better to have the > feature available, but there is clearly some tuning to have, and > potential for overdoing it. I've only seen demos and never used this feature a lot. You probably right that such a feature should be correctly tuned. > The other project that jumps to mind is the Why3 IDE ( > http://why3.lri.fr/ ). It seems they're not hype enough to have video > stuff available, but from what I remember the GUI does a pretty good job > of giving feedback on how external provers run, and pieces of code that > were previously verified and aren't anymore. I've used Why3 IDE on a regular basis. This IDE is far from what I am looking for because one needs to do explicit actions to launch the provers. And Why3 IDE is focused on VCs, not the original source code (event if the code is displayed). Ideally, one would edit a WhyML file in an editor and the proved VC would be displayed automatically, like in Dafny. In fact the purpose of an editor I'm looking for would be to hide as much as possible the machinery to generate VC, launch provers, etc., from the user (and the same for test, doc generation, etc.). After all, when we call a compiler, we don't really care if the compiler, assembler or linker are needed and the files exchanged between them. Best regards, david