Re: [mizar] Private DB

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

Josef Urban wrote:

> "M-! accom foo.miz RET" calls it the same way you call it from shell. 
> If you wish, I can add this to the Mizar mode menu.
I'll be grateful. A pack of Pilsner next time we'll meet or anything 
what you fix, I doubt if you want any Dojlidy beer. And I do not want 
even to pretend that I know what "M-! accom foo.miz RET" means.

> > I do not complain about the structure of files. Actually I think the 
> > DICT directory should be a subdirectory of the directory in which the 
> > article is kept, too.
>
>
> I think it used to be that way until quite recently. Whatever the 
> change will be, it will make someone's life painful (probably many 
> people use DICT, while not so many PREL), so I don't know if it is 
> worth the pain. 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.
O.K. Users that use local PREL are supposed to be more knowledgeable 
that those that use local DICT, that probably means every Mizar user. 
So, they (the guys using local PREL) are not so important. The special 
ENV directory is useful only for educational application. Well, 'only' , 
if we mostly concerned with the development of the repository, the 
teaching is still most important.