[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Private DB
Hi Andrzej,
On Sun, 17 Sep 2006, Andrzej Trybulec wrote:
So the problem is that
- MAKEENV does not recognize that used DB changed
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.
OK, at least until there are enough people complaining :-).
- 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.
"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 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.
Best,
Josef