clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
authorwenzelm
Fri Feb 15 17:00:21 2019 +0100 (7 months ago)
changeset 6981118f61ce86425
parent 69810 a23d6ff31f79
child 69812 9487788a94c1
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
tuned messages;
NEWS
src/Doc/System/Sessions.thy
src/Pure/Thy/export.scala
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Fri Feb 15 12:34:29 2019 +0100
     1.2 +++ b/NEWS	Fri Feb 15 17:00:21 2019 +0100
     1.3 @@ -104,10 +104,10 @@
     1.4  
     1.5  * Code generation: command 'export_code' without file keyword exports
     1.6  code as regular theory export, which can be materialized using the
     1.7 -command-line tool "isabelle export" or 'export_files' in the session
     1.8 -ROOT, or browsed in Isabelle/jEdit via the "isabelle-export:"
     1.9 -file-system. To get generated code dumped into output, use "file \<open>\<close>".
    1.10 -Minor INCOMPATIBILITY.
    1.11 +command-line tools "isabelle export" or "isabelle build -e" (with
    1.12 +'export_files' in the session ROOT), or browsed in Isabelle/jEdit via
    1.13 +the "isabelle-export:" file-system. To get generated code dumped into
    1.14 +output, use "file \<open>\<close>". Minor INCOMPATIBILITY.
    1.15  
    1.16  * Code generation for OCaml: proper strings are used for literals.
    1.17  Minor INCOMPATIBILITY.
    1.18 @@ -721,7 +721,9 @@
    1.19  *** ML ***
    1.20  
    1.21  * Operation Export.export emits theory exports (arbitrary blobs), which
    1.22 -are stored persistently in the session build database.
    1.23 +are stored persistently in the session build database. Command-line
    1.24 +tools "isabelle export" and "isabelle build -e" allow to materialize
    1.25 +exports in the physical file-system.
    1.26  
    1.27  * Command 'ML_export' exports ML toplevel bindings to the global
    1.28  bootstrap environment of the ML process. This allows ML evaluation
    1.29 @@ -777,8 +779,9 @@
    1.30  * Command-line tool "isabelle imports -I" also reports actual session
    1.31  imports. This helps to minimize the session dependency graph.
    1.32  
    1.33 -* The command-line tool "export" and 'export_files' in session ROOT
    1.34 -entries retrieve theory exports from the session build database.
    1.35 +* The command-line tool "export" and "isabelle build -e" (with
    1.36 +'export_files' in session ROOT entries) retrieve theory exports from the
    1.37 +session build database.
    1.38  
    1.39  * The command-line tools "isabelle server" and "isabelle client" provide
    1.40  access to the Isabelle Server: it supports responsive session management
     2.1 --- a/src/Doc/System/Sessions.thy	Fri Feb 15 12:34:29 2019 +0100
     2.2 +++ b/src/Doc/System/Sessions.thy	Fri Feb 15 17:00:21 2019 +0100
     2.3 @@ -145,13 +145,14 @@
     2.4    \<^verbatim>\<open>document\<close> within the session root directory.
     2.5  
     2.6    \<^descr> \isakeyword{export_files}~\<open>(\<close>\isakeyword{in}~\<open>target_dir) [number]
     2.7 -  patterns\<close> writes theory exports to the file-system: the \<open>target_dir\<close>
     2.8 -  specification is relative to the session root directory; its default is
     2.9 -  \<^verbatim>\<open>export\<close>. Exports are selected via \<open>patterns\<close> as in @{tool_ref export}
    2.10 -  (\secref{sec:tool-export}). The number given in brackets (default: 0)
    2.11 -  specifies elements that should be pruned from each name: it allows to reduce
    2.12 -  the resulting directory hierarchy at the danger of overwriting files due to
    2.13 -  loss of uniqueness.
    2.14 +  patterns\<close> specifies theory exports that may get written to the file-system,
    2.15 +  e.g. via @{tool_ref build} with option \<^verbatim>\<open>-e\<close> (\secref{sec:tool-build}). The
    2.16 +  \<open>target_dir\<close> specification is relative to the session root directory; its
    2.17 +  default is \<^verbatim>\<open>export\<close>. Exports are selected via \<open>patterns\<close> as in @{tool_ref
    2.18 +  export} (\secref{sec:tool-export}). The number given in brackets (default:
    2.19 +  0) specifies elements that should be pruned from each name: it allows to
    2.20 +  reduce the resulting directory hierarchy at the danger of overwriting files
    2.21 +  due to loss of uniqueness.
    2.22  \<close>
    2.23  
    2.24  
    2.25 @@ -288,6 +289,7 @@
    2.26      -b           build heap images
    2.27      -c           clean build
    2.28      -d DIR       include session directory
    2.29 +    -e           export files from session specification into file-system
    2.30      -f           fresh build
    2.31      -g NAME      select session group NAME
    2.32      -j INT       maximum number of parallel jobs (default 1)
    2.33 @@ -374,6 +376,15 @@
    2.34    parent or import graph) before performing the specified build operation.
    2.35  
    2.36    \<^medskip>
    2.37 +  Option \<^verbatim>\<open>-e\<close> executes the \isakeyword{export_files} directives from the ROOT
    2.38 +  specification of all explicitly selected sessions: the status of the session
    2.39 +  build database needs to be OK, but the session could have been built
    2.40 +  earlier. Using \isakeyword{export_files}, a session may serve as abstract
    2.41 +  interface for add-on build artefacts, but these are only materialized on
    2.42 +  explicit request: without option \<^verbatim>\<open>-e\<close> there is no effect on the physical
    2.43 +  file-system yet.
    2.44 +
    2.45 +  \<^medskip>
    2.46    Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
    2.47    requirements.
    2.48  
     3.1 --- a/src/Pure/Thy/export.scala	Fri Feb 15 12:34:29 2019 +0100
     3.2 +++ b/src/Pure/Thy/export.scala	Fri Feb 15 17:00:21 2019 +0100
     3.3 @@ -264,8 +264,7 @@
     3.4      progress: Progress = No_Progress,
     3.5      export_prune: Int = 0,
     3.6      export_list: Boolean = false,
     3.7 -    export_patterns: List[String] = Nil,
     3.8 -    export_prefix: String = "")
     3.9 +    export_patterns: List[String] = Nil)
    3.10    {
    3.11      using(store.open_database(session_name))(db =>
    3.12      {
    3.13 @@ -298,7 +297,7 @@
    3.14                }
    3.15                else export_dir + Path.make(elems.drop(export_prune))
    3.16  
    3.17 -            progress.echo(export_prefix + "export " + path)
    3.18 +            progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
    3.19              Isabelle_System.mkdirs(path.dir)
    3.20              Bytes.write(path, entry.uncompressed(cache = store.xz_cache))
    3.21              File.set_executable(path, entry.executable)
     4.1 --- a/src/Pure/Tools/build.scala	Fri Feb 15 12:34:29 2019 +0100
     4.2 +++ b/src/Pure/Tools/build.scala	Fri Feb 15 17:00:21 2019 +0100
     4.3 @@ -334,16 +334,8 @@
     4.4  
     4.5        Isabelle_System.rm_tree(export_tmp_dir)
     4.6  
     4.7 -      if (result1.ok) {
     4.8 -        for ((dir, prune, pats) <- info.export_files) {
     4.9 -          Export.export_files(store, name, info.dir + dir,
    4.10 -            progress = if (verbose) progress else No_Progress,
    4.11 -            export_prune = prune,
    4.12 -            export_patterns = pats,
    4.13 -            export_prefix = name + ": ")
    4.14 -        }
    4.15 +      if (result1.ok)
    4.16          Present.finish(progress, store.browser_info, graph_file, info, name)
    4.17 -      }
    4.18  
    4.19        graph_file.delete
    4.20  
    4.21 @@ -405,6 +397,7 @@
    4.22      soft_build: Boolean = false,
    4.23      system_mode: Boolean = false,
    4.24      verbose: Boolean = false,
    4.25 +    export_files: Boolean = false,
    4.26      pide: Boolean = false,
    4.27      requirements: Boolean = false,
    4.28      all_sessions: Boolean = false,
    4.29 @@ -640,8 +633,8 @@
    4.30  
    4.31                    val numa_node = numa_nodes.next(used_node(_))
    4.32                    val job =
    4.33 -                    new Job(progress, name, info, deps, store, do_output,
    4.34 -                      verbose, pide, numa_node, queue.command_timings(name))
    4.35 +                    new Job(progress, name, info, deps, store, do_output, verbose, pide = pide,
    4.36 +                      numa_node, queue.command_timings(name))
    4.37                    loop(pending, running + (name -> (ancestor_heaps, job)), results)
    4.38                  }
    4.39                  else {
    4.40 @@ -672,6 +665,21 @@
    4.41          (for ((name, result) <- results0.iterator)
    4.42            yield (name, (result.process, result.info))).toMap)
    4.43  
    4.44 +    if (export_files) {
    4.45 +      for (name <- full_sessions.imports_selection(selection1).iterator if results(name).ok) {
    4.46 +        val info = results.info(name)
    4.47 +        if (info.export_files.nonEmpty) {
    4.48 +          progress.echo("Exporting " + info.name + " ...")
    4.49 +          for ((dir, prune, pats) <- info.export_files) {
    4.50 +            Export.export_files(store, name, info.dir + dir,
    4.51 +              progress = if (verbose) progress else No_Progress,
    4.52 +              export_prune = prune,
    4.53 +              export_patterns = pats)
    4.54 +          }
    4.55 +        }
    4.56 +      }
    4.57 +    }
    4.58 +
    4.59      if (results.rc != 0 && (verbose || !no_build)) {
    4.60        val unfinished =
    4.61          (for {
    4.62 @@ -721,6 +729,7 @@
    4.63      var build_heap = false
    4.64      var clean_build = false
    4.65      var dirs: List[Path] = Nil
    4.66 +    var export_files = false
    4.67      var fresh_build = false
    4.68      var session_groups: List[String] = Nil
    4.69      var max_jobs = 1
    4.70 @@ -747,6 +756,7 @@
    4.71      -b           build heap images
    4.72      -c           clean build
    4.73      -d DIR       include session directory
    4.74 +    -e           export files from session specification into file-system
    4.75      -f           fresh build
    4.76      -g NAME      select session group NAME
    4.77      -j INT       maximum number of parallel jobs (default 1)
    4.78 @@ -772,6 +782,7 @@
    4.79        "b" -> (_ => build_heap = true),
    4.80        "c" -> (_ => clean_build = true),
    4.81        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    4.82 +      "e" -> (_ => export_files = true),
    4.83        "f" -> (_ => fresh_build = true),
    4.84        "g:" -> (arg => session_groups = session_groups ::: List(arg)),
    4.85        "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
    4.86 @@ -814,6 +825,7 @@
    4.87            soft_build = soft_build,
    4.88            system_mode = system_mode,
    4.89            verbose = verbose,
    4.90 +          export_files = export_files,
    4.91            pide = pide,
    4.92            requirements = requirements,
    4.93            all_sessions = all_sessions,