Factor out loader functions and core loads as hol_loader.ml and hol_lib.ml

[aqjune-aws]

This patch is a second one of splitted patches to support module compilation of HOL Light.

This
(1) Factors out core library loads as hol_lib.ml, which will be compiled into one giant module in the future
(2) Moves #install_printer commands from local files to hol.ml because the directive cannot be compiled
(3) Also factors out use_file, loads, needs, loadt and the functions they use to hol_loader.ml because these will be independently used by the inliner script which will be included in the later patch.

Passed holtest on OCaml 4.14 and 4.05, and also checked that hol.sh can be successfully loaded outside hol-light dir.

[aqjune-aws]

To test this pull request,

(1) Download this inliner script: https://gist.github.com/aqjune-aws/1d9ed4e1943a7a81c3f2ac6c8bdf6179
(2) Compile hol_lib.ml using the following commands:

ocaml inline_load.ml hol_lib.ml hol_lib_inlined.ml
ocamlc -verbose -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I . pa_j.cmo" hol_lib_inlined.ml bignum.cmo -o hol_lib.cmo
ocamlfind ocamlc -package zarith -linkpkg -a -o hol_lib.cma bignum.cmo hol_lib.cmo

(3) Replace loads "hol_lib.ml" in hol.ml with the following code:

(*loads "hol_lib.ml";;*)
Topdirs.dir_load Format.std_formatter
    (Filename.concat (!hol_dir) "hol_lib.cma");;
open Hol_lib;;

[jimgrundy]

This seems pretty nice.

[jrh13]

This is great, thank you! I tested both the regular loading process and module compilation on several OS/architecture/OCaml combinations and they all worked well. The refactoring nicely makes both approaches work without much other change.