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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
