[mizar] Errors recovery

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Dear Freek,

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?
>

By '_first_non *4 error' you mean probably errors with numbers less than 50.
The SCHEMATIZER is now much better, but in old implementation the correcting
errors reported by SCHEMATIZER was a very nasty job.

I am not sure if a beginner knows how to correct the error #50, but even an
experienced user might want to leave
an error #103 for a while, suspecting that some registration of clusters is
missing in the environment. So, it leaves
parsing errors. We teach students to correct first PARSER errors, because if
the system cannot parse correctly, it does not understand the text and other
errors may be misleading.

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.



>
> 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. It reminds me the old joke
from communist time, when they want to convince us that we got a (social)
progress. Eventually people agreed, the question was, if the progress was 'do
przodu' (forward) or 'do tylu' (backward). Well, 'the whole error recovery
stuff dates from ...' is true  and Euclidean Geometry dates from third century
BC.

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.

Andrzej