search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
944 stars 81 forks source link

Make CakeML build on the experimental kernel #321

Open xrchz opened 6 years ago

xrchz commented 6 years ago

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.

xrchz commented 6 years ago

Probably depends on a solution to HOL-Theorem-Prover/HOL#462 first

xrchz commented 6 years ago

@mn200 this is currently stuck with parse_topdecs going into a loop. It would be good if parse_topdecs could be taken out of whatever cf Lib it's in and made into a legitimate part of parsingComputeLib.

xrchz commented 6 years ago

@mn200: @Xaphiosis wonders if there's been any progress on this front

mn200 commented 6 years ago

None by me so far. I can look into it this week though.

mn200 commented 6 years ago

My suspicion (from running the parser's test suite) is that EVAL on the parser is just super-slow on the experimental kernel. For example, it takes a minute to parse val x = 0w3. I will profile to see if there's something obvious that can be improved there, but it is somewhat expected for this to be the case (though not to this extent of course!)

mn200 commented 6 years ago

This issue is not a barrier to OpenTheory recording of CakeML anymore.