<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=ISO-8859-1">
  </head>
  <body bgcolor="#FFFFFF" text="#000000">
    Hi all,<br>
    <br>
    since "Containers" are in the AFP mira results in global crashes of
    the build tool
    (<a class="moz-txt-link-freetext" href="http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694">http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694</a>).
    By global I mean that no session is built at all due to an outdated
    (wrt Isabelle repository, e.g.
    <meta name="qrichtext" content="1">
    <meta http-equiv="Content-Type" content="text/html;
      charset=ISO-8859-1">
    <style type="text/css">
p, li { white-space: pre-wrap; }
</style>916271d52466) import of "src/HOL/Library/Efficient_Nat.thy" in
    the session "Containers-Benchmarks".<br>
    <br>
    For now I commented the "Containers-Benchmarks" session out (AFP/
    <meta name="qrichtext" content="1">
    <meta http-equiv="Content-Type" content="text/html;
      charset=ISO-8859-1">
    <style type="text/css">
p, li { white-space: pre-wrap</style>99c45df7f5af) - now the test will
    reveal further outdated constructs in "Containers" (mostly related
    to Florian's reform of the code generation for numerals).<br>
    <br>
    The question remains, whether it is possible for the build tool to
    proceed with other sessions if the imports of a single session are
    faulty. <br>
    <br>
    Dmitriy<br>
  </body>
</html>