Email Gateway (Aug 19 2022 at 10:04): Email Gateway (Aug 19 2022 at 10:04):From: Rafal Kolanski <xs@xaph.net>
Hello,
In a new installation of RC3, I try to build HOL such that it goes into
$ISABELLE_OUTPUT (initially empty).
When I try to build HOL, it builds Pure, prints that it is building HOL,
then doesn't do anything. Other tools then complain that:
Unknown logic "HOL" -- no heap file found in:
/home/x/.isabelle/Isabelle2013-RC3/heaps/polyml-5.5.0_x86-linux
/home/x/src/Isabelle2013-RC3/heaps/polyml-5.5.0_x86-linux
Trying to build it (isa3 is aliased to the RC3 isabelle binary):
[~/src/Isabelle2013-RC3/src]# isa3 build HOL
0:00:03 elapsed time, 0:00:04 cpu time
And still no HOL.
When I try to build HOL-Word, HOL gets built but NOT HOL-Word:
[~/src/Isabelle2013-RC3/src]# isa3 build HOL-Word
Building HOL ...
Finished HOL (0:01:27 elapsed time, 0:04:21 cpu time, factor 3.00)
Running HOL-Word ...
Finished HOL-Word (0:00:07 elapsed time, 0:00:29 cpu time, factor 4.14)
0:01:38 elapsed time, 0:04:56 cpu time, factor 3.02
Finished? Where did it put it? The only heaps are in
~/.isabelle/Isabelle-RC3/heaps :
[~/.isabelle/Isabelle2013-RC3/heaps]# find .
./polyml-5.5.0_x86-linux
./polyml-5.5.0_x86-linux/Pure
./polyml-5.5.0_x86-linux/HOL
./polyml-5.5.0_x86-linux/log
./polyml-5.5.0_x86-linux/log/HOL-Word.gz
./polyml-5.5.0_x86-linux/log/Pure.gz
./polyml-5.5.0_x86-linux/log/HOL.gz
I am assuming that the intended semantics for the "isabelle build"
command is to actually build the specified target.
The log for HOL-Word is complete, so what's happening? A system-wide
search for HOL-Word reveals nothing but the log file, but trying to
build it again comes back in around 11 seconds and does nothing.
Incidentally, the wwwfind tool is still broken (keeps looking for
ROOT.ML which someone removed) and no one seems to care, so I will try
to fix it.
I'm on Ubuntu 12.10, 64-bit.
Sincerely,
Rafal Kolanski
Email Gateway (Aug 19 2022 at 10:04):From: Christian Sternagel <c.sternagel@gmail.com>
I was told that it is not ;)
You have to explicitly give the "-b" flag for building, i.e.,
isabelle build -b HOL
If I remember correctly, by default all images are built into your
~/.isabelle/<Isabelle-version>/heaps directory.
In case there are "previous" heap images that have to be build in order
to run the current target, they will be built even without the "-b"
flag, i.e.,
isabelle build HOL-Word
builds everything up to HOL-Word (i.e., Pure and HOL). At first this
sounds strange, but I found the build tool as is, very usable and
convenient.
Also, when using jedit, it is enough to start it, e.g., by
isabelle jedit -l HOL-Word
and all necessary builds are done automatically (including HOL-Word).
(an aside: this is based on the new "isabelle build_dialog")
hope this helps
chris
Email Gateway (Aug 19 2022 at 10:04):From: Rafal Kolanski <xs@xaph.net>
On 11/02/13 20:31, Christian Sternagel wrote:
On 02/11/2013 06:07 PM, Rafal Kolanski wrote:
I am assuming that the intended semantics for the "isabelle build"
command is to actually build the specified target.
I was told that it is not ;)
Ah. I heard rumors of something like that. Silly assumptions. My bad.
You have to explicitly give the "-b" flag for building, [...]
hope this helps
It does. Thank you for such a quick response!
I'll go back to fixing wwwfind now, which definitely does not work.
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 19 2022 at 10:04):From: Makarius <makarius@sketis.net>
On Mon, 11 Feb 2013, Rafal Kolanski wrote:
On 11/02/13 20:31, Christian Sternagel wrote:
On 02/11/2013 06:07 PM, Rafal Kolanski wrote:
I am assuming that the intended semantics for the "isabelle build"
command is to actually build the specified target.
I was told that it is not ;)Ah. I heard rumors of something like that. Silly assumptions. My bad.
You have to explicitly give the "-b" flag for building, [...]
hope this helps
It does. Thank you for such a quick response!
There is also the Isabelle system manual, with a whole chapter on Isabelle
sessions and build management, including real-life examples.
I'll go back to fixing wwwfind now, which definitely does not work.
You have approx. 24h left. I had reported its broken state almost 3
months ago. The Isabelle2013 release train will not wait for latecomers.
Makarius
Last updated: Apr 25 2024 at 04:18 UTC