[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Private DB


Hi Freek,

On Wed, 27 Sep 2006, Freek Wiedijk wrote:


The original problem was simplified import of other articles.
Your suggestion now seems to be to solve that by [...]


But I have no problem with the way the notations work in
Mizar!  _That's_ not why I consider the Mizar imports to be
baroque (so baroque that you might even call it rococo!)


Then I probably misunderstood what you wrote a week ago:

On Wed, 20 Sep 2006, Freek Wiedijk wrote:


But still, I often find that something does not work exactly
the way it should (sometimes when I've already been working on
an article for quite some time), and then after a long search
it turns out that I miss some cluster from an article, which
already turns out to be mentioned in one of the other
directives in the environment!  With a simplified way to
import stuff that kind of confusion very probably wouldn't
have happened.

So, a question: does it ever happen that it is harmful to have
_too many_ articles mentioned in the "environ".  That the
solution to some problem is to _remove_ an article from the
registrations, say?
As I tried to explain yesterday, the current overloading mechanisms do not allow reasonable adding (or merging if interpreted in the MML order) of some directives. 


What I would like, for simplification of writing the environ, is:

1. [..] everything NAT_1;

[..]

2. To have the "extends" directive like we discussed.  So

	extends XBOOLE_0;
	definitions XBOOLE_0;

  Again, this directive should be _extra,_ for lazy people
  like me, and not replace the current system.  Let's be
  backwards compatible for optimal control.
And I quite support both in principle - actually I asked Andrzej here if it would be OK to start to think about its implementation.
What I am not sure about, and what gave rise to the talk about overloading, is how to resolve various combinations of such directives. I quite fear that e.g. 

extends JORDAN, OSAFREE;
notations SCMRING4;
will be even more cryptic to the users than the current "rococo", unless the overloading "behaves well". 


3. To have a version of Mizar that has something like "irrths"
  built into the system in such a way that I don't need to
  write a "theorems" directive myself anymore.
Again, I quite agree in principle. I think there already are some related functions in the Emacs mode, and it should not be difficult to extend the Mizar "accommodator" to first do a shallow scan for something like "(by|from) *([A-Z_0-9]+):" (it's a bit more complicated, but feasible), and automatically add it all to the "theorems" directive.
And again, problem is that you may also need to add some "constructor" directives for that (that can also be automated), and those (I think) can in turn active some previously unused "notations", "registrations" and "definitions", change the way how overloading is resolved, and mess your article (I wish I were wrong with that).
That's why I think the fragility of current overloading mechanisms has to be addressed as part of the problem. 

Josef