myreen
myreen
Currently the CakeML tutorial, i.e. the files under [tutorial/solutions](https://github.com/CakeML/cakeml/tree/master/tutorial/solutions) and particularly [wordfreqProgScript.sml](https://github.com/CakeML/cakeml/blob/master/tutorial/solutions/wordfreqProgScript.sml), is based on CF proofs. Since the monadic translator, which is described in [Proof-Producing Synthesis of CakeML with...
The [latest HOL](https://github.com/HOL-Theorem-Prover/HOL/releases/tag/kananaskis-13) has support for nice user facing syntax. This issue is about updating the entire code base to use the new syntax. Two steps: 1. update all definitions,...
Peep-hole optimisation is an interesting optimisation that the CakeML compiler lacks at present. This issue is about adding a peep-hole optimiser to the CakeML compiler, in particular, to the DataLang...
Several people have contacted us asking to have the CakeML semantics in provers other than HOL4. There is an [AFP entry](https://devel.isa-afp.org/entries/CakeML.html) with the CakeML semantics ported to Isabelle/HOL via Lem....
The HOL build process produces an HTML index in `HOL/help/HOLindex.html`. Would it be possible to have a similar HTML file generated for the CakeML repo? @AndreasLoow suggested that such a...
It would be nice to have `process_topdecs` fail immediately when given type-incorrect code to parse. This would be particularly helpful when developing code in `basis`, but is not generally desirable...
This is correct behaviour: ``` > minisatProve.SAT_PROVE ``b ==> T``; val it = ⊢ b ⇒ T: thm ``` This is incorrect behaviour: ``` > minisatProve.SAT_ORACLE ``b ==> T``; Exception-...
I’m planning to make the HOL4 simplifier, decision procedure, and default EVAL set up use the new compute primitive for (at least) any computations over constant natural numbers. This way...
Using the new `--explorer` output, I found a bad code pattern. I gave the compiler the following code to compile: fun add_all x = case x of A a =>...