#
8c3fc760 |
|
09-Jun-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
A general update. Now lisp_finalTheory produces assembly files containing the verified LISP interpeteres (in machine code): arm_eval.s x86_eval.s ppc_eval.s Each of these have been successfully run on real hardware, for each respective platform. The proof scripts are likely to only work in the experimental kernel, due to some unfortuante differences between the two kernels. Some of these differences are exposed more frequently now due to recent(ish) changes to the datatype package. Maybe some of the changes made to the datatype package ought to be reconsidered?
|