src/Pure/System/build.ML
author wenzelm
Tue, 24 Jul 2012 12:38:33 +0200
changeset 48470 7483aa690b4f
parent 48468 7f2998b95249
child 48472 6ebb6cdd36a5
permissions -rw-r--r--
clarified "document" again, eliminated redundant "no_document";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48418
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/System/build.ML
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
     3
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
     4
Build Isabelle sessions.
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
     5
*)
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
     6
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
     7
signature BUILD =
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
     8
sig
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
     9
  val build: string -> unit
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    10
end;
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    11
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    12
structure Build: BUILD =
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    13
struct
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    14
48465
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    15
local
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    16
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    17
fun use_thys options =
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    18
  Thy_Info.use_thys
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    19
    |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    20
    |> Unsynchronized.setmp print_mode
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    21
        (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    22
    |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    23
    |> Unsynchronized.setmp Goal.parallel_proofs_threshold
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    24
        (Options.int options "parallel_proofs_threshold")
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    25
    |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
48460
20170ae271a5 tuned options;
wenzelm
parents: 48459
diff changeset
    26
    |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
48470
7483aa690b4f clarified "document" again, eliminated redundant "no_document";
wenzelm
parents: 48468
diff changeset
    27
    |> (case Options.string options "document" of "" => false | "false" => false | _ => true) ?
7483aa690b4f clarified "document" again, eliminated redundant "no_document";
wenzelm
parents: 48468
diff changeset
    28
        Present.no_document
48464
a7bf1587eba0 observe "quick_and_dirty";
wenzelm
parents: 48463
diff changeset
    29
    |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty");
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    30
48465
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    31
fun use_theories (options, thys) =
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    32
  let val condition = space_explode "," (Options.string options "condition") in
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    33
    (case filter_out (can getenv_strict) condition of
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    34
      [] => use_thys options thys
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    35
    | conds =>
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    36
        Output.physical_stderr ("Ignoring theories " ^ commas_quote thys ^
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    37
          " (missing " ^ commas conds ^ ")\n"))
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    38
  end;
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    39
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    40
in
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    41
48418
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    42
fun build args_file =
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    43
  let
48459
375e45df6fdf timing is command line options, not system option;
wenzelm
parents: 48458
diff changeset
    44
    val (save, (options, (timing, (verbose, (browser_info, (parent,
375e45df6fdf timing is command line options, not system option;
wenzelm
parents: 48458
diff changeset
    45
        (name, (base_name, theories)))))))) =
48418
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    46
      File.read (Path.explode args_file) |> YXML.parse_body |>
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    47
        let open XML.Decode in
48459
375e45df6fdf timing is command line options, not system option;
wenzelm
parents: 48458
diff changeset
    48
          pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
375e45df6fdf timing is command line options, not system option;
wenzelm
parents: 48458
diff changeset
    49
            (pair string (pair string ((list (pair Options.decode (list string)))))))))))
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    50
        end;
48418
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    51
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    52
    val _ =
48462
424fd5364f15 clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
wenzelm
parents: 48461
diff changeset
    53
      Session.init save false
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    54
        (Options.bool options "browser_info") browser_info
48458
09710d6fc3d1 clarified document options;
wenzelm
parents: 48457
diff changeset
    55
        (Options.string options "document")
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    56
        (Options.bool options "document_graph")
48466
3b2fb20df17d further imitation of ISABELLE_USEDIR_OPTIONS via options;
wenzelm
parents: 48465
diff changeset
    57
        (space_explode ":" (Options.string options "document_variants"))
48462
424fd5364f15 clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
wenzelm
parents: 48461
diff changeset
    58
        parent base_name
48468
7f2998b95249 added "document_dump_only" (cf. negated usedir -C);
wenzelm
parents: 48466
diff changeset
    59
        (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
48463
07f752935ece added "browser_info_remote" (cf. usedir -P);
wenzelm
parents: 48462
diff changeset
    60
        (Options.string options "browser_info_remote")
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48419
diff changeset
    61
        verbose;
48465
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    62
    val _ = Session.with_timing name timing (List.app use_theories) theories;
48418
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    63
    val _ = Session.finish ();
48419
6d7b6e47f3ef save image for inner nodes only;
wenzelm
parents: 48418
diff changeset
    64
    val _ = if save then () else quit ();
48418
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    65
  in () end
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    66
  handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    67
1a634f9614fb some actual build function on ML side;
wenzelm
parents:
diff changeset
    68
end;
48465
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    69
a25daffda966 observe "condition";
wenzelm
parents: 48464
diff changeset
    70
end;