Re: [mizar] Errors recovery

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Hello,

On Sun, 8 Feb 2004, Josef Urban wrote:

> On Sun, 8 Feb 2004, Piotr Rudnicki wrote:
>
> > 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.
>
> That should be options to verifier, something like
> verifier -P10 -A1 -C30 blah.miz .

I like the idea and the option syntax you've suggested. Actually, we've
added an option to stop the verifier on first error in the upcomming
version 7.0.02, but your proposal seems to be much more useful. At one go
we could also replace the options telling the verifier to stop after the
parser and analyser pass i.e. -p and -a by something like -P0 and -A0,
respectively.

Adam Naumowicz