Email Gateway (Aug 22 2022 at 16:36): Email Gateway (Aug 22 2022 at 16:36):From: Makarius <makarius@sketis.net>
On 10/01/18 07:12, Thomas.Sewell@data61.csiro.au wrote:
I have a query about what might be possible with timing data.
Isabelle proofs sometimes go into infinite loops, leading to session
builds that run forever. The isabelle build process has a per-session
timeout option, which can be specified in ROOT files.
BTW, a timeout that is hardwired in ROOT is sometimes not right for
different test hardware. In that case it may help to use something like
isabelle build -o timeout_scale=2 on the command line.
I don't know how
common it is to use this. Our test apparatus also has a crude mechanism
for killing a test after some length of time, and I guess that's pretty
common.
How is that different from the builtin timeout mechanism (which is in
Isabelle/Scala)?
My main question is, is there some way we could track slow commands
during session builds?In interactive mode, commands that are running for a while are
highlighted in the "Running" colour in jEdit (usually deep purple). My
understanding is that roughly the same PIDE infrastructure is in place
during session builds.
Session batch-builds still lack PIDE markup (and status) information. I
am working on that for many years, and maybe this week / month / year /
decade it will actually materialize. A proper PIDE markup db file for
session builds would have many benefits, e.g. for document preparation.
The elapsed time for the "purple" status of a command could be
definitely observed and recorded via PIDE, but there can be
irregularities: global GC time can be quite long and interfere with all
running commands. We shall see how it works out when it is there.
Would it be possible to log information about > slow commands (e.g.
those running more than one minute)? Could we set a
flag to send such information to an extra log file?
Yes, when PIDE markup becomes available in batch-mode builds.
Makarius
Email Gateway (Aug 22 2022 at 16:36):From: Thomas.Sewell@data61.csiro.au
Hello isabelle-users, and implementors.
I have a query about what might be possible with timing data.
Isabelle proofs sometimes go into infinite loops, leading to session
builds that run forever. The isabelle build process has a per-session
timeout option, which can be specified in ROOT files. I don't know how
common it is to use this. Our test apparatus also has a crude mechanism
for killing a test after some length of time, and I guess that's pretty
common.
A timeout result is our least desirable outcome. We learn very little.
If our apparatus kills the build, we don't get a log file. When the
timeout option fires, I haven't found any useful information in the log
file.
My main question is, is there some way we could track slow commands
during session builds?
In interactive mode, commands that are running for a while are
highlighted in the "Running" colour in jEdit (usually deep purple). My
understanding is that roughly the same PIDE infrastructure is in place
during session builds. Would it be possible to log information about
slow commands (e.g. those running more than one minute)? Could we set a
flag to send such information to an extra log file?
Reporting (roughly) which line the infinite loop is in would be a
substantial improvement. Even reporting which theory the loop was in
would help.
Would this be useful to other users?
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 16:37):From: Thomas.Sewell@data61.csiro.au
Thanks Makarius.
Indeed, a hardwired timeout is an imprecise approach. We've used very
generous
timeouts rather than fiddling with per-machine expectations. The point
is to ensure
that test runs finish eventually, since otherwise we'd have to keep
fiddling with the
test apparatus by hand.
As you say, an external timeout is the same as an Isabelle timeout, for
Isabelle builds.
Our test runs test a mix of Isabelle builds and other things, so we have
a similar
mechanism in the test-control script.
I was confused a little about the batch builds. The overall framework
(Isabelle/Scala
and protocol) is the same during builds, but the kinds of protocol
messages exchanged
are different.
In the meanwhile, I've got around to implementing a version on the ML
side. It's just a
simple task that runs every few seconds (via Event_Timer.request) and
blogs (to a file)
a report about what's running and which tasks have been running for a
while. It's not
very accurate but the log can still be interesting when a session times
out. I was going
to test it a bit more at this end before asking if anyone else wanted a
copy.
This is just a make-do solution. I'm sure you'd rather move toward a
more canonical
implementation with session builds running more of the document protocol
and a Scala
module producing similar output. I don't understand the Scala layer well
enough to
try that though.
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 16:39):From: Makarius <makarius@sketis.net>
The PIDE protocol is still not used at all in batch-builds. This would
require some reworking in various respects, e.g. full parallel proof
checking in PIDE.
Getting that all into proper shape has a high priority for me, but it
means it could happen next week / month / year / decade.
The current intermediate approach has some rudiments of
protocol_message, which are not PIDE messages. See
http://isabelle.in.tum.de/repos/isabelle/annotate/Isabelle2017/src/Pure/Tools/build.ML#l75
There is actually some Markup.command_timing information that ends up in
the build db file. Here is an example to access that in Isabelle/Scala
(Isabelle2017):
$ isabelle scala
import isabelle._
val store = Sessions.store(system_mode = false)
val name = "HOL"
val database = store.find_database(name).get
val db = SQLite.open_database(database)
val command_timings = store.read_command_timings(db, name)
The purpose of that is to fine-tune parallel checking of proofs in batch
mode. It does not handle the case of non-terminating commands, nor does
it take GC time into account.
Makarius
Last updated: Apr 19 2024 at 01:05 UTC