[mizar] Re: Mizar 7.8.04 MML 4.80.962

[Jesse Alama <alama@stanford.edu>]

Adam Grabowski <adam@math.uwb.edu.pl> writes:

> On Sun, 25 Mar 2007, Jesse Alama wrote:
>
>> Adam Grabowski <adam@math.uwb.edu.pl> writes:
>>
>>>   Let me briefly summarize the changes in the hottest official
>>> distribution of the Mizar system:
>>>
>>> [snip]
>>>
>>> - There is no agreement which approach is better: (let me describe
>>>   this based on the definition of a group) - to define the unity
>>>   of a group as the selector of the underlying structure possessing
>>>   the appropriate properties (the latter via "attribute" definition),
>>>   or to introduce it by an adjective without any additional selector.
>>>   The earlier approach is represented by "well-unital" adjective (and
>>>   the unity is denoted by 1.F for a field F), the latter - by
>>>   "unital" one (1_F). The change, done by Andrzej Trybulec consisted
>>>   mainly in replacing "unital" with "well-unital" and "1." with "1_"
>>>   (for "well-unital" these are equivalent notions). I am not sure if
>>>   it's right because as I remember some five years ago we did exactly
>>>   the opposite - but the "identify" construction wasn't available those
>>>   days.
>> What are the consequences of these changes for those (like me) doing
>> developments that use groups and fields?  I'm using the functor "1.";
>> should I now use "1_"?  Should I change "unital" to "well-unital"?
>   Hopefully, you shouldn't change the symbol of the unity; "well-unital"
> should be used instead of "unital". Note that some references have
> to be changed from GROUP_1:def 5 into VECTSP_1:def 16 then, but it
> depends on the directives are available in your environment. I guess
> "identify"
> registration present at the end of VECTSP_1 will save most of your proofs
> (1_F and 1.F are identified).
>> And where can I find the definition of a field now?
>   In the same place it was before, I don't think you use that from
> REALSET2 which was removed (well, shown equivalent), so VECTSP_1.
>>
>> Jesse
>>
>> PS I'm refraining from installing the latest version because you
>> mentioned it has bugs.  When might the bugfix release be available?
>   The main bug is that some of the abstracts are broken, and some
> additional unnecessary comments are flagged, the database is o'k.
>   I hope it will be this Monday.

I finally installed the newest MML and mizar binaries and found, to my
surprise, that new errors in my articles were introduced; the errors
were different from the ones that I might have found out about by
studying the above discussion.  I found that that what used to be the
definition of the predicate "in" for 1-sorted structures moved from
RLVECT_1:def 1 to STRUCT_0:def 5.  (Curiously, the definition
RLVECT_1:def 1 doesn't even exist anymore, that is, it doesn't seem
that it refers to anything, not just that the referent has changed!)

This was a minor though annoying problem to deal with.  How could I
have known about this in advance?  Perhaps a better summary of the
changes to the MML should be available, or maybe a script that one
could run on one's mizar articles that would make them conform to the
newest MML (as far as possible).

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*950: Too many schemes (http://www.mizar.org)