[isabelle-dev] problem with Nominal in the AFP

Lars Hupel hupel at in.tum.de
Tue May 31 12:12:12 CEST 2016

> 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. In the absence of a more formalized connection between
Isabelle and AFP changesets, guesswork is all we can do, and it will
always fail in some situations.

(For now I'm not suggesting we should add a more formalized connection.)


More information about the isabelle-dev mailing list