https://github.com/flyspeck/flyspeck
Raw File
Tip revision: 05bd66666b4b641f49e5131a37830f4881f39db9 authored by zipperer on 26 November 2020, 19:53:58 UTC
minuscule edits (#5)
Tip revision: 05bd666
load_flyspeck.ml
#load "unix.cma";;

(* Edit these paths *)
let flyspeck_dir = "/home/user/flyspeck/text_formalization";;
let hollight_dir = "/home/user/hol-light";;

let () = Unix.putenv "FLYSPECK_DIR" flyspeck_dir;;
let () = Unix.putenv "HOLLIGHT_DIR" hollight_dir;;

needs "Multivariate/flyspeck.ml";;

needs (Filename.concat flyspeck_dir "build/strictbuild.hl");;
needs "build/build.hl";;

let build_to_seq seq name =
  let i = index name seq in
  let seq0, _ = chop_list (i + 1) seq in
  let _ = map flyspeck_needs seq0 in
  ();;

(* Loads the given Flyspeck file and all its dependencies.
   The file path should be relative to flyspeck/text_formalization.
   The linear program bounds are not loaded and verified when this function is used.
   Examples:
   build_to "hypermap/hypermap.hl";  
   build_to "local/LFJCIXP.hl"; *)
let build_to name =
  build_to_seq Build.build_sequence_main_statement name;;

(* This function can be used to load and verify Flyspeck files including
   bounds of linear programs *)
let build_to_full name =
  build_to_seq Build.build_sequence_full name;;

(* Loading the main statement without linear program bounds *)
(*
build_to "general/the_main_statement.hl";;
*)

(* Loading the main statement with linear program bounds *)
(*
build_to_full "general/the_kepler_conjecture.hl";;
*)
back to top