Make CakeML build on the experimental kernel
Open
- Dominant language
- Standard ML
- Stars
- 1.2k
- Forks
- 104
- Avg merge
- 2d 21h
- Merged PRs (30d)
- 16
Description
The task here is to get the CakeML regression test to pass on HOL's experimental (and/or logging) kernels: the only difference should be in generated names, so this means making proofs robust against generated names.
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.