Hi Freek,You ask difficult questions. It is difficult to anticipate how new version of Mizar will behave and even how it will deal with new (more advanced) articles. It is still an experiment, even if the repository is rather large the most advanced articles are not so advanced and
I would prefer to be on secure side. Freek Wiedijk wrote:
I agree that it is confusing. Even more confusing is (I often have such problem) if the registration is not in the article that already is used but in a different, sometimes very strange, place, On the other hand one have to be careful with adding new registrations, it may cause problems with the complexity and change the behavior of the 'notation' directive.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.
It happened. Maybe we should register such cases, or better to do some experiments. And I do not intend to agree with Josef, I just agree. The problem is with the policy. I agree with you that we do not want to have "the only correct way to write Mizar articles", (I hope I cited you precisely). With a liberal policy we must accept that some articles are not of the highest quality and one may have troubles using them. That is the problem with "get all related to the topic". It goes beyond this. It is the problem of integrity. If the same theory is developed in different terminology, or a different settings, in two series of articles one have to be careful to use both.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? (If that would ever happen, I would tend to say with Josef that it would be a problem with the library.)
Of course, if differs for different directives. Maybe the most unpleasant are 'vocabularies'. E.g. with the CAT_4 vocabulary it is O.K to write 'P[y]' (in a scheme) but 'P[x]' is syntactically incorrect. The 'notation ' is prone with dangers. However, it is probably not the number of file names but the order. I believe it is secure to put anything on the beginning of the list of files.
The 'theorems' and 'scheme' directives seems to be immune to superfluous file names.
The 'registration' directive is dangerous . It can cause very slow processing or even a combinatorial explosion. And it can change the results of the 'notation' directive. The 'constructor' directive seems to be secure, but again it can influence the notation directive.
I am definitely for liberal policy. In is not the problem of freedom, we want to allow attempts to find possibly better solutions. We started reviewing Mizar articles. But reviewing is strictly negative: the reviewers are supposed to give (if any) reasons that the article should not be accepted, not the reasons that it should be published.
To conclude, it is mainly of choice between the liberal policy (then I have to be able to be very precise with import from DB) or more restricted policy (quality, integrity) (then I can to construct the environment in a haphazard way). What we need is probably a compromise. So, we want the golden middle, and we have old problem: left or right.
As yet the Mizar project is quite anti-bourbakist one, we allow for different approaches.
Greetings, Andrzej