Re: [mizar] Private DB

[Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp>]

Hi Freek,

Freek Wiedijk wrote:

One even more painful thing to do (at least from the point of fixing a lot 
of Mizar tools) would be to have additional ENV directory for all the 
environment files produced by accommodation, which are illegable to users 
and just make mess out of their clean TEXT directory.
    

What I always want is to have all those files just be
combined into one _file_ (with separators in such a way that
it is easy to navigate that file, I guess.)  Is there a good
reason not to do this, apart from the fact that all the tools
will need to be changed for that?
  

The only serious reason that can think about is the 'sound conservatism': it works, don't touch it. Czesiek argues many times in many years that in the reasonable repository we need an abstract form of an article. The accommodator should extract what is necessary. I am not so sure that I have presented his opinion adequately, but Czesiek will correct me if he wishes.

Mind you, that does not mean that I want one directive like 'import' in Coq. Even if we clean MML systematicaly, that cause a lot of complaints, still there is a need to import from an article a theorem, that has nothing to do with the article itself, and there is no reason to import from the article anything else but the theorem.

I never claim, of course, that I am right. :-)

All the best,
Andrzej