Email Gateway (Aug 22 2022 at 10:00): Email Gateway (Aug 22 2022 at 10:00):From: Peter Lammich <lammich@in.tum.de>
Hi,
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).
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.
Email Gateway (Aug 22 2022 at 10:13):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 16 2024 at 12:28 UTC