Hi, On Sun, 17 Sep 2006, Andrzej Trybulec wrote:
Hi Freek, Freek Wiedijk wrote: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.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?
I think there are also some (probably weak) efficiency reasons - having separate files is a poor man's database solution. Also, even if all the files produced by accommodation were merged, there would still be several files produced by different passes of verifier. They are also mergeable, but that's as natural as merging temporary files produced by gcc compiler.
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 think that one simplified directive like "import all the topology stuff" would at least simplify starting a Mizar article on advanced topics. The practice today is first to think "what article is closest to my topic", and then to copy its environment. If someone new does the mistake of trying to understand the black magic behind environmental directives, he is probably lost as a Mizar author forever. The old directives could remain for fine-tuning if needed.
Josef