Make CakeML build on the experimental kernel

[xrchz]

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]

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

[xrchz]

@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]

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

[mn200]

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

[mn200]

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]

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

[xrchz]

Is this still a performance issue because we use cv_eval instead of EVAL?

[xrchz]

@mn200 would you mind verifying that CakeML builds on expk?

[myreen]

Previously, the CakeML code base was difficult to build on -expk because of the heavy use of EVAL for which -expk is slower than the standard kernel -stdknl.

Now that CakeML uses cv_compute (via cv_transLib) for all really heavy evaluations, we should try to support -expk for all of the CakeML code base.