1 (* Title: Pure/System/build.ML
4 Build Isabelle sessions.
9 val build: string -> unit
12 structure Build: BUILD =
17 fun use_thys options =
19 |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
20 |> Unsynchronized.setmp print_mode
21 (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
22 |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
23 |> Unsynchronized.setmp Goal.parallel_proofs_threshold
24 (Options.int options "parallel_proofs_threshold")
25 |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
26 |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
27 |> (case Options.string options "document" of "" => true | "false" => true | _ => false) ?
29 |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty");
31 fun use_theories (options, thys) =
32 let val condition = space_explode "," (Options.string options "condition") in
33 (case filter_out (can getenv_strict) condition of
34 [] => use_thys options thys
36 Output.physical_stderr ("Ignoring theories " ^ commas_quote thys ^
37 " (undefined " ^ commas conds ^ ")\n"))
44 val (save, (options, (timing, (verbose, (browser_info, (parent,
45 (name, (base_name, theories)))))))) =
46 File.read (Path.explode args_file) |> YXML.parse_body |>
47 let open XML.Decode in
48 pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
49 (pair string (pair string ((list (pair Options.decode (list string)))))))))))
53 Session.init save false
54 (Options.bool options "browser_info") browser_info
55 (Options.string options "document")
56 (Options.bool options "document_graph")
57 (space_explode ":" (Options.string options "document_variants"))
59 (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
60 (Options.string options "browser_info_remote")
62 val _ = Session.with_timing name timing (List.app use_theories) theories;
63 val _ = Session.finish ();
64 val _ = if save then () else quit ();
66 handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);