Re: [mizar] Errors recovery

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Wed, Feb 04, 2004 at 01:07:56PM +0100, Andrzej Trybulec wrote:
> Freek Wiedijk wrote:
> 
> > You raise an interesting point here.
> >
> > Would you think a version of Mizar that only would report the
> > _first_ non *4 error and then quit, that it would be much
> > less usable than the current one?

> ...

> However, for teaching purposes, at least for distant learning, even it should
> not stop on the first syntactic error. The student wants to consult the error,
> still he may work on the remaining part of article.
> 
> So, for distant learning, the system that stops on the first error is USELESS.

> ...

> In distant learning students waits not one hour but sometimes a couple of
> days, for a comment of the teacher. So, the errors recovery is even more
> important.

No matter what are the current politically correct trends in education
industry, distance learning is pretty useless as attested by its
results that I see on a daily basis.  Besides, in distance learning as
widely done in this country, the turnaround time is a few hours rather
than days.  They use e-mail and web.

> > Dan Synek always claims to me that this whole error recovery
> > stuff dates from a time when computers were big, slow, and
> > you had to wait for the result of one run for an hour because
> > it would come on line printer paper from a mainframe.
> 
> Not only Dan. We got some progress from this time. 

I cannot speak for others, but when working with Mizar I always pay
attention only to the first non checker error and only to the last
checker error if there are no other errors.  And I try to have just
one checker error at any given time having @proof ... for others.  (I
would not mine having @by or @; too.) It just works faster for me,
though it hurts seeing the poor CPU checking the same correct pieces
of Mizar text over and over again.  

In the realm of programming languages like C, C++ or Java, syntactic
errors after the first one are typically total bogus.  In C++, where
identification is complicated, paying attention to any other but the
first identification error is just waste of time.

Winning in error recovery is like winning in any other guessing game.
And the winning strategy is: stay away.


-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr