merged
authorwenzelm
Mon Oct 09 22:08:05 2017 +0200 (19 months ago)
changeset 668259f6ec65f7a6e
parent 66817 0b12755ccbb2
parent 66824 49a3a0a6ffaf
child 66826 0d60d2118544
child 66828 3c936ebebc23
merged
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Admin/afp.scala	Mon Oct 09 22:08:05 2017 +0200
     1.3 @@ -0,0 +1,77 @@
     1.4 +/*  Title:      Pure/Admin/afp.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Administrative support for the Archive of Formal Proofs.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object AFP
    1.14 +{
    1.15 +  def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
    1.16 +    new AFP(options, base_dir)
    1.17 +
    1.18 +  sealed case class Entry(name: String, sessions: List[String])
    1.19 +}
    1.20 +
    1.21 +class AFP private(options: Options, val base_dir: Path)
    1.22 +{
    1.23 +  override def toString: String = base_dir.expand.toString
    1.24 +
    1.25 +  val main_dir: Path = base_dir + Path.explode("thys")
    1.26 +
    1.27 +
    1.28 +  /* entries and sessions */
    1.29 +
    1.30 +  val entries: List[AFP.Entry] =
    1.31 +    (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
    1.32 +      val sessions =
    1.33 +        Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
    1.34 +      AFP.Entry(name, sessions)
    1.35 +    }).sortBy(_.name)
    1.36 +
    1.37 +  val sessions: List[String] = entries.flatMap(_.sessions)
    1.38 +
    1.39 +  val sessions_structure: Sessions.T =
    1.40 +    Sessions.load(options, dirs = List(main_dir)).
    1.41 +      selection(Sessions.Selection(sessions = sessions.toList))._2
    1.42 +
    1.43 +
    1.44 +  /* dependency graph */
    1.45 +
    1.46 +  private def sessions_deps(entry: AFP.Entry): List[String] =
    1.47 +    entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted
    1.48 +
    1.49 +  val entries_graph: Graph[String, Unit] =
    1.50 +  {
    1.51 +    val session_entries =
    1.52 +      (Multi_Map.empty[String, String] /: entries) { case (m1, e) =>
    1.53 +        (m1 /: e.sessions) { case (m2, s) => m2.insert(s, e.name) }
    1.54 +      }
    1.55 +    (Graph.empty[String, Unit] /: entries) { case (g, e1) =>
    1.56 +      val name1 = e1.name
    1.57 +      val g1 = g.default_node(name1, ())
    1.58 +      (g1 /: sessions_deps(e1)) { case (g2, s2) =>
    1.59 +        (g2 /: session_entries.get_list(s2)) { case (g3, name2) =>
    1.60 +          if (name1 == name2) g3 else g3.default_node(name2, ()).add_edge(name2, name1)
    1.61 +        }
    1.62 +      }
    1.63 +    }
    1.64 +  }
    1.65 +
    1.66 +  def entries_graph_display: Graph_Display.Graph =
    1.67 +    Graph_Display.make_graph(entries_graph)
    1.68 +
    1.69 +  def entries_json_text: String =
    1.70 +    (for (entry <- entries.iterator) yield {
    1.71 +      val distrib_deps = sessions_deps(entry).filterNot(sessions.contains(_))
    1.72 +      val afp_deps = entries_graph.imm_preds(entry.name).toList
    1.73 +      """
    1.74 + {""" + JSON.Format(entry.name) + """:
    1.75 +  {"distrib_deps": """ + JSON.Format(distrib_deps) + """,
    1.76 +   "afp_deps": """ + JSON.Format(afp_deps) + """
    1.77 +  }
    1.78 + }"""
    1.79 +    }).mkString("[", ", ", "\n]\n")
    1.80 +}
     2.1 --- a/src/Pure/General/graph_display.scala	Sun Oct 08 22:28:22 2017 +0200
     2.2 +++ b/src/Pure/General/graph_display.scala	Mon Oct 09 22:08:05 2017 +0200
     2.3 @@ -60,5 +60,13 @@
     2.4          import XML.Decode._
     2.5          list(pair(pair(string, pair(string, x => x)), list(string)))(body)
     2.6        })
     2.7 +
     2.8 +  def make_graph[A](
     2.9 +    graph: isabelle.Graph[String, A],
    2.10 +    name: (String, A) => String = (x: String, a: A) => x): Graph =
    2.11 +  {
    2.12 +    val entries =
    2.13 +      (for ((x, (a, (ps, _))) <- graph.iterator) yield ((x, (name(x, a), Nil)), ps.toList)).toList
    2.14 +    build_graph(entries)
    2.15 +  }
    2.16  }
    2.17 -
     3.1 --- a/src/Pure/Thy/sessions.scala	Sun Oct 08 22:28:22 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 09 22:08:05 2017 +0200
     3.3 @@ -116,7 +116,7 @@
     3.4      overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     3.5      imported_sources: List[(Path, SHA1.Digest)] = Nil,
     3.6      sources: List[(Path, SHA1.Digest)] = Nil,
     3.7 -    session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
     3.8 +    session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph,
     3.9      errors: List[String] = Nil,
    3.10      imports: Option[Base] = None)
    3.11    {
    3.12 @@ -253,7 +253,7 @@
    3.13                  progress, overall_syntax.keywords, check_keywords, theory_files)
    3.14              }
    3.15  
    3.16 -            val session_graph: Graph_Display.Graph =
    3.17 +            val session_graph_display: Graph_Display.Graph =
    3.18              {
    3.19                def session_node(name: String): Graph_Display.Node =
    3.20                  Graph_Display.Node("[" + name + "]", "session." + name)
    3.21 @@ -303,7 +303,7 @@
    3.22                  overall_syntax = overall_syntax,
    3.23                  imported_sources = check_sources(imported_files),
    3.24                  sources = check_sources(session_files),
    3.25 -                session_graph = session_graph,
    3.26 +                session_graph_display = session_graph_display,
    3.27                  errors = thy_deps.errors ::: sources_errors,
    3.28                  imports = Some(imports_base))
    3.29  
    3.30 @@ -479,6 +479,9 @@
    3.31        val build_graph: Graph[String, Info],
    3.32        val imports_graph: Graph[String, Info])
    3.33    {
    3.34 +    def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
    3.35 +    def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
    3.36 +
    3.37      def apply(name: String): Info = imports_graph.get_node(name)
    3.38      def get(name: String): Option[Info] =
    3.39        if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
    3.40 @@ -550,26 +553,26 @@
    3.41        (THEORIES, Keyword.QUASI_COMMAND) +
    3.42        (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
    3.43  
    3.44 +  abstract class Entry
    3.45 +  sealed case class Chapter(name: String) extends Entry
    3.46 +  sealed case class Session_Entry(
    3.47 +    pos: Position.T,
    3.48 +    name: String,
    3.49 +    groups: List[String],
    3.50 +    path: String,
    3.51 +    parent: Option[String],
    3.52 +    description: String,
    3.53 +    options: List[Options.Spec],
    3.54 +    imports: List[String],
    3.55 +    theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
    3.56 +    document_files: List[(String, String)]) extends Entry
    3.57 +  {
    3.58 +    def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
    3.59 +      theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
    3.60 +  }
    3.61 +
    3.62    private object Parser extends Parse.Parser with Options.Parser
    3.63    {
    3.64 -    private abstract class Entry
    3.65 -    private sealed case class Chapter(name: String) extends Entry
    3.66 -    private sealed case class Session_Entry(
    3.67 -      pos: Position.T,
    3.68 -      name: String,
    3.69 -      groups: List[String],
    3.70 -      path: String,
    3.71 -      parent: Option[String],
    3.72 -      description: String,
    3.73 -      options: List[Options.Spec],
    3.74 -      imports: List[String],
    3.75 -      theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
    3.76 -      document_files: List[(String, String)]) extends Entry
    3.77 -    {
    3.78 -      def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
    3.79 -        theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
    3.80 -    }
    3.81 -
    3.82      private val chapter: Parser[Chapter] =
    3.83      {
    3.84        val chapter_name = atom("chapter name", _.is_name)
    3.85 @@ -618,70 +621,88 @@
    3.86              Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
    3.87      }
    3.88  
    3.89 -    def parse_root(options: Options, select: Boolean, path: Path): List[(String, Info)] =
    3.90 +    def parse_root(path: Path): List[Entry] =
    3.91      {
    3.92 -      def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) =
    3.93 -      {
    3.94 -        try {
    3.95 -          val name = entry.name
    3.96 -
    3.97 -          if (name == "" || name == DRAFT) error("Bad session name")
    3.98 -          if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
    3.99 -          if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
   3.100 -
   3.101 -          val session_options = options ++ entry.options
   3.102 -
   3.103 -          val theories =
   3.104 -            entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
   3.105 -
   3.106 -          val global_theories =
   3.107 -            for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
   3.108 -            yield {
   3.109 -              val thy_name = Path.explode(thy).expand.base_name
   3.110 -              if (Long_Name.is_qualified(thy_name))
   3.111 -                error("Bad qualified name for global theory " +
   3.112 -                  quote(thy_name) + Position.here(pos))
   3.113 -              else thy_name
   3.114 -            }
   3.115 -
   3.116 -          val document_files =
   3.117 -            entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
   3.118 -
   3.119 -          val meta_digest =
   3.120 -            SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports,
   3.121 -              entry.theories_no_position, entry.document_files).toString)
   3.122 -
   3.123 -          val info =
   3.124 -            Info(name, entry_chapter, select, entry.pos, entry.groups,
   3.125 -              path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
   3.126 -              entry.imports, theories, global_theories, document_files, meta_digest)
   3.127 -
   3.128 -          (name, info)
   3.129 -        }
   3.130 -        catch {
   3.131 -          case ERROR(msg) =>
   3.132 -            error(msg + "\nThe error(s) above occurred in session entry " +
   3.133 -              quote(entry.name) + Position.here(entry.pos))
   3.134 -        }
   3.135 -      }
   3.136 -
   3.137        val toks = Token.explode(root_syntax.keywords, File.read(path))
   3.138        val start = Token.Pos.file(path.implode)
   3.139  
   3.140        parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
   3.141 -        case Success(result, _) =>
   3.142 -          var entry_chapter = "Unsorted"
   3.143 -          val infos = new mutable.ListBuffer[(String, Info)]
   3.144 -          result.foreach {
   3.145 -            case Chapter(name) => entry_chapter = name
   3.146 -            case entry: Session_Entry => infos += make_info(entry_chapter, entry)
   3.147 -          }
   3.148 -          infos.toList
   3.149 +        case Success(result, _) => result
   3.150          case bad => error(bad.toString)
   3.151        }
   3.152      }
   3.153    }
   3.154  
   3.155 +  def parse_root(path: Path): List[Entry] = Parser.parse_root(path)
   3.156 +
   3.157 +  def parse_root_entries(path: Path): List[Session_Entry] =
   3.158 +    for (entry <- Parser.parse_root(path) if entry.isInstanceOf[Session_Entry])
   3.159 +    yield entry.asInstanceOf[Session_Entry]
   3.160 +
   3.161 +  def read_root(options: Options, select: Boolean, path: Path): List[(String, Info)] =
   3.162 +  {
   3.163 +    def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) =
   3.164 +    {
   3.165 +      try {
   3.166 +        val name = entry.name
   3.167 +
   3.168 +        if (name == "" || name == DRAFT) error("Bad session name")
   3.169 +        if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
   3.170 +        if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
   3.171 +
   3.172 +        val session_options = options ++ entry.options
   3.173 +
   3.174 +        val theories =
   3.175 +          entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
   3.176 +
   3.177 +        val global_theories =
   3.178 +          for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
   3.179 +          yield {
   3.180 +            val thy_name = Path.explode(thy).expand.base_name
   3.181 +            if (Long_Name.is_qualified(thy_name))
   3.182 +              error("Bad qualified name for global theory " +
   3.183 +                quote(thy_name) + Position.here(pos))
   3.184 +            else thy_name
   3.185 +          }
   3.186 +
   3.187 +        val document_files =
   3.188 +          entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
   3.189 +
   3.190 +        val meta_digest =
   3.191 +          SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports,
   3.192 +            entry.theories_no_position, entry.document_files).toString)
   3.193 +
   3.194 +        val info =
   3.195 +          Info(name, entry_chapter, select, entry.pos, entry.groups,
   3.196 +            path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
   3.197 +            entry.imports, theories, global_theories, document_files, meta_digest)
   3.198 +
   3.199 +        (name, info)
   3.200 +      }
   3.201 +      catch {
   3.202 +        case ERROR(msg) =>
   3.203 +          error(msg + "\nThe error(s) above occurred in session entry " +
   3.204 +            quote(entry.name) + Position.here(entry.pos))
   3.205 +      }
   3.206 +    }
   3.207 +
   3.208 +    var entry_chapter = "Unsorted"
   3.209 +    val infos = new mutable.ListBuffer[(String, Info)]
   3.210 +    parse_root(path).foreach {
   3.211 +      case Chapter(name) => entry_chapter = name
   3.212 +      case entry: Session_Entry => infos += make_info(entry_chapter, entry)
   3.213 +    }
   3.214 +    infos.toList
   3.215 +  }
   3.216 +
   3.217 +  def parse_roots(roots: Path): List[String] =
   3.218 +  {
   3.219 +    for {
   3.220 +      line <- split_lines(File.read(roots))
   3.221 +      if !(line == "" || line.startsWith("#"))
   3.222 +    } yield line
   3.223 +  }
   3.224 +
   3.225  
   3.226    /* load sessions from certain directories */
   3.227  
   3.228 @@ -714,10 +735,9 @@
   3.229        val roots = dir + ROOTS
   3.230        if (roots.is_file) {
   3.231          for {
   3.232 -          line <- split_lines(File.read(roots))
   3.233 -          if !(line == "" || line.startsWith("#"))
   3.234 +          entry <- parse_roots(roots)
   3.235            dir1 =
   3.236 -            try { check_session_dir(dir + Path.explode(line)) }
   3.237 +            try { check_session_dir(dir + Path.explode(entry)) }
   3.238              catch {
   3.239                case ERROR(msg) =>
   3.240                  error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
   3.241 @@ -743,7 +763,7 @@
   3.242          }
   3.243        }).toList.map(_._2)
   3.244  
   3.245 -    make(unique_roots.flatMap(p => Parser.parse_root(options, p._1, p._2)))
   3.246 +    make(unique_roots.flatMap(p => read_root(options, p._1, p._2)))
   3.247    }
   3.248  
   3.249  
     4.1 --- a/src/Pure/Tools/build.scala	Sun Oct 08 22:28:22 2017 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 09 22:08:05 2017 +0200
     4.3 @@ -198,7 +198,7 @@
     4.4        }
     4.5  
     4.6      private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
     4.7 -    isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph)
     4.8 +    isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
     4.9  
    4.10      private val future_result: Future[Process_Result] =
    4.11        Future.thread("build") {
     5.1 --- a/src/Pure/build-jars	Sun Oct 08 22:28:22 2017 +0200
     5.2 +++ b/src/Pure/build-jars	Mon Oct 09 22:08:05 2017 +0200
     5.3 @@ -9,6 +9,7 @@
     5.4  ## sources
     5.5  
     5.6  declare -a SOURCES=(
     5.7 +  Admin/afp.scala
     5.8    Admin/build_cygwin.scala
     5.9    Admin/build_doc.scala
    5.10    Admin/build_history.scala