From mboxrd@z Thu Jan  1 00:00:00 1970
Path: news.gmane.org!not-for-mail
From: Eli Zaretskii <eliz@gnu.org>
Newsgroups: gmane.emacs.devel
Subject: Re: Have you all gone crazy? Was: On being web-friendly and why
	info	must die
Date: Thu, 18 Dec 2014 05:45:37 +0200
Message-ID: <83k31pvcwu.fsf@gnu.org>
References: <CAP1yDHYm2uJ1fnObdN3F4X44w+9nVxHCaFULH9bM-M8Dz207Mw@mail.gmail.com>
	<87y4q69m4a.fsf@fencepost.gnu.org>
	<jwvvblaf0b6.fsf-monnier+emacs@gnu.org>
	<87mw6m9dt7.fsf@fencepost.gnu.org>
	<jwvh9wudixm.fsf-monnier+emacs@gnu.org>
Reply-To: Eli Zaretskii <eliz@gnu.org>
NNTP-Posting-Host: plane.gmane.org
X-Trace: ger.gmane.org 1418874375 4403 80.91.229.3 (18 Dec 2014 03:46:15 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Thu, 18 Dec 2014 03:46:15 +0000 (UTC)
Cc: dak@gnu.org, sven.axelsson@gmail.com, emacs-devel@gnu.org
To: Stefan Monnier <monnier@iro.umontreal.ca>
Original-X-From: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org Thu Dec 18 04:46:07 2014
Return-path: <emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org>
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 <emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org>)
	id 1Y1S2R-0002xY-Gl
	for ged-emacs-devel@m.gmane.org; Thu, 18 Dec 2014 04:46:07 +0100
Original-Received: from localhost ([::1]:52387 helo=lists.gnu.org)
	by lists.gnu.org with esmtp (Exim 4.71)
	(envelope-from <emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org>)
	id 1Y1S2Q-00030m-VC
	for ged-emacs-devel@m.gmane.org; Wed, 17 Dec 2014 22:46:06 -0500
Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:57174)
	by lists.gnu.org with esmtp (Exim 4.71)
	(envelope-from <eliz@gnu.org>) id 1Y1S2I-00030P-Q6
	for emacs-devel@gnu.org; Wed, 17 Dec 2014 22:46:03 -0500
Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
	(envelope-from <eliz@gnu.org>) id 1Y1S2D-0002Rb-L6
	for emacs-devel@gnu.org; Wed, 17 Dec 2014 22:45:58 -0500
Original-Received: from mtaout29.012.net.il ([80.179.55.185]:35697)
	by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from <eliz@gnu.org>)
	id 1Y1S24-0002P8-Gp; Wed, 17 Dec 2014 22:45:44 -0500
Original-Received: from conversion-daemon.mtaout29.012.net.il by mtaout29.012.net.il
	(HyperSendmail v2007.08) id <0NGR00L00DZKE800@mtaout29.012.net.il>;
	Thu, 18 Dec 2014 05:43:11 +0200 (IST)
Original-Received: from HOME-C4E4A596F7 ([87.69.4.28]) by mtaout29.012.net.il
	(HyperSendmail v2007.08) with ESMTPA id
	<0NGR00G9TEBY0K60@mtaout29.012.net.il>;
	Thu, 18 Dec 2014 05:43:10 +0200 (IST)
In-reply-to: <jwvh9wudixm.fsf-monnier+emacs@gnu.org>
X-012-Sender: halo1@inter.net.il
X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x
X-Received-From: 80.179.55.185
X-BeenThere: emacs-devel@gnu.org
X-Mailman-Version: 2.1.14
Precedence: list
List-Id: "Emacs development discussions." <emacs-devel.gnu.org>
List-Unsubscribe: <https://lists.gnu.org/mailman/options/emacs-devel>,
	<mailto:emacs-devel-request@gnu.org?subject=unsubscribe>
List-Archive: <http://lists.gnu.org/archive/html/emacs-devel>
List-Post: <mailto:emacs-devel@gnu.org>
List-Help: <mailto:emacs-devel-request@gnu.org?subject=help>
List-Subscribe: <https://lists.gnu.org/mailman/listinfo/emacs-devel>,
	<mailto:emacs-devel-request@gnu.org?subject=subscribe>
Errors-To: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org
Original-Sender: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org
Xref: news.gmane.org gmane.emacs.devel:180264
Archived-At: <http://permalink.gmane.org/gmane.emacs.devel/180264>

> From: Stefan Monnier <monnier@iro.umontreal.ca>
> Date: Wed, 17 Dec 2014 17:14:05 -0500
> Cc: Sven Axelsson <sven.axelsson@gmail.com>, emacs <emacs-devel@gnu.org>
> 
> > Just what I needed.  An Emacs that will formally prove to me that
> > redisplay has finished.
> 
> Better yet: a machine-checked proof that the redisplay will
> always terminate.

Don't worry: I made sure this is unprovable.