Re: [isabelle] build tool and moving of files



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 http://isabelle.in.tum.de/repos/isabelle/annotate/Isabelle2015/src/Pure/General/path.ML#l200

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


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.