Re: [mizar] vocabularies

[trybulec <trybulec@math.uwb.edu.pl>]

Freek Wiedijk wrote:

The location of _almost everything_ in MML is often
accidental.  If you consider this a serious issue then you
should move around stuff in MML much more than currently
happens.

  

We intend to.

After a revision the definitions of the attributes were
moved to XXREAL_0. But symbols are still on old
vocabularies.
    

That's a bad argument: just move the symbols also to XXREAL_0
(or to yet another article if that's a more natural place
for them).  Sorry, but I don't see the point of this example.

  

That's a very good argument. To move a symbol from a vocabulary A to a vocabulary B
is a lot of work. At least:
1. To look to all 1000 or so articles and change if necessary the 'vocabularies' directive.
2. To modify data for JFM
3. To check if parsing is still correct, of all MML. Actually it may be worse, the parsing is correct
but the meaning of the article has been changed.
and probably more.

What is the natural place for the attribute symbol 'negative'?
1. an article on logic (which one: ZF_LANG, QC_LANG1, MODAL_1,MODELC_1, MODELC_2, ABCMIZ_1)
 to keep it together with
    'conjunctive' 'atomic' 'existential'
2. an article on real numbers
    together with 'positive'
or another place: an article on ortholattices or maybe ordered rings?

What I have in mind that (without preprocessing) we should
move symbols from one article to the other, any time we
change the order of processing.
    

I would expect this to be minor.  Doesn't this kind of
thing also happen with definitions and notations and so on?
It seems more of the same.

  

I am ready to do a lot of work, if necessary. Why I should do more work, if it is not necessary.
Just to keep vocabularies inserted into the articles? Be serious.
Nothing to gain, only troubles.

We have now more flexible system keeping the lexical resources separated from articles.
It works pretty well, why to changed it?

Regards,
Andrzej