[Termtools] timeout for verification: 1 minute

[Johannes Waldmann]

Frederic Blanqui wrote:

> Then, I suggest to have a second round for the certified categories,
> either inside or outside the competition, with a 10 minutes timeout, but
> only on those problems that have not been checked within 1 minute.

Sounds interesting, but first let's see for how many proofs this
applies. I estimate that matchbox will lose about 1 percent of the
verifications by cutting down from 10 minutes to 1 minute (provided it
will find the certificates in time - which I cannot really predict)

> What do you think? Would it be possible to automate this?

We have to ask Simon to estimate the cost (workload) of implementing
this. Then we can decide. I assume there is, or will be,
some general mechanism for (re-)running categories
(or selected problems).


NB: I think a more urgent question (for the "verified" categories)
is this: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=45
Well perhaps not urgent but of fundamental importance (I think).


> I also suggest to provide statistics about the size of the generated Coq
> files (in Ko).

I'm sure this information is stored somewhere in the data base
(or it could be, by importing the file sizes),
the question is how to query for it.

That's the next major technical point:
we want a flexible query interface
(i.e., user-defined evaluation of the data collected during the runs)

I'll open a separate Mail thread for that.


Best regards, Johannes.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 257 bytes
Desc: OpenPGP digital signature
Url : http://lists.lri.fr/pipermail/termtools/attachments/20081104/e884b717/attachment.pgp