[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[piotr@sedalia.cs.ualberta.ca: Re: [mizar] Errors recovery]
I am sending this once more as it seems that the original message never made it through.
----- Forwarded message from Piotr Rudnicki <piotr@sedalia.cs.ualberta.ca> -----
Date: Thu, 5 Feb 2004 23:20:23 -0700
From: Piotr Rudnicki <piotr@sedalia.cs.ualberta.ca>
To: mizar-forum@mizar.uwb.edu.pl
Subject: Re: [mizar] Errors recovery
User-Agent: Mutt/1.2.5.1i
In-Reply-To: <40214A58.905BF5DD@math.uwb.edu.pl>; from trybulec@math.uwb.edu.pl on Wed, Feb 04, 2004 at 08:39:05PM +0100
On Wed, Feb 04, 2004 at 08:39:05PM +0100, Andrzej Trybulec wrote:
> In the course "Introduction to Logic and Set Theory" we had (Ania Zalewska and me)
> in average
> 8 students in the laboratory. In one teaching session they are supposed to prove 2 -
> 5 theorems in e.g. theory
> of binary relations.
> I can work with one student explaining, how to correct an error (and what is the
> cause ot the error). It takes let us say 3 minutes. TS lasts 105 minutes, so I have
> in average about 12 minutes for a student, so I talk to him app. 4 times.
> Of course, I allow students for discussing errors between themselves, and sometimes
> I ask for attention and explain the problem for the whole group. Still, if they do
> not know how to correct an error, they can work on other parts of the proof. If they
> wait for my explanation for the first error that they do not know how to correct,
> they have to stop their work about 20 minutes. That means that I just cannot teach
> without errors recovery.
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.
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.
> > 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.
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?
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.
And the final comment: when something is difficult to do it does not
yet mean that it is worth doing, e.g error recovery.
Cheers,
--
Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr
----- End forwarded message -----
--
Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr