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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id A27667EE4B for ; Wed, 2 Oct 2013 20:57:47 +0200 (CEST) Received-SPF: Neutral (mail3-smtp-sop.national.inria.fr: domain of simon.cruanes.2007@m4x.org does not assert whether or not 129.104.30.34 is permitted sender) identity=pra; client-ip=129.104.30.34; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="SRS0=jblY=TM=m4x.org=simon.cruanes.2007@bounces.m4x.org"; x-sender="simon.cruanes.2007@m4x.org"; x-conformance=sidf_compatible; x-record-type="spf2.0" Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of SRS0=jblY=TM=m4x.org=simon.cruanes.2007@bounces.m4x.org designates 129.104.30.34 as permitted sender) identity=mailfrom; client-ip=129.104.30.34; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="SRS0=jblY=TM=m4x.org=simon.cruanes.2007@bounces.m4x.org"; x-sender="SRS0=jblY=TM=m4x.org=simon.cruanes.2007@bounces.m4x.org"; x-conformance=sidf_compatible; x-record-type="spf2.0" Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of postmaster@mx1.polytechnique.org designates 129.104.30.34 as permitted sender) identity=helo; client-ip=129.104.30.34; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="SRS0=jblY=TM=m4x.org=simon.cruanes.2007@bounces.m4x.org"; x-sender="postmaster@mx1.polytechnique.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsQBAA9sTFKBaB4inGdsb2JhbABZgz+De7hBhlUWDgEBAQEBBhYJPIIlAQEEASNWBQsLISECAg8FKCGIEwYEqyiSORaNbIRAgTkDmACBMJN2 X-IPAS-Result: AsQBAA9sTFKBaB4inGdsb2JhbABZgz+De7hBhlUWDgEBAQEBBhYJPIIlAQEEASNWBQsLISECAg8FKCGIEwYEqyiSORaNbIRAgTkDmACBMJN2 X-IronPort-AV: E=Sophos;i="4.90,1020,1371074400"; d="scan'208";a="28881121" Received: from mx1.polytechnique.org ([129.104.30.34]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 02 Oct 2013 20:57:47 +0200 Received: from lenat (mna75-4-82-225-76-110.fbx.proxad.net [82.225.76.110]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (No client certificate requested) by ssl.polytechnique.org (Postfix) with ESMTPSA id E8B2C140C4E24; Wed, 2 Oct 2013 20:57:44 +0200 (CEST) Date: Wed, 2 Oct 2013 20:57:41 +0200 From: Simon Cruanes To: David =?utf-8?Q?MENTR=C3=89?= Cc: Gabriel Scherer , caml users Message-ID: <20131002185740.GH964@lenat> References: <524C6B99.5040806@linux-france.org> MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha512; protocol="application/pgp-signature"; boundary="1EKig6ypoSyM7jaD" Content-Disposition: inline In-Reply-To: <524C6B99.5040806@linux-france.org> User-Agent: Mutt/1.5.21 (2010-09-15) X-AV-Checked: ClamAV using ClamSMTP at svoboda.polytechnique.org (Wed Oct 2 20:57:46 2013 +0200 (CEST)) X-Spam-Flag: No, tests=bogofilter, spamicity=0.000000, queueID=215CB140C4E2A X-Org-Mail: simon.cruanes.2007@polytechnique.org Subject: Re: [Caml-list] OCaml editor running tests or other tasks in background? --1EKig6ypoSyM7jaD Content-Type: text/plain; charset=utf-8 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Le Wed, 02 Oct 2013, David MENTR=C3=89 a =C3=A9crit : > Hello, >=20 > 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. >=20 > Thanks for the pointer. >=20 > >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. >=20 > I've only seen demos and never used this feature a lot. You probably > right that such a feature should be correctly tuned. >=20 > >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. >=20 > 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. I agree with Gabriel, something close to what merlin does for type errors would probably be the best thing. If tests were launched every time you hit "save", run in the background, and display a warning (the same way merlin already does for compilation warnings), it would be a tight feedback loop indeed. There are some facilities for writing unit tests directly in source code, at least in Batteries. That would keep everything in the same editor page. My 2 cents --=20 Simon --1EKig6ypoSyM7jaD Content-Type: application/pgp-signature -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.21 (GNU/Linux) iQIcBAEBCgAGBQJSTGykAAoJEErAHQhJqmK245kQAIBooBSlKWgJaRBSXsMFBqM6 xISfY/8W9QxKp9xSrasDynNqVLaWf/D612I2xZezrqn/PVbv7ijL3IuoWx8b2z+b HMU1ZDbPZrouPx2zblXAFP+NFPELaBkIO2iVzVILayyPGOXyHzjXp5hhLiPx+RHP UyJHvssvkLUbMsBu4PmcY6+ZofgFEvAciZVzQXi749KmSktgxuq/uaDupcmNcUlS Z7975TnfA/aIvUzn9HvL/MbkMmCa5RVHdxCYUlQj1rmRufDHdZ/ZDSupTEhPzpp0 J7qIw3z3UgbY2g0lr7MQjwXmG74OtwlLi9VOD+KBnX6MCK8bQYLQKWiWzuibF+Gx zTAzQLDl7h/vyjU+XRZeAwux0+4s5YLQvS6ZKJQQ3117284czDgOcS8+ss5BAra1 fcMnoMJ8YPqL9+a+sbJtpswczQIQxO6yc9/zlHc9R9mGsRYx9qaSWW6lA4EIQHn3 YeXyxznNCujD/mswErr23HhQ6pd++ZvukMN+gAoqc19Ba6nxF8HViaiP0wmgEy5a +2pEWk8D4/wtZpjEVCNVyLKtQkv9gY4Z2dQaW4eDLJn1aynWJbsz3vb8zWRKD+cq Kh6Qt8uSAbA/nCpAlKyVT9cMPaJesUjdKfWvPM9zqGMOj7F47YTy82kMHoURmvdy bnpN6WqtGXQef10gNer8 =3B9U -----END PGP SIGNATURE----- --1EKig6ypoSyM7jaD--