Re: [piotr@sedalia.cs.ualberta.ca: Re: [mizar] Errors recovery]

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

Piotr Rudnicki wrote:

>
> I have tried that and it did not work too well.  In a similar laboratory setting,
> I run several sessions with students doing the same drills at the same pace.
> Only the first error is ever discussed.  After a month the students do individual
> and different exercises and are always told to deal with the first error only.

It is a malpractice. After getting some experience they should keep the exercise syntactically correct.

>
> They also get a piece of advice: you may deal with more errors if you know what
> you are doing.  And they stick with one.

If you encourage students to be lazy, what the poor guys should do?

>
>
> > > 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.
> >
> > So, there is no errors recovery in these languages.
>
> There is and a quite sophisticated one at times.  However, it is just faster
> to get a syntactically correct program by dealing with just the first error
> and recompiling.

It is inconsistent with your previous message that only the first error message is meaningful. So do these compilers have
errors recovery, then you can correct more errors, or not?

>
>
> Just today, I have run through Mizar 7 a text written in Mizar 6.  I have got
> some 700 parsing errors.  What was I supposed to do?  Analyze all of them?
>

Are you so compulsive? No, it is not necessary to analyze all of them. As you well know, most of them are not errors in
strict sense but the result of 'errors' occurring earlier. So, you should correct all registrations and notations. Probable
all of them, but of course you are allowed to correct them one by one. The other errors will vanish.

It happens quite often when we do revisions (1000 errors rarely happens, but happens). And to complete a revision in a
reasonable time we must work much faster.

>
> In the current Mizar when there is an error in the environment the further
> checking is abandoned (as it should be).  I propose that there is a standard macro
> in Mizar distribution that
>
>         - stops after finding parsing errors (at least 1 and no more than say 10),
>         - stops after the analyzer if there were any errors.
>

I am rather against. Such a macro would be misleading. But everybody may write it for himself.

The option that the verifier stops after first error is of course useful. At least in two cases:
- checking the repository after a revision: we want to select the articles that we have correct
- cleaning the environment - it is a revision of a sort - a utility removes e.g. a file name from the 'clusters' directive
and verifier checks if it is really necessary; so, the one error is enough to refute the hypothesis.

>
> And the final comment: when something is difficult to do it does not
> yet mean that it is worth doing, e.g error recovery.

Of course. Still, there is a slight suspicion that the enthusiasm about not doing it is caused by the fact that it is
difficult, not worthless. Such general rules solve nothing (it is again a general rule, isn't it :-))

Andrzej