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.
