Started work on fixing replCorrect for type inference
move not_evaluate_whole_prog_timeout to bigClockTheory
add option type to the initial environment in the semantics
add option to initial compiler env, and prove env_rs_empty
compile_prog proof fixes after change to init_compiler_state
add option type to inferencer's initial decls
add sptree compute things to cakeml_computeLib

ideally this should be in an sptree library providing a compset fragment
add compile_top to cakeml_computeLib

since this is another top-level entry-point, add it with the conversion
that adds the generated code to the good code labels database (as is
done for compile_prog too).
update compile_repl_decs to assume repl_decs is in a module
Merge remote-tracking branch 'origin/master' into Word8Array

Conflicts:
	compiler/proofs/compilerProofScript.sml
	compiler/proofs/conLangProofScript.sml
	inference/inferScript.sml
	semantics/initialEnv.lem
	semantics/initialEnvScript.sml

Some non-trivial conflicts because the Size->Subscript renaming hadn't
happened somewhere in the type inferencer, and also some of the compiler
proofs had diverged slightly. This commit should fix all that though.