(* ========================================================================== *)
(* 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;;