#
0e793d8f |
|
17-Aug-2020 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
Add a new example: a small verified bootstrapped compiler This commit contains a development of a "minimal" verified bootstrapped compiler that targets x86-64 assembly code. I have added this to the build-sequence as one of the final examples. The tactic proofs build under both the standard and the experimental kernels. However, the bootstrap evaluation (in compiler_evalScript.sml) seems to get stuck on the experimental kernel. (Is it possible to exclude an example from the build sequence if HOL is built using the experimental kernel?)
|