From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: phillip.lord@russet.org.uk (Phillip Lord) Newsgroups: gmane.emacs.devel Subject: Re: Beyond release Date: Mon, 27 Jun 2016 21:35:28 +0100 Message-ID: <8760sus73j.fsf@russet.org.uk> References: <5254d43b-39dd-7ac2-03d7-349e6d710a6b@online.de> <577135CD.1040605@gmail.com> <8a06c531-eac2-cfd5-eab0-6bf197e8c3e0@online.de> <57714BA1.8030506@gmail.com> <878txqfuuf.fsf@russet.org.uk> <57716AEB.9050409@gmail.com> NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1467059781 5228 80.91.229.3 (27 Jun 2016 20:36:21 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 27 Jun 2016 20:36:21 +0000 (UTC) Cc: emacs-devel@gnu.org To: =?utf-8?Q?Cl=C3=A9ment?= Pit--Claudel Original-X-From: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org Mon Jun 27 22:36:11 2016 Return-path: Envelope-to: ged-emacs-devel@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1bHdGL-00066w-Qu for ged-emacs-devel@m.gmane.org; Mon, 27 Jun 2016 22:36:09 +0200 Original-Received: from localhost ([::1]:60987 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bHdGL-0001kY-2d for ged-emacs-devel@m.gmane.org; Mon, 27 Jun 2016 16:36:09 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:54025) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bHdFn-0001kF-6I for emacs-devel@gnu.org; Mon, 27 Jun 2016 16:35:36 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1bHdFj-0005Cj-Nn for emacs-devel@gnu.org; Mon, 27 Jun 2016 16:35:35 -0400 Original-Received: from cloud103.planethippo.com ([31.216.48.48]:38689) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bHdFj-0005Ca-9x for emacs-devel@gnu.org; Mon, 27 Jun 2016 16:35:31 -0400 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=russet.org.uk; s=default; h=Content-Transfer-Encoding:Content-Type: MIME-Version:Message-ID:In-Reply-To:Date:References:Subject:Cc:To:From; bh=zQL07SNDO3tkAXzPY62/U8YwGN0EFcPppMV3pKQ5Xp8=; b=WEFNJpSjW1NVjABBJxSONPa2Ht qVDIzMWyPC1E9LOZ2Hg+LAex/+qC/M7LZSR7/IgLmwe98H5AU8C9iKcnorTljFLdyHIA5yOLbAGqJ oh1WjXltHsAbQ3pclO4KIujH0uxB1/BgT03nQNgCEX9swxWzTsOrnJz99V4Qj9iIpemfip9GMmcOo sfzY6nijZZv6qRXb9WRtLNntVsnufA6F6XPhtjZJT7PB4RIkbeXOliFp+/YZTsuGkOo5UPFEpI8Vn v0cSLqC9BSrcwQHpqHEJd+p/ZCQ/QoQEO06FcufOxP7JmrvUtfqUj6Aw9zifLsBPHvZUUV6jFLHLq 9ha941+g==; Original-Received: from cpc1-benw10-2-0-cust373.gate.cable.virginm.net ([77.98.219.118]:52765 helo=russet.org.uk) by cloud103.planethippo.com with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.86_1) (envelope-from ) id 1bHdFi-003Dtd-5B; Mon, 27 Jun 2016 21:35:30 +0100 In-Reply-To: <57716AEB.9050409@gmail.com> (=?utf-8?Q?=22Cl=C3=A9ment?= Pit--Claudel"'s message of "Mon, 27 Jun 2016 14:05:31 -0400") User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.0.95 (gnu/linux) X-AntiAbuse: This header was added to track abuse, please include it with any abuse report X-AntiAbuse: Primary Hostname - cloud103.planethippo.com X-AntiAbuse: Original Domain - gnu.org X-AntiAbuse: Originator/Caller UID/GID - [47 12] / [47 12] X-AntiAbuse: Sender Address Domain - russet.org.uk X-Get-Message-Sender-Via: cloud103.planethippo.com: authenticated_id: phillip.lord@russet.org.uk X-Authenticated-Sender: cloud103.planethippo.com: phillip.lord@russet.org.uk X-detected-operating-system: by eggs.gnu.org: GNU/Linux 3.x X-Received-From: 31.216.48.48 X-BeenThere: emacs-devel@gnu.org X-Mailman-Version: 2.1.21 Precedence: list List-Id: "Emacs development discussions." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org Original-Sender: "Emacs-devel" Xref: news.gmane.org gmane.emacs.devel:204835 Archived-At: Cl=C3=A9ment Pit--Claudel writes: > On 2016-06-27 12:40, Phillip Lord wrote: >> I'm guessing that Isabelle/Emacs integration used "parsing output" >> interaction. FWIW, I think that the days of this form of archictecture >> are numbered. Both scala and clojure interaction now use something with >> a structured protocol, with a specialized server on the scala or clojure >> side. A similar thing is happening with R, also, and maybe with JDEE. > > And with Coq, another proof assistant that still uses Emacs as its main I= DE. > We're currently working on porting Proof General to use Coq's structured > protocol. Ah, didn't know that. >> I don't know if anything could be done, but adding general support for >> repl interaction to core or ELPA would probably be a good thing. I don't >> know if it is possible -- most of the tools that I have mentioned so far >> use different protocols, so perhaps it is not. > > Do you really mean REPL interaction? If so, comint-mode does exactly this= , I > think :) Yeah, didn't put that very carefully. I meant "the sort of things that in the past, we used to do my passing stuff to a REPL and parsing the results". I.e. not REPL interaction. > But if you meant structured protocols, then it's tricky; there's indeed a > large variety of protocols. The main pain point when developing those (ba= sed > on limited experience developing Emacs modes for Dafny, F* and Coq =E2=80= =94 which all > use different protocols) is asynchronicity; you end up registering timers= to > delay certain actions or implement queues, and it's pretty tricky to keep= the > code organized properly. CIDER uses call-backs, which seems to work okay, and is reasonably easy to implement with closures. How much of this could be made generic, I don't know. There are definately some overlapping issues, though. Asynchronous callbacks are a little hard to implement and debug, so providing way of making call-backs that log might be nice. I'll have a think on it. PHil