[isabelledev] AFP dependencies
Makarius
makarius at sketis.net
Tue Oct 10 20:50:50 CEST 2017
Motivated by the question by Lars Hupel
https://lists.cam.ac.uk/pipermail/clisabelleusers/2017October/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 JNFAFPLib.
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 "JNFHOLLib" (AFP) = "HOLAlgebra" +
 description {* Theories that are not part of HOL but are used by this entry *}
 options [document = false, timeout = 600]
 sessions
 "HOLCardinals"
 "Containers"
 theories
 "HOLLibrary.AList"
 "HOLLibrary.Cardinality"
 "HOLLibrary.Char_ord"
 "HOLLibrary.Code_Char"
 "HOLLibrary.Code_Binary_Nat"
 "HOLLibrary.Code_Target_Numeral"
 "HOLLibrary.DAList"
 "HOLLibrary.DAList_Multiset"
 "HOLLibrary.Infinite_Set"
 "HOLLibrary.Lattice_Syntax"
 "HOLLibrary.List_lexord"
 "HOLLibrary.Mapping"
 "HOLLibrary.Monad_Syntax"
 "HOLLibrary.More_List"
 "HOLLibrary.Multiset"
 "HOLLibrary.Permutation"
 "HOLLibrary.Permutations"
 "HOLLibrary.IArray"
 "HOLLibrary.Phantom_Type"
 "HOLLibrary.Ramsey"
 "HOLLibrary.RBT_Impl"
 "HOLLibrary.Simps_Case_Conv"
 "HOLLibrary.While_Combinator"
 "HOLComputational_Algebra.Fundamental_Theorem_Algebra"
 "HOLComputational_Algebra.Fraction_Field"
 "HOLComputational_Algebra.Polynomial"
 "HOLComputational_Algebra.Primes"
 "HOLCardinals.Order_Union"
 "HOLCardinals.Wellorder_Extension"

session "JNFAFPLib" (AFP) = "JNFHOLLib" +
 description {* Theories from the Archive of Formal Proofs that are used by this entry *}
 options [document = false, timeout = 600]
 sessions
 "AbstractRewriting"
 Gauss_Jordan Matrix
 Polynomial_Interpolation
 Show
 VectorSpace
 theories
 Containers.Set_Impl
 Gauss_Jordan.IArray_Haskell
 Matrix.Utility
 Matrix.Ordered_Semiring
 "AbstractRewriting.SN_Order_Carrier"
 "AbstractRewriting.Relative_Rewriting"
 Show.Show_Instances
 VectorSpace.VectorSpace
 Polynomial_Interpolation.Missing_Polynomial

session "Jordan_Normal_Form" (AFP) = "JNFAFPLib" +
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 "JNFHOLLib" (AFP) = "HOLAlgebra" +
+ description {* Theories that are not part of HOL but are used by this entry *}
+ options [document = false, timeout = 600]
+ sessions
+ "HOLCardinals"
+ "Containers"
+ theories
+ "HOLLibrary.AList"
+ "HOLLibrary.Cardinality"
+ "HOLLibrary.Char_ord"
+ "HOLLibrary.Code_Char"
+ "HOLLibrary.Code_Binary_Nat"
+ "HOLLibrary.Code_Target_Numeral"
+ "HOLLibrary.DAList"
+ "HOLLibrary.DAList_Multiset"
+ "HOLLibrary.Infinite_Set"
+ "HOLLibrary.Lattice_Syntax"
+ "HOLLibrary.List_lexord"
+ "HOLLibrary.Mapping"
+ "HOLLibrary.Monad_Syntax"
+ "HOLLibrary.More_List"
+ "HOLLibrary.Multiset"
+ "HOLLibrary.Permutation"
+ "HOLLibrary.Permutations"
+ "HOLLibrary.IArray"
+ "HOLLibrary.Phantom_Type"
+ "HOLLibrary.Ramsey"
+ "HOLLibrary.RBT_Impl"
+ "HOLLibrary.Simps_Case_Conv"
+ "HOLLibrary.While_Combinator"
+ "HOLComputational_Algebra.Fundamental_Theorem_Algebra"
+ "HOLComputational_Algebra.Fraction_Field"
+ "HOLComputational_Algebra.Polynomial"
+ "HOLComputational_Algebra.Primes"
+ "HOLCardinals.Order_Union"
+ "HOLCardinals.Wellorder_Extension"
+
+session "JNFAFPLib" (AFP) = "JNFHOLLib" +
+ description {* Theories from the Archive of Formal Proofs that are used by this entry *}
+ options [document = false, timeout = 600]
+ sessions
+ "AbstractRewriting"
+ Gauss_Jordan Matrix
+ Polynomial_Interpolation
+ Show
+ VectorSpace
+ theories
+ Containers.Set_Impl
+ Gauss_Jordan.IArray_Haskell
+ Matrix.Utility
+ Matrix.Ordered_Semiring
+ "AbstractRewriting.SN_Order_Carrier"
+ "AbstractRewriting.Relative_Rewriting"
+ Show.Show_Instances
+ VectorSpace.VectorSpace
+ Polynomial_Interpolation.Missing_Polynomial
+
session Pre_Polynomial_Factorization (AFP) = "JNFAFPLib" +
description {* Theories from other AFPentries and Extended Theories for Matrices *}
options [timeout = 600, document = false]
 next part 
A nontext attachment was scrubbed...
Name: afp.pdf
Type: application/pdf
Size: 16440 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tumuenchen.de/pipermail/isabelledev/attachments/20171010/0043c031/attachment0001.pdf>
More information about the isabelledev
mailing list