myreen

Currently, my plan with #666 is to do the following w.r.t. the HOL string type in the lexer: https://github.com/CakeML/cakeml/blob/834e7c4e926d453bea905223f8affad2e460d1ba/compiler/bootstrap/translation/lexerProgScript.sml#L14-L19 Thus this does not avoid the `explode` on input to the...

Note that this issue goes against #186.

A potentially less intrusive approach could be to leave the compiler implementation as is, but instead construct _a compiler configuration transformer_ that given a normal compiler configuration produces a new...

Even if we merge parts, I hope we can retain the idea that: - `semantics` is the definition of the source semantics, and - `semantics/proofs` are proofs / general lemmas...

Work on this could advance in stages: 1. Implement the compression and decompression algorithms as functions in HOL 2. Make it easy to prove `∀s. decompress (compress s) = s`...

I think this is a great idea! I just want to add that I suspect one needs replace Step 4 with: 4. Call the binary CakeML compiler on `foo_sexpr_1` to...

@mn200 I'm confused by this: > you could then also think about attempting to verify that the parser and printer inverted each other. I was under the impression that the...

Ah, @mn200 points out that `If` does exist but as a primitive op.

> An initial approach could be to define an alternative exp_of and prove equivalence to the old one. Proofs can then choose which one to use. Better yet is to...

@binghe I'm on MacOS running on Mac. But note that you need to call **SAT_ORACLE** rather than SAT_PROVE.