#
f383b4fe |
|
18-Jun-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix examples/machine-code/lisp for tight equality
|
#
4b9431d8 |
|
04-May-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Finish fixing machine-code for new by build --selftest=3 now completes; I'm ready to merge into master.
|
#
caf04fc3 |
|
08-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Build more machine-code example thys with pat_assum
|
#
cdb70f70 |
|
03-Dec-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Minor updates.
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
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?
|
#
0e4ccf01 |
|
10-Apr-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Various minor modifications, also added two files that were apparently missing from the svn version.
|
#
44a6db21 |
|
03-Apr-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Restructuring and simplification.
|
#
c2f14f37 |
|
05-Mar-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Improvements to the verified LISP interepreters. The new interpreters have been proved to implement McCarthy's LISP 1.5 as formalise by Mike Gordon for the ACL2 workshop 2007. Warning: lisp_evalScript takes 73 minutes to run using Holmake under PolyML.
|
#
7c197d42 |
|
07-Jan-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
A new version of files previously in examples/mc-logic. Eventually examples/mc-logic will be deleted.
|