> Apart from that, there is also a custom to push AFP changes a bit later
> than the ones on the Isabelle repository. Maybe Jenkins can take this
> somehow into account and not start tests on AFP immediately.
I've thought about this. The problem is that the notion of "a bit later"
is ill-defined.
On 31/05/16 11:18, Lars Hupel wrote:
>> Incompleteness FAILED
>
> This problem has already been addressed. Makarius changed some Isabelle
> signatures in Isabelle/4d04e14d7ab8, and adapted AFP in d46ea7497f.
>
> Unfortunately it's currently impossible to perform atomic changes to
> both repositor
> Incompleteness FAILED
This problem has already been addressed. Makarius changed some Isabelle
signatures in Isabelle/4d04e14d7ab8, and adapted AFP in d46ea7497f.
Unfortunately it's currently impossible to perform atomic changes to
both repositories.
Cheers
Lars
Incompleteness FAILED
(see also
/media/data/jenkins/workspace/isabelle-repo-afp/heaps/polyml-5.6_x86_64-linux/log/Incompleteness)
*** Specification.definition NONE [] ((permute_def_name, []), permute_eqn)
*** : Attrib.binding * term ->
*** local_theory -> (term * (string * th