[isabelle-dev] AFP dependencies
makarius at sketis.net
Thu Oct 12 21:49:15 CEST 2017
On 10/10/17 20:50, Makarius wrote:
> 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,
> The resulting afp.pdf is included. Note that it ignores isolated nodes,
> otherwise the graph layout would be even larger.
Andreas Lochbihler and Lars Hupel have discovered oddities in the graph:
unnecessary session dependencies that probably stem from early versions
of "isabelle imports -I", which had particular problems with theory
files used in many sessions.
In Isabelle/c75769065548 I have refined the tool further to print
"actual session dependencies", based on the imported theories and
minimized according to the session imports relation.
I have used that in AFP/3235d24e075a to eliminate pointless session imports.
More information about the isabelle-dev