Motivated by the question by Lars Hupel https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-October/msg00010.html "Calling Isabelle tools without exiting" (and implicitly about "isabelle afp_dependencies"), I have now produced a module in Isabelle/Scala to support administration of AFP.
Here is an example for Isabelle/c925393ae6b9 and AFP/cd292cbedcb9 (after applying the included changeset): import isabelle._ val options = Options.init val afp = AFP.init(options) isabelle.graphview.Graph_File.write(options + "graphview_font_size=24", Path.explode("afp.pdf").file, afp.entries_graph_display) The resulting afp.pdf is included. Note that it ignores isolated nodes, otherwise the graph layout would be even larger. 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. Makarius
# HG changeset patch # User wenzelm # Date 1507659422 -7200 # Tue Oct 10 20:17:02 2017 +0200 # Node ID e65225a319b03ff627d67f7d68459937409f03d2 # Parent cd292cbedcb9cfe65f9aee2f44fb639bf13b3fa2 avoid cyclic dependency of Jordan_Normal_Form vs. Polynomial_Factorization; diff -r cd292cbedcb9 -r e65225a319b0 thys/Jordan_Normal_Form/ROOT --- a/thys/Jordan_Normal_Form/ROOT Tue Oct 10 17:18:28 2017 +0100 +++ b/thys/Jordan_Normal_Form/ROOT Tue Oct 10 20:17:02 2017 +0200 @@ -1,62 +1,5 @@ chapter AFP -session "JNF-HOL-Lib" (AFP) = "HOL-Algebra" + - description {* Theories that are not part of HOL but are used by this entry *} - options [document = false, timeout = 600] - sessions - "HOL-Cardinals" - "Containers" - theories - "HOL-Library.AList" - "HOL-Library.Cardinality" - "HOL-Library.Char_ord" - "HOL-Library.Code_Char" - "HOL-Library.Code_Binary_Nat" - "HOL-Library.Code_Target_Numeral" - "HOL-Library.DAList" - "HOL-Library.DAList_Multiset" - "HOL-Library.Infinite_Set" - "HOL-Library.Lattice_Syntax" - "HOL-Library.List_lexord" - "HOL-Library.Mapping" - "HOL-Library.Monad_Syntax" - "HOL-Library.More_List" - "HOL-Library.Multiset" - "HOL-Library.Permutation" - "HOL-Library.Permutations" - "HOL-Library.IArray" - "HOL-Library.Phantom_Type" - "HOL-Library.Ramsey" - "HOL-Library.RBT_Impl" - "HOL-Library.Simps_Case_Conv" - "HOL-Library.While_Combinator" - "HOL-Computational_Algebra.Fundamental_Theorem_Algebra" - "HOL-Computational_Algebra.Fraction_Field" - "HOL-Computational_Algebra.Polynomial" - "HOL-Computational_Algebra.Primes" - "HOL-Cardinals.Order_Union" - "HOL-Cardinals.Wellorder_Extension" - -session "JNF-AFP-Lib" (AFP) = "JNF-HOL-Lib" + - description {* Theories from the Archive of Formal Proofs that are used by this entry *} - options [document = false, timeout = 600] - sessions - "Abstract-Rewriting" - Gauss_Jordan Matrix - Polynomial_Interpolation - Show - VectorSpace - theories - Containers.Set_Impl - Gauss_Jordan.IArray_Haskell - Matrix.Utility - Matrix.Ordered_Semiring - "Abstract-Rewriting.SN_Order_Carrier" - "Abstract-Rewriting.Relative_Rewriting" - Show.Show_Instances - VectorSpace.VectorSpace - Polynomial_Interpolation.Missing_Polynomial - session "Jordan_Normal_Form" (AFP) = "JNF-AFP-Lib" + options [timeout = 1200] sessions diff -r cd292cbedcb9 -r e65225a319b0 thys/Polynomial_Factorization/ROOT --- a/thys/Polynomial_Factorization/ROOT Tue Oct 10 17:18:28 2017 +0100 +++ b/thys/Polynomial_Factorization/ROOT Tue Oct 10 20:17:02 2017 +0200 @@ -1,5 +1,62 @@ chapter AFP +session "JNF-HOL-Lib" (AFP) = "HOL-Algebra" + + description {* Theories that are not part of HOL but are used by this entry *} + options [document = false, timeout = 600] + sessions + "HOL-Cardinals" + "Containers" + theories + "HOL-Library.AList" + "HOL-Library.Cardinality" + "HOL-Library.Char_ord" + "HOL-Library.Code_Char" + "HOL-Library.Code_Binary_Nat" + "HOL-Library.Code_Target_Numeral" + "HOL-Library.DAList" + "HOL-Library.DAList_Multiset" + "HOL-Library.Infinite_Set" + "HOL-Library.Lattice_Syntax" + "HOL-Library.List_lexord" + "HOL-Library.Mapping" + "HOL-Library.Monad_Syntax" + "HOL-Library.More_List" + "HOL-Library.Multiset" + "HOL-Library.Permutation" + "HOL-Library.Permutations" + "HOL-Library.IArray" + "HOL-Library.Phantom_Type" + "HOL-Library.Ramsey" + "HOL-Library.RBT_Impl" + "HOL-Library.Simps_Case_Conv" + "HOL-Library.While_Combinator" + "HOL-Computational_Algebra.Fundamental_Theorem_Algebra" + "HOL-Computational_Algebra.Fraction_Field" + "HOL-Computational_Algebra.Polynomial" + "HOL-Computational_Algebra.Primes" + "HOL-Cardinals.Order_Union" + "HOL-Cardinals.Wellorder_Extension" + +session "JNF-AFP-Lib" (AFP) = "JNF-HOL-Lib" + + description {* Theories from the Archive of Formal Proofs that are used by this entry *} + options [document = false, timeout = 600] + sessions + "Abstract-Rewriting" + Gauss_Jordan Matrix + Polynomial_Interpolation + Show + VectorSpace + theories + Containers.Set_Impl + Gauss_Jordan.IArray_Haskell + Matrix.Utility + Matrix.Ordered_Semiring + "Abstract-Rewriting.SN_Order_Carrier" + "Abstract-Rewriting.Relative_Rewriting" + Show.Show_Instances + VectorSpace.VectorSpace + Polynomial_Interpolation.Missing_Polynomial + session Pre_Polynomial_Factorization (AFP) = "JNF-AFP-Lib" + description {* Theories from other AFP-entries and Extended Theories for Matrices *} options [timeout = 600, document = false]
afp.pdf
Description: Adobe PDF document
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev