Fix TacticTrace to support OCaml 5.4, add 'hol.sh compile/link/inline-load/-use-module'

[aqjune-aws]

This patch

• Fixes TacticTrace to support OCaml 5.4
• Add an example to TacticTrace. This can be checked with make test inside TacticTrace dir, as well as make -f holtest.mk /tmp/hol-light-test/TacticTrace/make-test.ready.
• For easier compilation and inlining of HOL Light proofs, add the following options to hol_4.14.sh:
  • hol.sh compile <args to ocamlopt>
  • hol.sh link <args to ocamlopt>
  • hol.sh inline-load <args to inline_load.ml>
  • Updates to hol_4.sh is not necessary because OCaml 4.14 is the minimal version that supports proof compilation.
• Also add hol.sh -use-module which prints 1 if HOLLIGHT_USE_MODULE was set when built (0 otherwise)
• Slighly simplify TacticTrace by removing the usage of TACLOGGER_DIR env variable.