4 Unix.putenv "FLYSPECK_DIR" "/mnt/Repository/text_formalization";;
\r
7 (* The FLYSPECK_DIR environment variable must be set *)
\r
9 try Sys.getenv "FLYSPECK_DIR" with Not_found -> failwith "FLYSPECK_DIR must be set";;
\r
12 (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;
\r
14 let add_to_load_path path =
\r
15 if mem path !load_path then ()
\r
16 else load_path := path :: !load_path;;
\r
18 add_to_load_path flyspeck_dir;;
\r
20 (* From strictbuild.hl (required by flyspeck_lib.hl) *)
\r
21 let process_to_string unixstring =
\r
22 let p = Unix.open_process_in unixstring
\r
23 and b = Buffer.create 64 in
\r
24 let rec read () = Buffer.add_channel b p 1; read () in
\r
25 try read () with End_of_file -> (let _ = Unix.close_process_in p in Buffer.contents b);;
\r
27 needs "general/lib.hl";;
\r
28 needs "general/flyspeck_lib.hl";;
\r
30 needs "../glpk/tame_archive/lpproc.ml";;
\r
31 needs "../glpk/sphere.ml";;
\r
32 needs "../glpk/tame_archive/hard_lp.ml";;
\r
34 needs "../formal_lp/glpk/build_certificates.hl";;
\r
36 module Lp_build_main = struct
\r
41 open Build_certificates;;
\r
45 easy : branchnbound list;
\r
47 hard : branchnbound list;
\r
51 let tame = Glpk_link.strip_archive (!archiveraw) in
\r
52 let all_bbs = map mk_bb tame in
\r
53 let hard_bbs, easy_bbs = partition (fun bb -> mem bb.hypermap_id Lpproc.hardid) all_bbs in
\r
54 {easy = easy_bbs; hard = map resolve_with_hints_include_flat hard_bbs};;
\r
57 let build_all_easy max =
\r
58 let _ = make_models false in
\r
59 let bbs = get_lp_bbs() in
\r
60 let _ = report "Building easy lp certificates" in
\r
61 build_and_save_all "easy" max true bbs.easy;;
\r
64 let build_all_hard max =
\r
65 let _ = make_models false in
\r
66 let bbs = get_lp_bbs() in
\r
67 let _ = report "Building hard lp certificates" in
\r
68 build_and_save_all "hard" max true bbs.hard;;
\r
72 let _ = build_all_easy max in
\r
73 (* Save each hard lp certificate in a separate file: max = 1 *)
\r
74 let _ = build_all_hard 1 in
\r
82 open Build_certificates;;
\r
83 open Lp_build_main;;
\r
86 let bbs = get_lp_bbs();;
\r
88 let bb = List.nth bbs.hard 1;;
\r
91 let cert = build_certificate true bb;;
\r
92 Lp_certificate.certificate_info cert;;
\r
94 allpass_hint_include_flat 20000 [bb];;
\r