[isabelle-dev] Distro broken

Makarius makarius at sketis.net
Wed Oct 19 11:11:21 CEST 2016


> Am Dienstag, den 18.10.2016, 20:40 +0200 schrieb Florian Haftmann:
>>> *** No such file:
>>> "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Ess
>>> ential_Supremum.thy"

On 19/10/16 00:19, Johannes Hölzl wrote:
> My bad, should be fixed now.

That is the traditional situation that someone pulling from the
repository sees a total existence failure and reports it manually on the
mailing list.

So far, the main argument for the massive waste of CPU resources by
Jenkins was to make that report automatic.

What happened that it did not work here?


BTW, isabelle could easily detect the situation of missing files in the
repository and emit a warning. I will add that in the next round of
refinement (after the release).


	Makarius




More information about the isabelle-dev mailing list