[isabelle-dev] AFP dependencies

[Makarius]

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
assumption.


	Makarius