[isabelle] RC3: new installation isn't interested in building target, only dependencies?



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





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