#
bc99bcfb |
|
25-Jul-2018 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Another go at strengthening the (default) behaviour of Tactical.prove. By default Tactical.prove now checks for the validity of the supplied tactic using VALID. This breaks a few proofs in which assumptions were surreptitiously being introduced. It is expected that this commit will break some external proofs that relied on the old behaviour (e.g. under CakeML). A workaround is to selectively restore the old behaviour with val () = set_prover (fn (t, tac) => TAC_PROOF (([], t), tac)) in places that contain non-valid tactic proofs.
|
#
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
|
#
845531b5 |
|
14-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in source files.
|
#
693a0c50 |
|
08-Mar-2011 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
|
#
dcb98b45 |
|
08-Mar-2011 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
This proof was getting stuck because the prime on h' is no longer needed.
|
#
e3a30244 |
|
23-Sep-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
A tweak which might help Peter Homeier get this script-file to build on his computer.
|
#
c6b7dae9 |
|
04-Dec-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
More minor fixes.
|
#
cdb70f70 |
|
03-Dec-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Minor updates.
|
#
5add4ae8 |
|
01-Dec-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Switching from using ARM/v4 to the new model ARM model in ARM/v7. This is an intermediate check-in.
|
#
90a751a1 |
|
05-Oct-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Many 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!
|
#
9030ae5a |
|
26-Jun-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
A general update: 1. the decompiler is now slightly faster, due to new code abbreviations (terms smaller in internal proofs); 2. the definition of the machine-code Hoare triple was slightly altered to support instruction caches; 3. the x86 model now includes an instruction cache. Also, I give up on attempting to support MoscowML for examples/machine-code/lisp. Both the standard kernel and the experimental kernel crash while loading files in this directory using the latest patched version of MoscowML. Both kernels exit with an uninformative message: Compiling lisp_equalScript.sml Linking lisp_equalScript.uo to produce theory-builder executable Uncaught exception: Chr Failed to build script file, lisp_equalScript Did they run out of memory? If so, why does the error message not say so?
|
#
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.
|