[isabelle-dev] AFP dependencies

Makarius makarius at sketis.net
Thu Oct 12 21:41:25 CEST 2017

On 10/10/17 20:50, Makarius wrote:
> The above change to AFP is required to avoid cyclic dependency of
> Jordan_Normal_Form vs. Polynomial_Factorization, due to session JNF-AFP-Lib.
> This problem can be exhibited as follows (without the change):
>   Exn.capture { afp.dependency_graph(acyclic = true) }
> Maybe such a check should be part of the normal AFP routine. We can then
> always assume that afp.entries_graph is acyclic. This would simplify the
> rather complex situation of auxiliary sessions in AFP.

See now Isabelle/d20a668b394e and AFP/592936584e2e, i.e.
AFP.entries_graph always needs to be acyclic -- a quite reasonable


More information about the isabelle-dev mailing list