Commits on Aug 11, 2024

1. Factor out loader functions and core loads as hol_loader.ml and hol_l… …

   …ib.ml
   
   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 committed Aug 11, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 3a7e062
   • Browse repository at this point

   Copy the full SHA

   3a7e062 View commit details

   Browse the repository at this point in the history