caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: "David MENTRÉ" <dmentre@linux-france.org>
To: Gabriel Scherer <gabriel.scherer@gmail.com>
Cc: caml users <caml-list@inria.fr>
Subject: Re: [Caml-list] OCaml editor running tests or other tasks in background?
Date: Wed, 02 Oct 2013 20:53:13 +0200	[thread overview]
Message-ID: <524C6B99.5040806@linux-france.org> (raw)
In-Reply-To: <CAPFanBHaMHcQ++60EQ_LMpf=WJwqOrPEeYPRsQHLbpLweBbyjA@mail.gmail.com>

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


  reply	other threads:[~2013-10-02 18:53 UTC|newest]

Thread overview: 6+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2013-10-02 16:00 David MENTRE
2013-10-02 17:06 ` Gabriel Scherer
2013-10-02 18:53   ` David MENTRÉ [this message]
2013-10-02 18:57     ` Simon Cruanes
2013-10-02 18:56   ` Jeremie Salvucci
2013-10-03  6:06     ` David MENTRE

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=524C6B99.5040806@linux-france.org \
    --to=dmentre@linux-france.org \
    --cc=caml-list@inria.fr \
    --cc=gabriel.scherer@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).