Hi Jesse, 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.
I did not work and Adam Naumowicz wrote me what to do. The article had been already accommodated and used MATRIX_2 from the public DB, then when I called Mizar, MAKEENV did not recognized that accommodation should be repeated (new files for MATRIX_2 where in the local DB). So, I should force the accommodation by hand: go to DOS console and call ACCOM.
It may happen only if in the local DB is an article with the same name as an article in public DB (and moreover it had been accommodated before the local DB was created). That means that either it is a mistake (an attempt to override the name of a public article) or it is the start of a revision (it was the case) that is rather special activity.
So the problem is that - MAKEENV does not recognize that used DB changed- one cannot call, when in Mizar mode for emacs, ACCOM and force the accommodation.
Albeit it is not a big deal. Regards, Andrzej Jesse Alama wrote:
Hi Andrzej, I use emacs often and might be able to help. What's going on? Warm regards, Jesse On 9/15/06, Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp> wrote:I have created private PREL just for one article and I do not know how to change settings in emacs to press him to use it. Anybody could help? Andrzej Trybulec