module Log = struct type t = { date: string; (* "yearXXXX/monthXX/dayXX" *) hol_version: string; hol_snapshot: string; (* yearXXmonthXXdayXX *) svn_version: int; (* from http://code.google.com/p/flyspeck *) ftable : (string*int) list; comment : string; };; let loglist = [ (* put newest at the beginnning *) { date = "2010/01/12"; hol_version="2.20+"; hol_snapshot="091221"; svn_version=1531; ftable=[("volume/vol1.hl", 750); ("trigonometry/trigonometry.hl", 732); ("trigonometry/trig2.hl", 730); ("trigonometry/trig1.hl", 721); ("nonlinear/ineqdata3q1h.hl", 720); ("nonlinear/ineq.hl", 720); ("leg/enclosed_def.hl", 720); ("leg/quadratic_root_plus_def.hl", 719); ("leg/abc_of_quadratic_def.hl", 718); ("leg/muR_def.hl", 717); ("leg/collect_geom.hl", 716); ("leg/cayleyR_def.hl", 691); ("leg/affprops.hl", 690); ("leg/AFF_SGN_TAC.hl", 690); ("leg/geomdetail.hl", 690); ("general/sphere.hl", 648); ("general/flyspeck_utility.hl", 580); ("general/prove_by_refinement.hl", 580); ("general/update_database_310.ml", 580); ("general/print-types.ml", 580); ("pervasives", 580)]; comment = "Thales, office Mac, Virtual Box, Ubuntu, checkpointed, hypermap.hl failed"; }; ];; end;;