Re: [isabelle] Timing information from isabelle build

Thanks Makarius.

Indeed, a hardwired timeout is an imprecise approach. We've used very 
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 
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 

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.


On 01/02/18 08:35, Makarius wrote:
> On 10/01/18 07:12, Thomas.Sewell at 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.