(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: All Chapters                                                      *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-07-14                                                           *)
(* ========================================================================== *)


(* 
   Build file for Flyspeck project.

   hol-light should already be loaded
   #use "hol.ml";;

   Make sure the reference load_path points to the
   flyspeck/text_formalization dir If the "FLYSPECK_DIR" environment
   variable is set to this directory then this can be done with

   load_path:= 
     let dir = (Sys.getenv "FLYSPECK_DIR") in
     let jdir = Filename.concat dir "../jHOLLight" in
      jdir::dir::(!load_path);;

   It should also point to the hol-light source
   load_path := (Sys.getenv "HOLLIGHT_DIR")::(!load_path);;

   let flyspeck_needs = needs;;

   Multivariate/flyspeck.ml is needed everywhere.
   
 *)

module Build = struct
 
let build_sequence = 
  ["general/hol_pervasives.hl";
   "general/lib.hl";
   "general/flyspeck_lib.hl";
   "general/sphere.hl";
   "usr/thales/hales_tactic.hl";

   "leg/basics.hl";
   "leg/geomdetail.hl";
   "leg/AFF_SGN_TAC.hl";
   "leg/affprops.hl";
   "leg/cayleyR_def.hl";
   "leg/enclosed_def.hl";
   "leg/collect_geom.hl";
   "leg/collect_geom2.hl"; 

   "jordan/refinement.hl"; 
   "jordan/lib_ext.hl"; 
   "jordan/hash_term.hl"; 
   "jordan/parse_ext_override_interface.hl"; 
   "jordan/goal_printer.hl"; 
   "jordan/real_ext.hl";  
   "jordan/tactics_jordan.hl"; 
   "jordan/num_ext_nabs.hl";   
   "jordan/taylor_atn.hl";
   "jordan/float.hl"; 
   "jordan/flyspeck_constants.hl";
   "jordan/misc_defs_and_lemmas.hl"; 
   "general/tactics.hl";

   "trigonometry/trig1.hl";
   "trigonometry/trig2.hl";

   "nonlinear/vukhacky_tactics.hl" ;
   "nonlinear/compute_2158872499.hl"; (* needs trig1.hl trig2.hl *)

   "trigonometry/delta_x.hl";
   "trigonometry/euler_complement.hl";
   "trigonometry/euler_multivariate.hl";
   "trigonometry/euler_main_theorem.hl";
   "trigonometry/trigonometry.hl";
   "trigonometry/HVIHVEC.hl";

   "nonlinear/calc_derivative.hl";
   "nonlinear/ineqdata3q1h.hl";
   "nonlinear/types.hl";
   "nonlinear/nonlin_def.hl";
   "nonlinear/ineq.hl";
   "nonlinear/main_estimate_ineq.hl";
   "nonlinear/lemma.hl";  (* needs trig1, trig2 *)
   "nonlinear/functional_equation.hl";
   "nonlinear/parse_ineq.hl";
   "nonlinear/optimize.hl";
   "nonlinear/auto_lib.hl";
   "nonlinear/merge_ineq.hl";

   "volume/vol1.hl";

   "hypermap/hypermap.hl";  
(*   "hypermap/bauer_nipkow.hl";  *)

   "fan/fan_defs.hl";
   "fan/introduction.hl";
   "fan/GMLWKPK.hl";
   "fan/topology.hl";
   "fan/fan_misc.hl";
   "fan/planarity.hl";   
   "fan/HypermapAndFan.hl";
   "fan/Conforming.hl";
   "fan/polyhedron.hl";

   "packing/pack1.hl"; 
   "packing/pack2.hl"; 
   "packing/pack_defs.hl";
   "packing/pack_concl.hl";
   "packing/pack3.hl";  (* needs pack_defs.hl *)
   "packing/Rogers.hl";
   "packing/TARJJUW.hl"; 
   "packing/marchal_cells.hl";
   "packing/UPFZBZM_support_lemmas.hl";
   "packing/EMNWUUS.hl";
   "packing/marchal_cells_2_new.hl"; 
   "packing/SLTSTLO.hl";
   "packing/LEPJBDJ.hl";
   "packing/URRPHBZ1.hl";
   "packing/URRPHBZ2.hl";
   "packing/HDTFNFZ.hl";
   "packing/URRPHBZ3.hl";
   "packing/RVFXZBU.hl"; 

   "local/WRGCVDR_CIZMRRH.hl";  (* These 4 were moved up on Jan 1, 2013 *)
   "local/LVDUCXU.hl";
   "local/LDURDPN.hl";
   "local/LOCAL_LEMMAS.hl"; 
   "tame/Inequalities.hl"; (* moved Feb 6, 2013 *)
   
   "packing/YNHYJIT.hl";  
   "packing/NJIUTIU.hl";
   "packing/TEZFFSK.hl";
   "packing/QZKSYKG.hl";
   "packing/DDZUPHJ.hl";
   "packing/AJRIPQN.hl";
   "packing/QZYZMJC.hl";
   "packing/marchal_cells_3.hl";
   "packing/GRUTOTI.hl"; 
   "packing/KIZHLTL.hl";
   "packing/bump.hl";
   "packing/sum_gammaX_lmfun_estimate.hl";
   "packing/UPFZBZM.hl";
   "packing/RDWKARC.hl";

   "local/local_lemmas1.hl";  
   "local/NKEZBFC.hl";
   "tame/ArcProperties.hl"; 
   "fan/CFYXFTY.hl";  (* needs Nkezbfc_local and Local_lemmas *)

   "packing/YSSKQOY.hl"; (* needs ArcProperties.hl *)
   "packing/counting_spheres.hl";
   "packing/REUHADY.hl";
   "packing/TSKAJXY_lemmas.hl";
   "packing/TSKAJXY_034.hl";
   "packing/OXL_def.hl";
   "packing/oxl_2012.hl"; 
   "packing/leaf_cell.hl";
   "packing/TSKAJXY.hl";
   "packing/OXLZLEZ.hl";

   "local/dih2k.hl"; 
   "local/WJSCPRO.hl";
   "local/TECOXBM.hl";
   "local/VPWSHTO.hl";
   "local/LFJCIXP.hl";
   "local/localization.hl";
   "local/polar_fan.hl"; (*  needs Tecoxbm *)
   "local/HDPLYGY.hl";
   "local/GBYCPXS.hl";
   "local/MTUWLUN.hl";
   "local/PCRTTID.hl";
   "local/XIVPHKS.hl";  (* added 2013-06-11 *)

   "tame/tame_defs.hl";
   "tame/tame_concl.hl";
   "../jHOLLight/caml/ssreflect.hl";
   "../jHOLLight/caml/sections.hl";
   "fan/hypermap_iso-compiled.hl";

   "tame/TameGeneral.hl";
   "tame/JGTDEBU.hl";

   "tame/tame_opposite.hl";
   "tame/FATUGPD.hl"; 
   "tame/CRTTXAT.hl";
   "tame/HRXEFDM.hl";  
   "tame/CKQOWSA_3.hl";
   "tame/CKQOWSA_4.hl";
   "tame/CKQOWSA.hl";
(*   "tame/pishort.hl";  not used. *)
   "tame/ssreflect/FNJLBXS-compiled.hl";
   "../formal_lp/hypermap/ssreflect/add_triangle-compiled.hl";
   "tame/ssreflect/tame_lemmas-compiled.hl";

   (* Local Fan Appendix *)
   "local/appendix_main_estimate.hl"; 
   "local/terminal.hl";
   "local/pent_hex.hl"; (* added 2013-06-13 *)
   "local/lp_details.hl"; (* added 2013-06-19 *)
   "local/ZITHLQN.hl";
   "local/XWITCCN.hl";  
   "local/AYQJTMD.hl";
   "local/JKQEWGV.hl";
   "local/UXCKFPE.hl";
   "local/SGTRNAF.hl";
   "local/QKNVMLB.hl";
   "local/YXIONXL.hl";
   "local/HXHYTIJ.hl"; 
   "local/UAGHHBM.hl";
   "local/LKGRQUI.hl"; (* added 2013-06-13 *)
   "local/deformation.hl";
   "local/ODXLSTCv2.hl"; (* added 2013-06-13 *)
   "local/lunar_deform.hl"; (* updated 2013-06-11 *)
   "local/OCBICBY.hl"; (* added 2013-06-27 *)
   "local/YXIONXL2.hl"; (* 2013-06-26,. *)
(*   "local/XBJRPHC.hl"; (* 2013-07-02 *) moved to flyspeck.ml *)
   "local/EYYPQDW.hl"; (* 2013-07-08 *)
   "local/IMJXPHR.hl"; 
   "local/ZLZTHIC.hl"; (* 2013-07-10 *)
   "local/PQCSXWG.hl"; (* 2013-07-12 *)
   "local/NUXCOEA.hl";  (* 2013-07-14  *)
   "local/FEKTYIY.hl"; (* 2013-07-21 *)
   "local/AURSIPD.hl"; (* 2013-07-21 *)
   "local/PPBTYDQ.hl"; (* 2013-07-21 *)
   "local/AXJRPNC.hl"; (* 2013-07-21 *)
   "local/CUXVZOZ.hl"; (* 2013-07-22 *)
   "local/RRCWNSJ.hl"; (* 2013-07-27 *)
   "local/JCYFMRP.hl";(* 2013-07-27 *)
   "local/TFITSKC.hl";(* 2013-07-27 *)
   "local/CQAOQLR.hl";(* 2013-07-27 *)
   "local/JLXFDMJ.hl";(* 2013-07-27 *)
   "local/YRTAFYH.hl";  (* 2013-07-31 *)
   "local/WKEIDFT.hl"; (* 2013-07-31 *)
   "local/hexagons.hl"; (* 2013-07-31 *)
   "local/IUNBUIG.hl"; (* 2013-07-31 *)
   "local/OTMTOTJ.hl"; (* 2013-08-06 *)
   "local/HIJQAHA.hl"; (* 2013-08-06 *)
   "local/CNICGSF.hl"; (* 2013-08-06 *)
   "local/BKOSSGE.hl"; (* 2013-08-07 *)
   "local/JOTSWIX.hl"; (* 2013-08-11 *)
   "local/ARDBZYE.hl"; (* 2013-08-15 *)
   "local/AUEAHEH.hl"; (* 2013-08-15 *)
   "local/VASYYAU.hl"; (* 2013-08-15 *)
   "local/MIQMCSN.hl"; (* 2013-08-15 *)
   "local/JEJTVGB.hl"; (* 2013-08-15 *)

   (* integration and compatibility checks *)
   "../graph_generator/graph_control.hl";
(*   "tame/dont_repeat_yourself.hl"; *)
  ];;

let build_all() =
  (needs "Multivariate/flyspeck.ml"; 
   map (fun t -> State_manager.neutralize_state(); needs t) build_sequence);;

end;;