src/Pure/Tools/dump.scala
author wenzelm
Sat Sep 08 13:22:23 2018 +0200 (9 months ago)
changeset 68946 6dd1460f6920
parent 68945 fa5d936daf1c
child 68947 ea804c814693
permissions -rw-r--r--
more accurate output;
     1 /*  Title:      Pure/Tools/dump.scala
     2     Author:     Makarius
     3 
     4 Dump cumulative PIDE session database.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Dump
    11 {
    12   /* aspects */
    13 
    14   sealed case class Aspect_Args(
    15     options: Options,
    16     progress: Progress,
    17     deps: Sessions.Deps,
    18     output_dir: Path,
    19     snapshot: Document.Snapshot,
    20     node_status: Document_Status.Node_Status)
    21   {
    22     def write(file_name: Path, bytes: Bytes)
    23     {
    24       val path = output_dir + Path.basic(snapshot.node_name.theory) + file_name
    25       Isabelle_System.mkdirs(path.dir)
    26       Bytes.write(path, bytes)
    27     }
    28 
    29     def write(file_name: Path, text: String): Unit =
    30       write(file_name, Bytes(text))
    31 
    32     def write(file_name: Path, body: XML.Body): Unit =
    33       write(file_name, Symbol.encode(YXML.string_of_body(body)))
    34   }
    35 
    36   sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
    37     options: List[String] = Nil)
    38   {
    39     override def toString: String = name
    40   }
    41 
    42   val known_aspects =
    43     List(
    44       Aspect("markup", "PIDE markup (YXML format)",
    45         { case args =>
    46             args.write(Path.explode("markup.yxml"),
    47               args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
    48         }),
    49       Aspect("messages", "output messages (YXML format)",
    50         { case args =>
    51             args.write(Path.explode("messages.yxml"),
    52               args.snapshot.messages.iterator.map(_._1).toList)
    53         }),
    54       Aspect("latex", "generated LaTeX source",
    55         { case args =>
    56             for (entry <- args.snapshot.exports if entry.name == "document.tex")
    57               args.write(Path.explode(entry.name), entry.uncompressed())
    58         }, options = List("editor_presentation", "export_document")),
    59       Aspect("theory", "foundational theory content",
    60         { case args =>
    61             for {
    62               entry <- args.snapshot.exports
    63               if entry.name.startsWith(Export_Theory.export_prefix)
    64             } args.write(Path.explode(entry.name), entry.uncompressed())
    65         }, options = List("editor_presentation", "export_theory"))
    66     ).sortBy(_.name)
    67 
    68   def show_aspects: String =
    69     cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
    70 
    71   def the_aspect(name: String): Aspect =
    72     known_aspects.find(aspect => aspect.name == name) getOrElse
    73       error("Unknown aspect " + quote(name))
    74 
    75 
    76   /* dump */
    77 
    78   val default_output_dir: Path = Path.explode("dump")
    79   val default_commit_clean_delay: Time = Time.seconds(-1.0)
    80   val default_watchdog_timeout: Time = Time.seconds(600.0)
    81 
    82   def make_options(options: Options, aspects: List[Aspect]): Options =
    83   {
    84     val options1 = options + "completion_limit=0" + "ML_statistics=false" + "parallel_proofs=0"
    85     (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
    86   }
    87 
    88   def dump(options: Options, logic: String,
    89     aspects: List[Aspect] = Nil,
    90     progress: Progress = No_Progress,
    91     log: Logger = No_Logger,
    92     dirs: List[Path] = Nil,
    93     select_dirs: List[Path] = Nil,
    94     output_dir: Path = default_output_dir,
    95     verbose: Boolean = false,
    96     commit_clean_delay: Time = default_commit_clean_delay,
    97     watchdog_timeout: Time = default_watchdog_timeout,
    98     system_mode: Boolean = false,
    99     selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
   100   {
   101     if (Build.build_logic(options, logic, build_heap = true, progress = progress,
   102       dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
   103 
   104     val dump_options = make_options(options, aspects)
   105 
   106 
   107     /* dependencies */
   108 
   109     val deps =
   110       Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
   111         selection_deps(selection)
   112 
   113     val include_sessions =
   114       deps.sessions_structure.imports_topological_order
   115 
   116     val use_theories =
   117       deps.sessions_structure.build_topological_order.
   118         flatMap(session_name => deps.session_bases(session_name).used_theories.map(_.theory))
   119 
   120 
   121     /* dump aspects asynchronously */
   122 
   123     object Consumer
   124     {
   125       private val consumer_ok = Synchronized(true)
   126 
   127       private val consumer =
   128         Consumer_Thread.fork(name = "dump")(
   129           consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
   130             {
   131               val (snapshot, node_status) = args
   132               if (node_status.ok) {
   133                 val aspect_args =
   134                   Aspect_Args(dump_options, progress, deps, output_dir, snapshot, node_status)
   135                 aspects.foreach(_.operation(aspect_args))
   136               }
   137               else {
   138                 consumer_ok.change(_ => false)
   139                 for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) {
   140                   val msg = XML.content(Pretty.formatted(List(tree)))
   141                   progress.echo_error_message("Error" + Position.here(pos) + ":\n" + msg)
   142                 }
   143               }
   144               true
   145             })
   146 
   147       def apply(snapshot: Document.Snapshot, node_status: Document_Status.Node_Status): Unit =
   148         consumer.send((snapshot, node_status))
   149 
   150       def shutdown(): Boolean =
   151       {
   152         consumer.shutdown()
   153         consumer_ok.value
   154       }
   155     }
   156 
   157 
   158     /* session */
   159 
   160     val session =
   161       Thy_Resources.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs,
   162         include_sessions = include_sessions, progress = progress, log = log)
   163 
   164     val theories_result =
   165       session.use_theories(use_theories,
   166         progress = progress,
   167         commit = Some(Consumer.apply _),
   168         commit_clean_delay = commit_clean_delay,
   169         watchdog_timeout = watchdog_timeout)
   170 
   171     val session_result = session.stop()
   172 
   173     val consumer_ok = Consumer.shutdown()
   174 
   175     if (theories_result.ok && consumer_ok) session_result
   176     else session_result.error_rc
   177   }
   178 
   179 
   180   /* Isabelle tool wrapper */
   181 
   182   val isabelle_tool =
   183     Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
   184     {
   185       var aspects: List[Aspect] = known_aspects
   186       var base_sessions: List[String] = Nil
   187       var commit_clean_delay = default_commit_clean_delay
   188       var select_dirs: List[Path] = Nil
   189       var output_dir = default_output_dir
   190       var requirements = false
   191       var watchdog_timeout = default_watchdog_timeout
   192       var exclude_session_groups: List[String] = Nil
   193       var all_sessions = false
   194       var dirs: List[Path] = Nil
   195       var session_groups: List[String] = Nil
   196       var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
   197       var options = Options.init()
   198       var system_mode = false
   199       var verbose = false
   200       var exclude_sessions: List[String] = Nil
   201 
   202       val getopts = Getopts("""
   203 Usage: isabelle dump [OPTIONS] [SESSIONS ...]
   204 
   205   Options are:
   206     -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
   207     -B NAME      include session NAME and all descendants
   208     -C SECONDS   delay for cleaning of already dumped theories (disabled for < 0, default: """ +
   209       Value.Seconds(default_commit_clean_delay) + """)
   210     -D DIR       include session directory and select its sessions
   211     -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
   212     -R           operate on requirements of selected sessions
   213     -W SECONDS   delay for cleaning of already dumped theories (unlimited for 0, default: """ +
   214       Value.Seconds(default_watchdog_timeout) + """)
   215     -X NAME      exclude sessions from group NAME and all descendants
   216     -a           select all sessions
   217     -d DIR       include session directory
   218     -g NAME      select session group NAME
   219     -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
   220     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   221     -s           system build mode for logic image
   222     -v           verbose
   223     -x NAME      exclude session NAME and all descendants
   224 
   225   Dump cumulative PIDE session database, with the following aspects:
   226 
   227 """ + Library.prefix_lines("    ", show_aspects) + "\n",
   228       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
   229       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
   230       "C:" -> (arg => commit_clean_delay = Value.Seconds.parse(arg)),
   231       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   232       "O:" -> (arg => output_dir = Path.explode(arg)),
   233       "R" -> (_ => requirements = true),
   234       "W:" -> (arg => watchdog_timeout = Value.Seconds.parse(arg)),
   235       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   236       "a" -> (_ => all_sessions = true),
   237       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   238       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   239       "l:" -> (arg => logic = arg),
   240       "o:" -> (arg => options = options + arg),
   241       "s" -> (_ => system_mode = true),
   242       "v" -> (_ => verbose = true),
   243       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   244 
   245       val sessions = getopts(args)
   246 
   247       val progress = new Console_Progress()
   248       {
   249         override def theory_percentage(session: String, theory: String, percentage: Int)
   250         {
   251           if (verbose) echo(Progress.theory_message(session, theory) + ": " + percentage + "%")
   252         }
   253       }
   254 
   255       val result =
   256         progress.interrupt_handler {
   257           dump(options, logic,
   258             aspects = aspects,
   259             progress = progress,
   260             dirs = dirs,
   261             select_dirs = select_dirs,
   262             output_dir = output_dir,
   263             commit_clean_delay = commit_clean_delay,
   264             watchdog_timeout = watchdog_timeout,
   265             verbose = verbose,
   266             selection = Sessions.Selection(
   267               requirements = requirements,
   268               all_sessions = all_sessions,
   269               base_sessions = base_sessions,
   270               exclude_session_groups = exclude_session_groups,
   271               exclude_sessions = exclude_sessions,
   272               session_groups = session_groups,
   273               sessions = sessions))
   274         }
   275 
   276       progress.echo(result.timing.message_resources)
   277 
   278       sys.exit(result.rc)
   279     })
   280 }