Re: [mizar] changes in 7.8.05

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

On Thu, 5 Jul 2007, Jesse Alama wrote:

> I noticed just today that a new mizar was released (7.8.05, MML
> 4.83.967).  It looks like this one wasn't announced.  What's new in the
> latest version?

There are some changes to the XML presentation still being improved by
Josef. But most importantly, we started to restructure the database,
the registrations in particular. Previously, all registrations were
'rounded-up' before storing them in the database which meant that not only
the things an author put explicitely into the registration were
exported, but also all consequences of other registrations imported
into that article. It made the registration mechanism a bit stronger,
but also hard to understand for the users in certain situations,
because users didn't have a real control over what they imported.

So in the new version (7.8.05), the library contains only the 
'visible' registrations, and the verifier must do the round-up after
importing - this makes the situation much clearer for the users,
but in many cases may require a few more registrations directives
used explicitely.

To clarify things, let's imagine we have a vocablary tester0.voc and an 
article tester0.miz with the following contents:
-------------------------
Vfoo1
Vfoo2
Ofoonc1
-------------------------
environ
vocabularies TESTER0;

begin

definition
let x be set;
attr x is foo1 means contradiction;
end;

definition
let x be set;
attr x is foo2 means contradiction;
end;

registration
cluster foo1 -> foo2 set;
correctness @proof end;
end;
-------------------------

When we create a local database with 'miz2prel', we can consider
a new article tester.miz:

-------------------------
environ
vocabularies TESTER0;
constructors TESTER0;
notations TESTER0;
registrations TESTER0;

begin

definition
func foonc1 means not contradiction;
correctness @proof end;
end;

registration
cluster foonc1 -> foo1;
correctness @proof end;
end;
-------------------------

Eventually, when we export TESTER into the local database, in all articles 
that import TESTER with the registrations directive one would get

foonc1 is foo2;

as obvious for Mizar ver 7.8.04 - even if only 'registrations TESTER;' was 
used, because the consequence of the conditional cluster from TESTER0 
would be added to the term registration from TESTER.

In the new version, one must state explicitely he wants to import the 
TESTER0 registrations to get the above statement accepted. It may look 
like a step 'backward' compared to the previous capabilities of the 
checker, but we believe it's a step 'in a good direction' - updating old 
articles can be a bit troublesome, but creating new environments from 
scratch with the new version is surely less cryptic now.

I hope this helps,

Adam