Re: [isabelle] build tool and moving of files
- To: Peter Lammich <lammich at in.tum.de>
- Subject: Re: [isabelle] build tool and moving of files
- From: Makarius <makarius at sketis.net>
- Date: Mon, 15 Jun 2015 17:41:54 +0200 (CEST)
- Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <1432814588.4208.5.camel@lapnipkow10>
- References: <1432814588.4208.5.camel@lapnipkow10>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Thu, 28 May 2015, Peter Lammich wrote:
I have built some images using "isabelle build". Then, I have moved
around the thy-files in my file-system. Invoking "isabelle build" in the
new directory rebuilds nothing. However, when using jedit with the built
image, CTRL-Clicking on theory names takes me to the old file locations
(opening a new, empty buffer).
This is a known weakness of file references compiled into a session image.
For files in the ~~ (or $ISABELLE_HOME) hierarchy, there are special
provisions in some function Path.smart_implode to evade bad effects on
official logic images, see also
As usual, a function called "smart" is apt to cause problems elsewhere,
and in opposition to the old-school principle of "don't try to be smart".
These slight inconveniences will all disappear, when session images are
based on PIDE sessions, with abstract command span identifiers instead of
file names. But this can take a few more years.
I know that I can do a clean build, but I always thought the purpose of
a build-tool is to re-build as soon as something is changed that may
result in a change of the built artifacts. Here, some path-names would
change, but no rebuild is issued.
Isabelle build does many things, but it is not an absolutely closed world
concerning dependencies. Practically important examples are document
options. It is easy to fool it in more obscure ways, like the example
This archive was generated by a fusion of
Pipermail (Mailman edition) and