remove probably useless bring_to_front_overload"Num" from cakeml_compute

I didn't see any occurrences of "Num" in the file, so I presume this
isn't necessary any more. If it is, it should be the temp_ version since
this is not a script file.
make dependence on $HOLDIR/examples/parsing explicit

for pegLib which is used in cakeml_computeLib

this might be picked up transitively (through heaps) via the dependence
on ../parsing, but that seems to be a bit flaky
start updating bootstrap/Holmakefile

this commit makes it something more reasonable given all the changes
since bootstrap was last touched, although it may still need further
tweaking
tidy use of SUC_TO_NUMERAL_DEFN_CONV in cakeml_computeLib
use sLet_pat_thm rather than _def in cakeml_computeLib

the former is a small simple definition, whereas the definition has
unwieldy pattern-matching. probably the nice theorem should move into
compilerTermination or something so it doesn't depend on the proofs, but
this works for now.
move sLet_pat_thm into compilerTerminationTheory
save theorems precomputing evaluation of real_inst_length together

previously had generated a separate theorem for each case and added them
to the_compset. it makes more sense to save a single theorem (the
conjunction) so it's easier to find it to add it to other compsets.
use eval_real_inst_length for code_labels_conv in cakeml_compute

labels_computeLib.code_labels_conv needs a conversion to evaluate the
length function. previously had been passing in the cakeml compset
evaluator, but this doesn't include evaluation of real_inst_length. it
actually probably makes more sense to use a conversion that is
specialised to evaluating real_inst_length, so that is what we do in
this commit. if it needs to become more versatile later (e.g. for other
instruction lengths) we could make eval_real_inst_length a reference.
add some missing defs to conLang part of cakeml compset
initial experiments bootstrapping repl_decs

on a basic evaluation using the cakeml compset the time starts to go
badly non-linear after about 100 decs, which is around when the type
inferencer and rest of compiler start being defined. will probably need
to resort to some of the tricks used last time, namely splitting the
decs up into chunks and doing something smart with finite map lookups.
possibly other optmisations are possible too.