Re: [mizar] Private DB

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi Andrzej,

On Sun, 17 Sep 2006, Andrzej Trybulec wrote:

> Actually two problems.
>
> I am so accustomed to have two subdirectories of the working directory (TEXT 
> where the article is kept, and PREL for local DB) that I forgot to put PREL 
> directory as as subdirectory of TEXT, where the article was. If one uses 
> Mizar mode for emacs the local DB must be subdirectory of the directory in 
> which the article is. I fixed it after thinking a bit.

If this is a problem, it's probably easy to correct in the Mizar mode. I 
remember similar problem with the vocabulary directory. For some time I 
was trying to chase different possible locations under various operating 
systems and modes of running Mizar, and then just finally decided that it 
is too much pain, and the file structure should be fixed. So whatever the 
location of local DB should be, I'd suggest that the place is fixed too.

> So the problem is that
> - MAKEENV does not recognize that used DB changed

That's now probably completely true only for the local DB, the version 
check ($MIZFILES/mml.ini) should now find that the distributed DB has 
changed. I don't remember how strict that version check is, so e.g. the 
MMl version used for last accommodation could be also noted in the check 
file created by makeenv. This assumes that users don't do bad things with 
the global DB. For the local DB makeenv would probably have to check 
modification times of the relevant files.


> - one cannot call, when in Mizar mode for emacs, ACCOM and force the 
> accommodation.

There are two ways to do it:
- by hand: M-! accom foo.miz RET
- set accom instead of makeenv, if you do "dangerous things" often:
M-x customize-variable RET makeenv RET
Write accom instead of makeenv to the editable field, and either only "Set 
for Current Session", or even "Save for Future Sessions". This way accom 
will be used each time instead of makeenv.

Best,
Josef