[isabelle-dev] AFP dependencies

[Makarius]

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,
> afp.entries_graph_display)
> 
> 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.


	Makarius