text_formalization/build.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: All Chapters                                                      *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-07-14                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 (*
  11    Build file for Flyspeck project.
  12
  13    hol-light should already be loaded
  14    #use "hol.ml";;
  15
  16    Make sure the reference load_path points to the
  17    flyspeck/text_formalization dir If the "FLYSPECK_DIR" environment
  18    variable is set to this directory then this can be done with
  19
  20    load_path:=
  21      let dir = (Sys.getenv "FLYSPECK_DIR") in
  22      let jdir = Filename.concat dir "../jHOLLight" in
  23       jdir::dir::(!load_path);;
  24
  25    It should also point to the hol-light source
  26    load_path := (Sys.getenv "HOLLIGHT_DIR")::(!load_path);;
  27
  28    let flyspeck_needs = needs;;
  29
  30    Multivariate/flyspeck.ml is needed everywhere.
  31
  32  *)
  33
  34 module Build = struct
  35
  36 let build_sequence =
  37   ["general/hol_pervasives.hl";
  38    "general/lib.hl";
  39    "general/flyspeck_lib.hl";
  40    "general/sphere.hl";
  41    "usr/thales/hales_tactic.hl";
  42
  43    "leg/basics.hl";
  44    "leg/geomdetail.hl";
  45    "leg/AFF_SGN_TAC.hl";
  46    "leg/affprops.hl";
  47    "leg/cayleyR_def.hl";
  48    "leg/enclosed_def.hl";
  49    "leg/collect_geom.hl";
  50    "leg/collect_geom2.hl";
  51
  52    "jordan/refinement.hl";
  53    "jordan/lib_ext.hl";
  54    "jordan/hash_term.hl";
  55    "jordan/parse_ext_override_interface.hl";
  56    "jordan/goal_printer.hl";
  57    "jordan/real_ext.hl";
  58    "jordan/tactics_jordan.hl";
  59    "jordan/num_ext_nabs.hl";
  60    "jordan/taylor_atn.hl";
  61    "jordan/float.hl";
  62    "jordan/flyspeck_constants.hl";
  63    "jordan/misc_defs_and_lemmas.hl";
  64    "general/tactics.hl";
  65
  66    "trigonometry/trig1.hl";
  67    "trigonometry/trig2.hl";
  68
  69    "nonlinear/vukhacky_tactics.hl" ;
  70    "nonlinear/compute_2158872499.hl"; (* needs trig1.hl trig2.hl *)
  71
  72    "trigonometry/delta_x.hl";
  73    "trigonometry/euler_complement.hl";
  74    "trigonometry/euler_multivariate.hl";
  75    "trigonometry/euler_main_theorem.hl";
  76    "trigonometry/trigonometry.hl";
  77    "trigonometry/HVIHVEC.hl";
  78
  79    "nonlinear/calc_derivative.hl";
  80    "nonlinear/ineqdata3q1h.hl";
  81    "nonlinear/types.hl";
  82    "nonlinear/nonlin_def.hl";
  83    "nonlinear/ineq.hl";
  84    "nonlinear/main_estimate_ineq.hl";
  85    "nonlinear/lemma.hl";  (* needs trig1, trig2 *)
  86    "nonlinear/functional_equation.hl";
  87    "nonlinear/parse_ineq.hl";
  88    "nonlinear/optimize.hl";
  89    "nonlinear/auto_lib.hl";
  90    "nonlinear/merge_ineq.hl";
  91
  92    "volume/vol1.hl";
  93
  94    "hypermap/hypermap.hl";
  95 (*   "hypermap/bauer_nipkow.hl";  *)
  96
  97    "fan/fan_defs.hl";
  98    "fan/introduction.hl";
  99    "fan/GMLWKPK.hl";
 100    "fan/topology.hl";
 101    "fan/fan_misc.hl";
 102    "fan/planarity.hl";
 103    "fan/HypermapAndFan.hl";
 104    "fan/Conforming.hl";
 105    "fan/polyhedron.hl";
 106
 107    "packing/pack1.hl";
 108    "packing/pack2.hl";
 109    "packing/pack_defs.hl";
 110    "packing/pack_concl.hl";
 111    "packing/pack3.hl";  (* needs pack_defs.hl *)
 112    "packing/Rogers.hl";
 113    "packing/TARJJUW.hl";
 114    "packing/marchal_cells.hl";
 115    "packing/UPFZBZM_support_lemmas.hl";
 116    "packing/EMNWUUS.hl";
 117    "packing/marchal_cells_2_new.hl";
 118    "packing/SLTSTLO.hl";
 119    "packing/LEPJBDJ.hl";
 120    "packing/URRPHBZ1.hl";
 121    "packing/URRPHBZ2.hl";
 122    "packing/HDTFNFZ.hl";
 123    "packing/URRPHBZ3.hl";
 124    "packing/RVFXZBU.hl";
 125
 126    "local/WRGCVDR_CIZMRRH.hl";  (* These 4 were moved up on Jan 1, 2013 *)
 127    "local/LVDUCXU.hl";
 128    "local/LDURDPN.hl";
 129    "local/LOCAL_LEMMAS.hl";
 130    "tame/Inequalities.hl"; (* moved Feb 6, 2013 *)
 131
 132    "packing/YNHYJIT.hl";
 133    "packing/NJIUTIU.hl";
 134    "packing/TEZFFSK.hl";
 135    "packing/QZKSYKG.hl";
 136    "packing/DDZUPHJ.hl";
 137    "packing/AJRIPQN.hl";
 138    "packing/QZYZMJC.hl";
 139    "packing/marchal_cells_3.hl";
 140    "packing/GRUTOTI.hl";
 141    "packing/KIZHLTL.hl";
 142    "packing/bump.hl";
 143    "packing/sum_gammaX_lmfun_estimate.hl";
 144    "packing/UPFZBZM.hl";
 145    "packing/RDWKARC.hl";
 146
 147    "local/local_lemmas1.hl";
 148    "local/NKEZBFC.hl";
 149    "tame/ArcProperties.hl";
 150    "fan/CFYXFTY.hl";  (* needs Nkezbfc_local and Local_lemmas *)
 151
 152    "packing/YSSKQOY.hl"; (* needs ArcProperties.hl *)
 153    "packing/counting_spheres.hl";
 154    "packing/REUHADY.hl";
 155    "packing/TSKAJXY_lemmas.hl";
 156    "packing/TSKAJXY_034.hl";
 157    "packing/OXL_def.hl";
 158    "packing/oxl_2012.hl";
 159    "packing/leaf_cell.hl";
 160    "packing/TSKAJXY.hl";
 161    "packing/OXLZLEZ.hl";
 162
 163    "local/dih2k.hl";
 164    "local/WJSCPRO.hl";
 165    "local/TECOXBM.hl";
 166    "local/VPWSHTO.hl";
 167    "local/LFJCIXP.hl";
 168    "local/localization.hl";
 169    "local/polar_fan.hl"; (*  needs Tecoxbm *)
 170    "local/HDPLYGY.hl";
 171    "local/GBYCPXS.hl";
 172    "local/MTUWLUN.hl";
 173    "local/PCRTTID.hl";
 174    "local/XIVPHKS.hl";  (* added 2013-06-11 *)
 175
 176    "tame/tame_defs.hl";
 177    "tame/tame_concl.hl";
 178    "../jHOLLight/caml/ssreflect.hl";
 179    "../jHOLLight/caml/sections.hl";
 180    "fan/hypermap_iso-compiled.hl";
 181
 182    "tame/TameGeneral.hl";
 183    "tame/JGTDEBU.hl";
 184
 185    "tame/tame_opposite.hl";
 186    "tame/FATUGPD.hl";
 187    "tame/CRTTXAT.hl";
 188    "tame/HRXEFDM.hl";
 189    "tame/CKQOWSA_3.hl";
 190    "tame/CKQOWSA_4.hl";
 191    "tame/CKQOWSA.hl";
 192 (*   "tame/pishort.hl";  not used. *)
 193    "tame/ssreflect/FNJLBXS-compiled.hl";
 194    "../formal_lp/hypermap/ssreflect/add_triangle-compiled.hl";
 195    "tame/ssreflect/tame_lemmas-compiled.hl";
 196
 197    (* Local Fan Appendix *)
 198    "local/appendix_main_estimate.hl";
 199    "local/terminal.hl";
 200    "local/pent_hex.hl"; (* added 2013-06-13 *)
 201    "local/lp_details.hl"; (* added 2013-06-19 *)
 202    "local/ZITHLQN.hl";
 203    "local/XWITCCN.hl";
 204    "local/AYQJTMD.hl";
 205    "local/JKQEWGV.hl";
 206    "local/UXCKFPE.hl";
 207    "local/SGTRNAF.hl";
 208    "local/QKNVMLB.hl";
 209    "local/YXIONXL.hl";
 210    "local/HXHYTIJ.hl";
 211    "local/UAGHHBM.hl";
 212    "local/LKGRQUI.hl"; (* added 2013-06-13 *)
 213    "local/deformation.hl";
 214    "local/ODXLSTCv2.hl"; (* added 2013-06-13 *)
 215    "local/lunar_deform.hl"; (* updated 2013-06-11 *)
 216    "local/OCBICBY.hl"; (* added 2013-06-27 *)
 217    "local/YXIONXL2.hl"; (* 2013-06-26,. *)
 218 (*   "local/XBJRPHC.hl"; (* 2013-07-02 *) moved to flyspeck.ml *)
 219    "local/EYYPQDW.hl"; (* 2013-07-08 *)
 220    "local/IMJXPHR.hl";
 221    "local/ZLZTHIC.hl"; (* 2013-07-10 *)
 222    "local/PQCSXWG.hl"; (* 2013-07-12 *)
 223    "local/NUXCOEA.hl";  (* 2013-07-14  *)
 224    "local/FEKTYIY.hl"; (* 2013-07-21 *)
 225    "local/AURSIPD.hl"; (* 2013-07-21 *)
 226    "local/PPBTYDQ.hl"; (* 2013-07-21 *)
 227    "local/AXJRPNC.hl"; (* 2013-07-21 *)
 228    "local/CUXVZOZ.hl"; (* 2013-07-22 *)
 229    "local/RRCWNSJ.hl"; (* 2013-07-27 *)
 230    "local/JCYFMRP.hl";(* 2013-07-27 *)
 231    "local/TFITSKC.hl";(* 2013-07-27 *)
 232    "local/CQAOQLR.hl";(* 2013-07-27 *)
 233    "local/JLXFDMJ.hl";(* 2013-07-27 *)
 234    "local/YRTAFYH.hl";  (* 2013-07-31 *)
 235    "local/WKEIDFT.hl"; (* 2013-07-31 *)
 236    "local/hexagons.hl"; (* 2013-07-31 *)
 237    "local/IUNBUIG.hl"; (* 2013-07-31 *)
 238    "local/OTMTOTJ.hl"; (* 2013-08-06 *)
 239    "local/HIJQAHA.hl"; (* 2013-08-06 *)
 240    "local/CNICGSF.hl"; (* 2013-08-06 *)
 241    "local/BKOSSGE.hl"; (* 2013-08-07 *)
 242    "local/JOTSWIX.hl"; (* 2013-08-11 *)
 243    "local/ARDBZYE.hl"; (* 2013-08-15 *)
 244    "local/AUEAHEH.hl"; (* 2013-08-15 *)
 245    "local/VASYYAU.hl"; (* 2013-08-15 *)
 246    "local/MIQMCSN.hl"; (* 2013-08-15 *)
 247    "local/JEJTVGB.hl"; (* 2013-08-15 *)
 248
 249    (* integration and compatibility checks *)
 250    "../graph_generator/graph_control.hl";
 251 (*   "tame/dont_repeat_yourself.hl"; *)
 252   ];;
 253
 254 let build_all() =
 255   (needs "Multivariate/flyspeck.ml";
 256    map (fun t -> State_manager.neutralize_state(); needs t) build_sequence);;
 257
 258 end;;