cakeml

cakeml copied to clipboard

Most of our targets have some degree of ISA support for a stack using a single register, which by necessity is shared with C: * x64: %rsp is the only...

sorear

target real ELF files for x86-64

4

myreen

Remove Failure CompileError

3

Currently, [the compiler is allowed to](https://github.com/CakeML/cakeml/blob/master/compiler/proofs/compilerProofScript.sml#L125) return `Failure CompileError` for any input program. At present, these compiler errors can only occur when a code label is too far from the...

myreen

A version of the compiler that starts from wordLang (without GC)

2

We want to compile HOL functions that essentially only operate over a memory modelling function and word types to wordLang (phase 1) and from there compile it to concrete machine...

myreen

Double.fma not returning anything.

2

Double.fma doesn't return a value and breaks subsequent code in certain cases. It does, however, always compile. Example program: ``` fun main () = let val a = (Double.fromString "1.0")...

bksaiki

Use Runtime.exit for non-zero exit return in bootstrapped compiler

1

This revives issue #260 The goal is to instead use Runtime.exit and prove the required CF and whole prog spec for the compiler instead of relying on the current approach....

tanyongkiam

w1 ₃₂→₁₆ w2

5

Make it so. Depends on #499

mn200

Currently, the translator dumps all of its state to "disk" with every export theory, when really, it should just dump the changes (new stuff) to disk and then have the...

mn200

Clean up dataLang cost semantics

1

This issue is to clean up some of the mess we made when introducing the dataLang cost semantics. - The `allowed_op` definition serves no purpose anymore --- all operators except...

IlmariReissumies

The translator accepts constants with preconditions, and duplicates preconditions: ```sml > val foo_def = Define` foo = 5 DIV 0`; Definition has been stored under "foo_def" val foo_def = []...

oskarabrahamsson