[isabelle-dev] `compiling' the cookbook

[urban at math.lmu.de]

Hi Christian,

> Recently I checked out the mercurial repos of Isabelle and the Cookbook
> and additionally added rail to my TeX installation.

Rail is not necessary to compile the programming tutorial.
There is also a ready-made pdf-file in the repository,
in case you just want to read it.

> Approximately 4 hours later (my machine was doing something  
> according to its noise, but there was no output at the terminal) I  
> killed the process.
>
> Did I miss anything? How long is it supposed to take?

Sorry this is my fault!

No, it is supposed to take less than a minute, but
it needs PolyML 5.2.1. My guess is that you compiling it
with something else.

The reason is that one example in the programming tutorial
shows the timeLimit function, which only works properly
in 5.2.1. The example I use to demonstrate timeLimit uses
the Ackermann function. So for 4 hours you tried to
calculate the (4,12)-datapoint of this function (which I
think takes considerably longer than 4 hours ;o)

For the time being, I can show you how to disable this
example (it is in the file TimeLimit.thy) and for the
future I will think of a better example to illustrate
this function.

Hope this helps,
Christian

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.