[isabelle-dev] Graphview

Makarius makarius at sketis.net
Thu Oct 11 16:53:44 CEST 2012

On Thu, 11 Oct 2012, Florian Haftmann wrote:

> * Misfit of node annotation size wrt. to the size of the full graphs –
> node annotations are not readable within a reasonable size coverage of
> the graph.
> * Does not scale well (e.g. class_deps from Main.thy).

I've made 1-2 rounds of refinements of the codebase already, and worked 
slowly towards these most imminent issues.  (Presently at 

The class_deps non-scalability probably stems from the omission of the 
transitive reduction (Hasse diagram).  This was probably done due to the 
anticipated locale graph visualization (which does not quite work), or it 
might be just an omission.  I was about to add the reduction 2 days ago, 
but got stuck elsewhere.  (Graph operations are always critical, and not 
to be rushed in any way.  We had famous drop-outs in that module already.)

> What are the plans for the next release?  Graph browsing is a tool too 
> vital that it can be set inoperative.  Is there any chancing for 
> improvements, or will there be a switch towards the classical browser 
> alternatively?

The release probably happens shortly after the start of the year -- I 
still don't see the details of the schedule.

As usual the general plan is to put things into shape, or disable things 
that are not in shape.  (I will make another round on Graphview pretty 


More information about the isabelle-dev mailing list