[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Private DB
Hi Andrzej,
On Wed, 20 Sep 2006, Andrzej Trybulec wrote:
Hi Josef,
Josef Urban wrote:
That's exactly the point. Mizar is very good at discouraging newbies. And
with arguments like "we have more important work to do, than to add simple
features for newbies" it will hardly change.
I am not against "simple features for newbies". I guess you work on it.
I can add features easily to the Mizar Emacs mode, and I often do it
without any previous discussion (just because usually no one else cares).
I probably can submit a change like this "extends" directive to the Mizar
CVS (though I'd be happy if someone else implemented it), but I doubt that
this kind of change would go through without any discussion.
So yes, whatever is the mechanism deciding about Mizar changes (I strongly
suspect that the mechanism is _you_ :-), if this mechanism does not object
to the "extends" directive, we should start to think about how to
implement it.
On the other hand I wonder what "newbies' means. I almost believe that it is
a bad practice just to get a student and order him "formalize this and this".
So, I thnik we need regular Mizar cources, like in UwB.
I think both is needed. It would be good to have whatever course material
you have downloadable from your web site. I've been ranting for almost a
year now about putting on the main Mizar web page a message in big red
letters saying "NEW!! A NICE MIZAR TUTORIAL!! REALLY!!" with a link to
Freek's tutorial. Currently, there are no pointers to any manuals on the
main web page, they are hidden quite deep in your web under a bit obscure
link "Mizar Bibliography" (and the link to the "new" Freek's tutorial is
missing). No manual/tutorial is distributed with Mizar. All these things
are done in Bialystok, I cannot work on them. Note that the link to
Freek's tutorial appeared quite quickly on the Mizar Wiki, being put there
by a "newbie" Michael Nedzelsky who actually tried to learn Mizar by
himself.
Best,
Josef