continuously clean frontier of already committed theories: much less resource requirements;
authorwenzelm
Fri Sep 07 23:47:26 2018 +0200 (9 months ago)
changeset 6893690c08c7bab9c
parent 68935 7a420bee1eea
child 68937 cbf5475a0f66
continuously clean frontier of already committed theories: much less resource requirements;
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Fri Sep 07 20:35:18 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Fri Sep 07 23:47:26 2018 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  
     1.5  import java.io.{File => JFile}
     1.6  
     1.7 +import scala.annotation.tailrec
     1.8 +
     1.9  
    1.10  object Thy_Resources
    1.11  {
    1.12 @@ -78,6 +80,7 @@
    1.13  
    1.14    val default_check_delay: Double = 0.5
    1.15    val default_nodes_status_delay: Double = -1.0
    1.16 +  val default_commit_clean_delay: Double = 60.0
    1.17  
    1.18  
    1.19    class Session private[Thy_Resources](
    1.20 @@ -135,6 +138,7 @@
    1.21        }
    1.22  
    1.23        def cancel_result { result.cancel }
    1.24 +      def finished_result: Boolean = result.is_finished
    1.25        def await_result { result.join_result }
    1.26        def join_result: Theories_Result = result.join
    1.27        def check_result(
    1.28 @@ -197,6 +201,7 @@
    1.29        id: UUID = UUID(),
    1.30        // commit: must not block, must not fail
    1.31        commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
    1.32 +      commit_clean_delay: Time = Time.seconds(default_commit_clean_delay),
    1.33        progress: Progress = No_Progress): Theories_Result =
    1.34      {
    1.35        val dep_theories =
    1.36 @@ -241,6 +246,12 @@
    1.37              progress.nodes_status(use_theories_state.value.nodes_status)
    1.38            }
    1.39  
    1.40 +        val delay_commit_clean =
    1.41 +          Standard_Thread.delay_first(commit_clean_delay max Time.zero) {
    1.42 +            val clean = use_theories_state.value.already_committed.keySet
    1.43 +            resources.clean_theories(session, id, clean)
    1.44 +          }
    1.45 +
    1.46          Session.Consumer[Session.Commands_Changed](getClass.getName) {
    1.47            case changed =>
    1.48              if (changed.nodes.exists(dep_theories_set)) {
    1.49 @@ -291,6 +302,12 @@
    1.50                  progress.theory_percentage("", theory, percentage)
    1.51  
    1.52                check_result()
    1.53 +
    1.54 +              if (commit.isDefined && commit_clean_delay >= Time.zero) {
    1.55 +                if (use_theories_state.value.finished_result)
    1.56 +                  delay_commit_clean.revoke
    1.57 +                else delay_commit_clean.invoke
    1.58 +              }
    1.59              }
    1.60          }
    1.61        }
    1.62 @@ -363,6 +380,14 @@
    1.63      required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
    1.64      theories: Map[Document.Node.Name, Theory] = Map.empty)
    1.65    {
    1.66 +    lazy val theory_graph: Graph[Document.Node.Name, Unit] =
    1.67 +    {
    1.68 +      val entries =
    1.69 +        for ((name, theory) <- theories.toList)
    1.70 +        yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
    1.71 +      Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
    1.72 +    }
    1.73 +
    1.74      def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
    1.75  
    1.76      def insert_required(id: UUID, names: List[Document.Node.Name]): State =
    1.77 @@ -386,12 +411,52 @@
    1.78        copy(theories = theories -- remove)
    1.79      }
    1.80  
    1.81 -    lazy val theory_graph: Graph[Document.Node.Name, Unit] =
    1.82 +    def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name]): State =
    1.83 +    {
    1.84 +      val st1 = remove_required(id, dep_theories)
    1.85 +      val theory_edits =
    1.86 +        for {
    1.87 +          node_name <- dep_theories
    1.88 +          theory <- st1.theories.get(node_name)
    1.89 +        }
    1.90 +        yield {
    1.91 +          val theory1 = theory.required(st1.is_required(node_name))
    1.92 +          val edits = theory1.node_edits(Some(theory))
    1.93 +          (edits, (node_name, theory1))
    1.94 +        }
    1.95 +      session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
    1.96 +      st1.update_theories(theory_edits.map(_._2))
    1.97 +    }
    1.98 +
    1.99 +    def purge_theories(session: Session, nodes: List[Document.Node.Name])
   1.100 +      : ((List[Document.Node.Name], List[Document.Node.Name]), State) =
   1.101      {
   1.102 -      val entries =
   1.103 -        for ((name, theory) <- theories.toList)
   1.104 -        yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
   1.105 -      Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
   1.106 +      val all_nodes = theory_graph.topological_order
   1.107 +      val purge = nodes.filterNot(is_required(_)).toSet
   1.108 +
   1.109 +      val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet
   1.110 +      val (retained, purged) = all_nodes.partition(retain)
   1.111 +
   1.112 +      val purge_edits = purged.flatMap(name => theories(name).purge_edits)
   1.113 +      session.update(Document.Blobs.empty, purge_edits)
   1.114 +
   1.115 +      ((purged, retained), remove_theories(purged))
   1.116 +    }
   1.117 +
   1.118 +    def frontier_theories(clean: Set[Document.Node.Name]): Set[Document.Node.Name] =
   1.119 +    {
   1.120 +      @tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name])
   1.121 +        : Set[Document.Node.Name] =
   1.122 +      {
   1.123 +        val add = base.filter(b => theory_graph.imm_succs(b).forall(front))
   1.124 +        if (add.isEmpty) front
   1.125 +        else {
   1.126 +          val pre_add = add.map(theory_graph.imm_preds)
   1.127 +          val base1 = (pre_add.head /: pre_add.tail)(_ ++ _).toList.filter(clean)
   1.128 +          frontier(base1, front ++ add)
   1.129 +        }
   1.130 +      }
   1.131 +      frontier(theory_graph.maximals.filter(clean), Set.empty)
   1.132      }
   1.133    }
   1.134  }
   1.135 @@ -438,45 +503,29 @@
   1.136        })
   1.137    }
   1.138  
   1.139 -  def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
   1.140 +  def unload_theories(
   1.141 +    session: Thy_Resources.Session, id: UUID, dep_theories: List[Document.Node.Name])
   1.142 +  {
   1.143 +    state.change(_.unload_theories(session, id, dep_theories))
   1.144 +  }
   1.145 +
   1.146 +  def clean_theories(session: Thy_Resources.Session, id: UUID, clean: Set[Document.Node.Name])
   1.147    {
   1.148      state.change(st =>
   1.149        {
   1.150 -        val st1 = st.remove_required(id, dep_theories)
   1.151 -        val theory_edits =
   1.152 -          for {
   1.153 -            node_name <- dep_theories
   1.154 -            theory <- st1.theories.get(node_name)
   1.155 -          }
   1.156 -          yield {
   1.157 -            val theory1 = theory.required(st1.is_required(node_name))
   1.158 -            val edits = theory1.node_edits(Some(theory))
   1.159 -            (edits, (node_name, theory1))
   1.160 -          }
   1.161 -        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
   1.162 -        st1.update_theories(theory_edits.map(_._2))
   1.163 +        val frontier = st.frontier_theories(clean).toList
   1.164 +        if (frontier.isEmpty) st
   1.165 +        else {
   1.166 +          val st1 = st.unload_theories(session, id, frontier)
   1.167 +          val (_, st2) = st1.purge_theories(session, frontier)
   1.168 +          st2
   1.169 +        }
   1.170        })
   1.171    }
   1.172  
   1.173 -  def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
   1.174 +  def purge_theories(session: Thy_Resources.Session, nodes: Option[List[Document.Node.Name]])
   1.175      : (List[Document.Node.Name], List[Document.Node.Name]) =
   1.176    {
   1.177 -    state.change_result(st =>
   1.178 -      {
   1.179 -        val graph = st.theory_graph
   1.180 -        val all_nodes = graph.topological_order
   1.181 -
   1.182 -        val purge =
   1.183 -          (if (nodes.isEmpty) all_nodes else nodes.get.filter(graph.defined(_))).
   1.184 -            filterNot(st.is_required(_)).toSet
   1.185 -
   1.186 -        val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet
   1.187 -        val (retained, purged) = all_nodes.partition(retain)
   1.188 -
   1.189 -        val purge_edits = purged.flatMap(name => st.theories(name).purge_edits)
   1.190 -        session.update(Document.Blobs.empty, purge_edits)
   1.191 -
   1.192 -        ((purged, retained), st.remove_theories(purged))
   1.193 -      })
   1.194 +    state.change_result(st => st.purge_theories(session, nodes getOrElse st.theory_graph.keys))
   1.195    }
   1.196  }
     2.1 --- a/src/Pure/Tools/dump.scala	Fri Sep 07 20:35:18 2018 +0200
     2.2 +++ b/src/Pure/Tools/dump.scala	Fri Sep 07 23:47:26 2018 +0200
     2.3 @@ -76,6 +76,7 @@
     2.4    /* dump */
     2.5  
     2.6    val default_output_dir = Path.explode("dump")
     2.7 +  val default_commit_clean_delay = Time.seconds(-1.0)
     2.8  
     2.9    def make_options(options: Options, aspects: List[Aspect]): Options =
    2.10    {
    2.11 @@ -91,6 +92,7 @@
    2.12      select_dirs: List[Path] = Nil,
    2.13      output_dir: Path = default_output_dir,
    2.14      verbose: Boolean = false,
    2.15 +    commit_clean_delay: Time = default_commit_clean_delay,
    2.16      system_mode: Boolean = false,
    2.17      selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
    2.18    {
    2.19 @@ -158,7 +160,10 @@
    2.20          include_sessions = include_sessions, progress = progress, log = log)
    2.21  
    2.22      val theories_result =
    2.23 -      session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _))
    2.24 +      session.use_theories(use_theories,
    2.25 +        progress = progress,
    2.26 +        commit = Some(Consumer.apply _),
    2.27 +        commit_clean_delay = commit_clean_delay)
    2.28  
    2.29      val session_result = session.stop()
    2.30  
    2.31 @@ -176,6 +181,7 @@
    2.32      {
    2.33        var aspects: List[Aspect] = known_aspects
    2.34        var base_sessions: List[String] = Nil
    2.35 +      var commit_clean_delay = default_commit_clean_delay
    2.36        var select_dirs: List[Path] = Nil
    2.37        var output_dir = default_output_dir
    2.38        var requirements = false
    2.39 @@ -195,6 +201,8 @@
    2.40    Options are:
    2.41      -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
    2.42      -B NAME      include session NAME and all descendants
    2.43 +    -C SECONDS   delay for cleaning of already dumped theories (disabled for < 0, default: """ +
    2.44 +      default_commit_clean_delay.seconds.toInt + """)
    2.45      -D DIR       include session directory and select its sessions
    2.46      -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
    2.47      -R           operate on requirements of selected sessions
    2.48 @@ -213,6 +221,7 @@
    2.49  """ + Library.prefix_lines("    ", show_aspects) + "\n",
    2.50        "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
    2.51        "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
    2.52 +      "C:" -> (arg => commit_clean_delay = Time.seconds(Value.Double.parse(arg))),
    2.53        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    2.54        "O:" -> (arg => output_dir = Path.explode(arg)),
    2.55        "R" -> (_ => requirements = true),
    2.56 @@ -241,9 +250,11 @@
    2.57            dump(options, logic,
    2.58              aspects = aspects,
    2.59              progress = progress,
    2.60 +            log = new File_Logger(Path.explode("$ISABELLE_HOME_USER/dump.log")),
    2.61              dirs = dirs,
    2.62              select_dirs = select_dirs,
    2.63              output_dir = output_dir,
    2.64 +            commit_clean_delay = commit_clean_delay,
    2.65              verbose = verbose,
    2.66              selection = Sessions.Selection(
    2.67                requirements = requirements,