command-line tool "isabelle export";
authorwenzelm
Tue May 08 20:24:08 2018 +0200 (13 months ago)
changeset 68116ac82ee617a75
parent 68115 23c6ae3dd3a0
child 68117 7e349d1e3c95
command-line tool "isabelle export";
more documentation;
tuned;
NEWS
src/Doc/System/Sessions.thy
src/Pure/System/isabelle_tool.scala
src/Pure/Thy/export.scala
     1.1 --- a/NEWS	Tue May 08 15:41:52 2018 +0200
     1.2 +++ b/NEWS	Tue May 08 20:24:08 2018 +0200
     1.3 @@ -327,8 +327,17 @@
     1.4  INCOMPATIBILITY.
     1.5  
     1.6  
     1.7 +*** ML ***
     1.8 +
     1.9 +* Operation Export.export emits theory exports (arbitrary blobs), which
    1.10 +are stored persistently in the session build database.
    1.11 +
    1.12 +
    1.13  *** System ***
    1.14  
    1.15 +* The command-line tool retrieves theory exports from the session build
    1.16 +database.
    1.17 +
    1.18  * The command-line tools "isabelle server" and "isabelle client" provide
    1.19  access to the Isabelle Server: it supports responsive session management
    1.20  and concurrent use of theories, based on Isabelle/PIDE infrastructure.
     2.1 --- a/src/Doc/System/Sessions.thy	Tue May 08 15:41:52 2018 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Tue May 08 20:24:08 2018 +0200
     2.3 @@ -545,4 +545,50 @@
     2.4    @{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>}
     2.5  \<close>
     2.6  
     2.7 +
     2.8 +section \<open>Retrieve theory exports\<close>
     2.9 +
    2.10 +text \<open>
    2.11 +  The @{tool_def "export"} tool retrieves theory exports from the session
    2.12 +  database. Its command-line usage is: @{verbatim [display]
    2.13 +\<open>Usage: isabelle export [OPTIONS] SESSION
    2.14 +
    2.15 +  Options are:
    2.16 +    -D DIR       target directory for exported files (default: "export")
    2.17 +    -d DIR       include session directory
    2.18 +    -l           list exports
    2.19 +    -n           no build of session
    2.20 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    2.21 +    -s           system build mode for session image
    2.22 +    -x PATTERN   extract files matching pattern (e.g. "*:**" for all)
    2.23 +
    2.24 +  List or export theory exports for SESSION: named blobs produced by
    2.25 +  isabelle build. Option -l or -x is required.
    2.26 +
    2.27 +  The PATTERN language resembles glob patterns in the shell, with ? and *
    2.28 +  (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
    2.29 +  and variants {pattern1,pattern2,pattern3}.\<close>}
    2.30 +
    2.31 +  \<^medskip>
    2.32 +  The specified session is updated via @{tool build}
    2.33 +  (\secref{sec:tool-build}), with the same options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close>. The
    2.34 +  option \<^verbatim>\<open>-n\<close> suppresses the implicit build process: it means that a
    2.35 +  potentially outdated session database is used!
    2.36 +
    2.37 +  \<^medskip>
    2.38 +  Option \<^verbatim>\<open>-l\<close> lists all stored exports, with compound names
    2.39 +  \<open>theory\<close>\<^verbatim>\<open>:\<close>\<open>name\<close>.
    2.40 +
    2.41 +  \<^medskip>
    2.42 +  Option \<^verbatim>\<open>-x\<close> extracts stored exports whose compound name matches the given
    2.43 +  pattern. Note that wild cards ``\<^verbatim>\<open>?\<close>'' and ``\<^verbatim>\<open>*\<close>'' do not match the
    2.44 +  separators ``\<^verbatim>\<open>:\<close>'' and ``\<^verbatim>\<open>/\<close>''; the wild card \<^verbatim>\<open>**\<close> matches over directory
    2.45 +  name hierarchies separated by ``\<^verbatim>\<open>/\<close>''. Thus the pattern ``\<^verbatim>\<open>*:**\<close>'' matches
    2.46 +  \<^emph>\<open>all\<close> theory exports.
    2.47 +
    2.48 +  Option \<^verbatim>\<open>-D\<close> specifies an alternative base directory for option \<^verbatim>\<open>-x\<close>: the
    2.49 +  default is \<^verbatim>\<open>export\<close> within the current directory. Each theory creates its
    2.50 +  own sub-directory hierarchy, using the session-qualified theory name.
    2.51 +\<close>
    2.52 +
    2.53  end
     3.1 --- a/src/Pure/System/isabelle_tool.scala	Tue May 08 15:41:52 2018 +0200
     3.2 +++ b/src/Pure/System/isabelle_tool.scala	Tue May 08 20:24:08 2018 +0200
     3.3 @@ -109,6 +109,7 @@
     3.4        Build_Status.isabelle_tool,
     3.5        Check_Sources.isabelle_tool,
     3.6        Doc.isabelle_tool,
     3.7 +      Export.isabelle_tool,
     3.8        Imports.isabelle_tool,
     3.9        Mkroot.isabelle_tool,
    3.10        ML_Process.isabelle_tool,
     4.1 --- a/src/Pure/Thy/export.scala	Tue May 08 15:41:52 2018 +0200
     4.2 +++ b/src/Pure/Thy/export.scala	Tue May 08 20:24:08 2018 +0200
     4.3 @@ -6,6 +6,11 @@
     4.4  
     4.5  package isabelle
     4.6  
     4.7 +
     4.8 +import scala.annotation.tailrec
     4.9 +import scala.util.matching.Regex
    4.10 +
    4.11 +
    4.12  object Export
    4.13  {
    4.14    /* SQL data model */
    4.15 @@ -21,9 +26,17 @@
    4.16      val table =
    4.17        SQL.Table("isabelle_exports", List(session_name, theory_name, name, compressed, body))
    4.18  
    4.19 -    def where_equal(session_name: String, theory_name: String): SQL.Source =
    4.20 +    def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
    4.21        "WHERE " + Data.session_name.equal(session_name) +
    4.22 -      " AND " + Data.theory_name.equal(theory_name)
    4.23 +        (if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) +
    4.24 +        (if (name == "") "" else " AND " + Data.name.equal(name))
    4.25 +  }
    4.26 +
    4.27 +  def read_name(db: SQL.Database, session_name: String, theory_name: String, name: String): Boolean =
    4.28 +  {
    4.29 +    val select =
    4.30 +      Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name, name))
    4.31 +    db.using_statement(select)(stmt => stmt.execute_query().next())
    4.32    }
    4.33  
    4.34    def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] =
    4.35 @@ -33,17 +46,19 @@
    4.36        stmt.execute_query().iterator(res => res.string(Data.name)).toList)
    4.37    }
    4.38  
    4.39 -  def read_name(db: SQL.Database, session_name: String, theory_name: String, name: String): Boolean =
    4.40 +  def read_theory_names(db: SQL.Database, session_name: String): List[(String, String)] =
    4.41    {
    4.42 -    val select =
    4.43 -      Data.table.select(List(Data.name),
    4.44 -        Data.where_equal(session_name, theory_name) + " AND " + Data.name.equal(name))
    4.45 -    db.using_statement(select)(stmt => stmt.execute_query().next())
    4.46 +    val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name))
    4.47 +    db.using_statement(select)(stmt =>
    4.48 +      stmt.execute_query().iterator(res =>
    4.49 +        (res.string(Data.theory_name), res.string(Data.name))).toList)
    4.50    }
    4.51  
    4.52    def message(msg: String, theory_name: String, name: String): String =
    4.53      msg + " " + quote(name) + " for theory " + quote(theory_name)
    4.54  
    4.55 +  def compound_name(a: String, b: String): String = a + ":" + b
    4.56 +
    4.57    sealed case class Entry(
    4.58      session_name: String,
    4.59      theory_name: String,
    4.60 @@ -51,7 +66,7 @@
    4.61      compressed: Boolean,
    4.62      body: Future[Bytes])
    4.63    {
    4.64 -    override def toString: String = theory_name + ":" + name
    4.65 +    override def toString: String = compound_name(theory_name, name)
    4.66  
    4.67      def write(db: SQL.Database)
    4.68      {
    4.69 @@ -66,6 +81,27 @@
    4.70          stmt.execute()
    4.71        })
    4.72      }
    4.73 +
    4.74 +    def body_uncompressed: Bytes =
    4.75 +      if (compressed) body.join.uncompress() else body.join
    4.76 +  }
    4.77 +
    4.78 +  def make_regex(pattern: String): Regex =
    4.79 +  {
    4.80 +    @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex =
    4.81 +      chs match {
    4.82 +        case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest)
    4.83 +        case '*' :: rest => make("[^:/]*" :: result, depth, rest)
    4.84 +        case '?' :: rest => make("[^:/]" :: result, depth, rest)
    4.85 +        case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest)
    4.86 +        case '{' :: rest => make("(" :: result, depth + 1, rest)
    4.87 +        case ',' :: rest if depth > 0 => make("|" :: result, depth, rest)
    4.88 +        case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest)
    4.89 +        case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest)
    4.90 +        case c :: rest => make(c.toString :: result, depth, rest)
    4.91 +        case Nil => result.reverse.mkString.r
    4.92 +      }
    4.93 +    make(Nil, 0, pattern.toList)
    4.94    }
    4.95  
    4.96    def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry =
    4.97 @@ -78,7 +114,7 @@
    4.98    {
    4.99      val select =
   4.100        Data.table.select(List(Data.compressed, Data.body),
   4.101 -        Data.where_equal(session_name, theory_name) + " AND " + Data.name.equal(name))
   4.102 +        Data.where_equal(session_name, theory_name, name))
   4.103      db.using_statement(select)(stmt =>
   4.104      {
   4.105        val res = stmt.execute_query()
   4.106 @@ -126,4 +162,113 @@
   4.107        export_errors.value.reverse
   4.108      }
   4.109    }
   4.110 +
   4.111 +
   4.112 +  /* Isabelle tool wrapper */
   4.113 +
   4.114 +  val default_export_dir = Path.explode("export")
   4.115 +
   4.116 +  val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args =>
   4.117 +  {
   4.118 +    /* arguments */
   4.119 +
   4.120 +    var export_dir = default_export_dir
   4.121 +    var dirs: List[Path] = Nil
   4.122 +    var export_list = false
   4.123 +    var no_build = false
   4.124 +    var options = Options.init()
   4.125 +    var system_mode = false
   4.126 +    var export_pattern = ""
   4.127 +
   4.128 +    val getopts = Getopts("""
   4.129 +Usage: isabelle export [OPTIONS] SESSION
   4.130 +
   4.131 +  Options are:
   4.132 +    -D DIR       target directory for exported files (default: """ + default_export_dir + """)
   4.133 +    -d DIR       include session directory
   4.134 +    -l           list exports
   4.135 +    -n           no build of session
   4.136 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   4.137 +    -s           system build mode for session image
   4.138 +    -x PATTERN   extract files matching pattern (e.g. "*:**" for all)
   4.139 +
   4.140 +  List or export theory exports for SESSION: named blobs produced by
   4.141 +  isabelle build. Option -l or -x is required.
   4.142 +
   4.143 +  The PATTERN language resembles glob patterns in the shell, with ? and *
   4.144 +  (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
   4.145 +  and variants {pattern1,pattern2,pattern3}.
   4.146 +""",
   4.147 +      "D:" -> (arg => export_dir = Path.explode(arg)),
   4.148 +      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   4.149 +      "l" -> (_ => export_list = true),
   4.150 +      "n" -> (_ => no_build = true),
   4.151 +      "o:" -> (arg => options = options + arg),
   4.152 +      "s" -> (_ => system_mode = true),
   4.153 +      "x:" -> (arg => export_pattern = arg))
   4.154 +
   4.155 +    val more_args = getopts(args)
   4.156 +    val session_name =
   4.157 +      more_args match {
   4.158 +        case List(session_name) if export_list || export_pattern != "" => session_name
   4.159 +        case _ => getopts.usage()
   4.160 +      }
   4.161 +
   4.162 +
   4.163 +    /* build */
   4.164 +
   4.165 +    val progress = new Console_Progress()
   4.166 +
   4.167 +    if (!no_build &&
   4.168 +        !Build.build(options, no_build = true, dirs = dirs, system_mode = system_mode,
   4.169 +          sessions = List(session_name)).ok)
   4.170 +    {
   4.171 +      progress.echo("Build started for Isabelle/" + session_name + " ...")
   4.172 +      progress.interrupt_handler {
   4.173 +        val res =
   4.174 +          Build.build(options, progress = progress, dirs = dirs, system_mode = system_mode,
   4.175 +            sessions = List(session_name))
   4.176 +        if (!res.ok) sys.exit(res.rc)
   4.177 +      }
   4.178 +    }
   4.179 +
   4.180 +
   4.181 +    /* database */
   4.182 +
   4.183 +    val store = Sessions.store(system_mode)
   4.184 +    val database =
   4.185 +      store.find_database(session_name) match {
   4.186 +        case None => error("Missing database for session " + quote(session_name))
   4.187 +        case Some(database) => database
   4.188 +      }
   4.189 +
   4.190 +    using(SQLite.open_database(database))(db =>
   4.191 +    {
   4.192 +      db.transaction {
   4.193 +        val export_names = read_theory_names(db, session_name)
   4.194 +
   4.195 +        // list
   4.196 +        if (export_list) {
   4.197 +          (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
   4.198 +            sorted.foreach(Output.writeln(_, stdout = true))
   4.199 +        }
   4.200 +
   4.201 +        // export
   4.202 +        if (export_pattern != "") {
   4.203 +          val regex = make_regex(export_pattern)
   4.204 +          for {
   4.205 +            (theory_name, name) <- export_names
   4.206 +            if regex.pattern.matcher(compound_name(theory_name, name)).matches
   4.207 +          } {
   4.208 +            val entry = read_entry(db, session_name, theory_name, name)
   4.209 +            val path = export_dir + Path.basic(theory_name) + Path.explode(name)
   4.210 +
   4.211 +            progress.echo("exporting " + path)
   4.212 +            Isabelle_System.mkdirs(path.dir)
   4.213 +            Bytes.write(path, entry.body_uncompressed)
   4.214 +          }
   4.215 +        }
   4.216 +      }
   4.217 +    })
   4.218 +  })
   4.219  }