cakeml
cakeml copied to clipboard
CakeML
CakeML: A Verified Implementation of ML
Some of the `GiveUp`s in `data_to_word` could be compiler failures rather than generating code that aborts at runtime. This is better for the user since the failure is caught earlier....
`dataLang` contains a dead code elimination pass, but it only works for pure code, and primitives which consume space are not considered pure. There should be a switch in `dataLang`,...
Currently, if you translate something with a side-condition from `ARB`, the translator produces the code `raise Bind`. It would be nice to tweak this a little to allow an arbitrary...
Currently, entry into a `Handle` is more expensive than it strictly needs to be. See dev mail from 28 September 2016.
This is quite a bad way but still better than the old way Progress list. 1. unpack_types --done 2. unpack_v_thms 3. unpack_cons_names 4. unpack_type_mods
Looking at the result of eq_lemmas after calling ``val _ = translation_extends "decProg";`` in the front of to_flatProgTheory it seems some theorems stored have unnecessary T in the implication ```...
I recently made a PR (https://github.com/CakeML/cakeml/pull/1270) that added `Test` to source `op` datatype. This issue is about doing more of these kinds of rearranging and additions to source `op`. My...
Files such as `cakeml/basis/basisProgScript.sml` already use [modern syntax for quotes](https://github.com/HOL-Theorem-Prover/HOL/issues/1229). Ideally, we would be using it more extensively where it makes sense. For example, in `readerProgScript.sml`, ```sml val _ =...
follow up of #1243. We can always be faster :)
Maintaining `panStaticExamples.sml` (the static checker being orthogonal to the compiler verification) is super tedious because of the different yet similar permutations of test cases, eg. 6 (soon to be 7)...
