[Agda] dependency graph

[Martin Escardo]

On 07/01/2019 18:02, nad at cse.gu.se wrote:
> On 07/01/2019 17.48, Martin Escardo wrote:
>> Is there a way to get a dependency graph of all (global) defined names
>> in a set of Agda files?
> 
> Yes, for instance by editing the Agda source code and adding such a
> feature. The logic for the current --dependency-graph option is
> implemented mainly in Agda.Interaction.Highlighting.Dot. 

Interesting. I indeed tried to inspect the source code to try to find 
this, but I didn't occur to me to look at Interaction.

Is there a resource that explains the architecture of the Agda 
implementation? I tried to find this, too.

> I assume that
> it would be fairly easy to construct a similar feature that worked on
> the level of top-level definitions instead of top-level modules.

Great.

> Do you want to look at the dependency graph, or do you want to query it?

I want to query it, but I know how to do this if I have the graph (e.g. 
in dot format), although it would be great if the Agda framework had 
some tools, particularly in the interactive mode, to ask some questions 
about this graph.

At the moment, I would benefit from this for three mathematical papers I 
am writing based on a single Agda code base. Manual inspection is 
tedious and prone incompleteness.

Martin

> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe