[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Private DB

Hi Josef:

Josef Urban wrote:
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. 
Yeah, it is misleading. The subdirectory for vocabularies is 'parallel'. 
The structure of subdirectories needed now is:

                                                         ..
                                                          |
                                              -------------------

                                              
|                            |
                                            DICT                    
TEXT (or something?)
                                                                           
|
                                                              -- 
-------------------
                                                              
|                               |
                                                          
PREL                      the article

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.

I think so. And for local DB is is more complicated. So, it is the 
author responsibility.

- 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.

I would rather avoid it. The simplest trick is to changed the 
Environment Declaration: swap two vocabularies or the names in the 
'constructors' declaration. Still, I think it would be nice to be able 
to call ACCOM from emacs. Not in the case of revision, actually I should 
not attempt revision on not properly customized computer. But in the 
case of multiple files in local DB it may be needed quite often.

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.

All the best,
Andrzej