[isabelle-dev] Regression test for documents?
makarius at sketis.net
Tue Feb 28 16:53:29 CET 2012
On Sat, 18 Feb 2012, Florian Haftmann wrote:
> …seems not really operative. Otherwise accidents like
> http://isabelle.in.tum.de/reports/Isabelle/rev/2a0e1bcf713c could not
> have escaped attention for so long.
> Maybe we could setup a mira test for this, also including the makedist
isatest used to do that, but the main crontab on macbroy28 has the
following commented out:
#17 10 * * * $HOME/bin/isatest-doc
Gerwin might know the reason.
Incidently doc-src is failing again (e.g. in 0162a0d284ac):
*** Failed to finish proof
*** At command "done" (line 378 of "~~/doc-src/TutorialI/CTL/CTL.thy")
This might be related to some recent complete_lattice changes that I've
seen passing by.
More information about the isabelle-dev