Now that Alice 1.4 has been released, we continue our efforts to make Isabelle work with it. The static part of Isabelle/Pure now essentially compiles, and works -- a little bit. Alice produces a core dump just after bootstrapping most of the system.
Note that the problem occurs on x86 Linux and Mac OS uniformly. I've also tried a version without just-in-time compilation, which crashes at the same position, albeit more slowly. Here is how to reproduce the problem, using the bits of Isabelle source from http://www4.in.tum.de/~wenzelm/test/Isabelle-alice.tar.gz $ cd Isabelle-alice $ alice - use "alice1.ML"; - use "alice2.ML"; This takes some while. Now we have the ProtoPure.thy, just before bootstrapping Pure.thy. It can already be used like this: - use_thy "Test"; - print_theory (theory "Test"); Now comes the critical bit: - use_thy "Pure"; Segmentation fault (core dumped) The core dump is caused by the 'setup' command in Pure.thy, which initializes a number of sub-components. (Of approx. 30 inits only 2 or 3 appear to be critical). A simpler way to produce core dumps is by adding the following line to Test.thy (after "axioms", say): lemma "PROP A ==> PROP A" . Now use_thy "Test" will fail also. Any ideas? Makarius _______________________________________________ alice-users mailing list [email protected] http://www.ps.uni-sb.de/mailman/listinfo/alice-users
