From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: phillip.lord@newcastle.ac.uk (Phillip Lord) Newsgroups: gmane.emacs.devel Subject: Re: Have you all gone crazy? Was: On being web-friendly and why info must die Date: Fri, 19 Dec 2014 21:26:58 +0100 Message-ID: <878ui3o06l.fsf@newcastle.ac.uk> References: <87y4q69m4a.fsf@fencepost.gnu.org> <87mw6m9dt7.fsf@fencepost.gnu.org> NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain X-Trace: ger.gmane.org 1419021926 19925 80.91.229.3 (19 Dec 2014 20:45:26 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 19 Dec 2014 20:45:26 +0000 (UTC) Cc: David Kastrup , Sven Axelsson , emacs To: Stefan Monnier Original-X-From: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org Fri Dec 19 21:45:18 2014 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 1Y24QH-0003gl-6s for ged-emacs-devel@m.gmane.org; Fri, 19 Dec 2014 21:45:17 +0100 Original-Received: from localhost ([::1]:60487 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Y24QG-0005LU-KE for ged-emacs-devel@m.gmane.org; Fri, 19 Dec 2014 15:45:16 -0500 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:33290) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Y24Q6-00059n-2H for emacs-devel@gnu.org; Fri, 19 Dec 2014 15:45:11 -0500 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1Y24Q0-0000Fv-6O for emacs-devel@gnu.org; Fri, 19 Dec 2014 15:45:06 -0500 Original-Received: from cheviot22.ncl.ac.uk ([128.240.234.22]:46652) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1Y24Pt-0000Bj-4T; Fri, 19 Dec 2014 15:44:53 -0500 Original-Received: from smtpauth-vm.ncl.ac.uk ([10.8.233.129] helo=smtpauth.ncl.ac.uk) by cheviot22.ncl.ac.uk with esmtp (Exim 4.63) (envelope-from ) id 1Y24Ps-0007NV-Eh; Fri, 19 Dec 2014 20:44:52 +0000 Original-Received: from [151.65.203.145] (helo=localhost) by smtpauth.ncl.ac.uk with esmtpsa (TLSv1:AES128-SHA:128) (Exim 4.63) (envelope-from ) id 1Y24Ps-00050c-3q; Fri, 19 Dec 2014 20:44:52 +0000 In-Reply-To: (Stefan Monnier's message of "Wed, 17 Dec 2014 17:14:05 -0500") User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux) X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Received-From: 128.240.234.22 X-BeenThere: emacs-devel@gnu.org X-Mailman-Version: 2.1.14 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-bounces+ged-emacs-devel=m.gmane.org@gnu.org Xref: news.gmane.org gmane.emacs.devel:180347 Archived-At: Stefan Monnier writes: >> 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. That would be nice. > > Finally, an end to all those "I waited a year and redisplay still isn't > done" bug reports, Sadly this requires proof checkers that can distinguish between "will terminate" and "will terminate within the known life-time of the universe". That's a research problem I fear. Phil