text_formalization/nonlinear/formal_tests/load.hl

   1 let flyspeck_dir = "/mnt/Repository/text_formalization";;\r
   2 let hollight_dir = "";;\r
   3 \r
   4 load_path := flyspeck_dir :: !load_path;;\r
   5 \r
   6 let flyspeck_needs = needs;;\r
   7 \r
   8 map needs [\r
   9         "Multivariate/flyspeck.ml";\r
  10         "Rqe/num_calc_simp.ml";\r
  11         "general/sphere.hl";\r
  12         "general/prove_by_refinement.hl";\r
  13 ];;\r
  14 \r
  15 #load "unix.cma";;\r
  16 let process_to_string unixstring =\r
  17   let p = Unix.open_process_in unixstring\r
  18   and b = Buffer.create 64 in\r
  19   let rec read () = Buffer.add_channel b p 1; read () in\r
  20     try read () with End_of_file -> (Unix.close_process_in p; Buffer.contents b);;\r
  21 \r
  22 \r
  23 open Prove_by_refinement;;\r
  24 \r
  25 map needs [\r
  26         "general/flyspeck_lib.hl";\r
  27         "leg/collect_geom2.hl";\r
  28         "leg/enclosed_def.hl";\r
  29         "trigonometry/trig2.hl";\r
  30 ];;\r
  31 \r
  32 map needs [\r
  33         "jordan/lib_ext.hl";\r
  34         "jordan/refinement.hl";\r
  35         "jordan/parse_ext_override_interface.hl";\r
  36         "jordan/real_ext.hl";\r
  37         "jordan/hash_term.hl";\r
  38 ];;\r
  39 \r
  40 \r
  41 prioritize_real();;\r
  42 map needs [\r
  43         "jordan/tactics_jordan.hl";\r
  44         "jordan/num_ext_nabs.hl";\r
  45         "jordan/taylor_atn.hl";\r
  46         "jordan/float.hl";\r
  47         "jordan/flyspeck_constants.hl";\r
  48 ];;\r
  49 \r
  50 map needs [\r
  51         "nonlinear/ineq.hl";\r
  52         "nonlinear/lemma.hl";\r
  53 ];;\r