[isabelle-dev] AFP dependencies

[Makarius]

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

-------------- next part --------------
# 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]
-------------- next part --------------
A non-text attachment was scrubbed...
Name: afp.pdf
Type: application/pdf
Size: 16440 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20171010/0043c031/attachment-0001.pdf>