text_formalization/computational_build.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - CODE BUILD                                                      *)
   3 (*                                                                            *)
   4 (* Chapter: All Chapters                                                      *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2012-04-12                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 (* Build of the computational parts of the Flyspeck Project *)
  11
  12 flyspeck_needs "strictbuild.hl";;
  13 flyspeck_needs "general/flyspeck_lib.hl";;
  14
  15 (* Tikz *)
  16 flyspeck_needs  "../kepler_tex/tikz/tikz.ml";;
  17
  18 (* graph generator *)
  19 flyspeck_needs ("/../graph_generator/graph_control.hl");;
  20
  21 (* glpk *)
  22 flyspeck_needs "nonlinear/parse_ineq.hl";;
  23 flyspeck_needs "../glpk/glpk_link.ml";;
  24 flyspeck_needs "../glpk/minorlp/tame_table.ml";;
  25 flyspeck_needs "../glpk/minorlp/OXLZLEZ.ml";;
  26 flyspeck_needs "../glpk/tame_archive/lpproc.ml";;
  27 flyspeck_needs "../glpk/sphere.ml";;
  28 flyspeck_needs "../glpk/tame_archive/hard_lp.ml";;
  29 flyspeck_needs "../glpk/tame_archive/scaffolding.hl";;
  30
  31 flyspeck_needs "../glpk/tame_archive/build_lp.hl";;
  32
  33 (* formal lp see formal_lp/README.txt for installation instructions. *)
  34 (*
  35 needs "../formal_lp/hypermap/verify_all.hl";;
  36 let result = Verify_all.verify_all();;
  37 *)
  38
  39 (* nonlinear inequalities needs *)
  40 flyspeck_needs   "nonlinear/ineq.hl";;
  41 flyspeck_needs   "nonlinear/lemma.hl";; (* indep of Ineq *)
  42 flyspeck_needs   "nonlinear/functional_equation.hl";; (* indep of Ineq *)
  43 flyspeck_needs   "nonlinear/parse_ineq.hl";;
  44 flyspeck_needs   "nonlinear/optimize.hl";;
  45 flyspeck_needs   "nonlinear/auto_lib.hl";;
  46 flyspeck_needs "../glpk/sphere.ml";;
  47 flyspeck_needs "nonlinear/check_completeness.hl";;
  48 flyspeck_needs "nonlinear/scripts.hl";;
  49
  50
  51
  52
  53 module Computational_build = struct
  54
  55   open Flyspeck_lib;;
  56
  57 (* tex generation Tikz figures. /tmp/x.txt *)
  58
  59   let tikz_out = Tikz.execute();;
  60
  61 (* graph generator (informal java) *)
  62
  63   let java_found = exists_pgm "java";;
  64
  65
  66   let graph_control_out =    Graph_control.execute();;
  67
  68 (* run on April 13, 2012.  Output saved to string_archive.txt *)
  69
  70 (* glpk (informal) *)
  71
  72   let glpsol_found = exists_pgm "glpsol";;
  73
  74 (* tests consistency of lp computed b table with values in graph_control.flyspeck_properties *)
  75   let tame_table_out = Tame_table.execute();;
  76   let oxlzlez_informal_out = Oxlzlez_informal.execute();;
  77   let build_lp_out = Build_lp.execute();;
  78
  79 (* cfsqp (informal) *)
  80
  81 (* returns list that fail to compile or that are negative *)
  82   let cfsqp_out = Scripts.execute_cfsqp();;
  83
  84
  85 (* nonlinear (informal) *)
  86
  87   let interval_out = Scripts.execute_interval_allbutdodec true;;
  88
  89   let check_completeness_out = Check_completeness.execute();;
  90
  91
  92 (* nonlinear informal prep.hl form *)
  93
  94   let mk_prep_hl = Preprocess.exec();;  (* generate /tmp/prep.hl *)
  95
  96   let preplist = ref [];;
  97   let add_inequality t = (preplist:= t::!preplist);;
  98   let getprep idv = filter (fun t -> (t.idv = idv)) (!preplist);;
  99
 100   flyspeck_needs "nonlinear/prep.hl";;  (* load after add_inequality has been defined *)
 101   List.length !preplist;;
 102
 103   let testprep_idq ex idq =
 104     let (s,tags,ineq) = Optimize.idq_fields idq in
 105       Auto_lib.execute_interval ex tags s ineq;;
 106
 107   let testprep ex s = testprep_idq ex (hd (getprep s));;
 108
 109   let runprep cases =
 110     map (fun t -> try (testprep true t) with Failure _ -> ()) cases;;
 111
 112 (*  runprep (map fst Scripts.fast_cases);; *)
 113
 114
 115  end;;
 116