Stream: Coq users

Topic: File-level Dependency Graph


view this post on Zulip Gregory Malecha (Jan 24 2022 at 21:26):

It looks like coqdep --dumpgraph was removed (probably a while ago) can anyone recommend a good replacement?

view this post on Zulip Guillaume Melquiond (Jan 24 2022 at 21:32):

If you are willing to write a bit of shell script, you can take inspiration from the following: https://coq.discourse.group/t/tool-for-drawing-coq-project-dependency-graph/653/16

view this post on Zulip Gregory Malecha (Jan 25 2022 at 02:12):

Thanks!

view this post on Zulip Michael Soegtrop (Jan 25 2022 at 08:39):

There is also the coq-dpdgraph package (maintained by @Yves Bertot ). It's description is "Coq plugin that extracts the dependencies between Coq objects, and produces files with dependency information. Includes tools to visualize dependency graphs and find unused definitions."

view this post on Zulip Karl Palmskog (Jan 25 2022 at 08:42):

dpdgraph focuses on the "semantic level", i.e., the elaborated term and module level dependencies. The old dumpgraph was purely at the file/filesystem level, using the shallow parsing done by coqdep. Probably dpdgraph could be extended to handle file level as well like dumpgraph did, since it's such a basic thing.

view this post on Zulip Pierre-Marie Pédrot (Jan 25 2022 at 08:45):

technically we have this data stored in the vo, so you could use a script based on the coqobjinfo POC https://github.com/coq/coq/pull/10333

view this post on Zulip Karl Palmskog (Jan 25 2022 at 08:45):

thanks for pointing that out, I will put this as TODO for the hackathon

view this post on Zulip Karl Palmskog (Jan 25 2022 at 08:49):

I think one could argue that the vo data is morally more correct than coqdep, even though we all rely on coqdep

view this post on Zulip Yves Bertot (Jan 25 2022 at 08:55):

In my recent playing with coq-dpdgraph, I was disappointed that it was not easy to group objects by file or module. In fact, I would like to improve the way data is collected so that each object should have its long name associated to it. Then it would be possible to interact with automatic documentation tools to have navigation from the dependency graph to the beautified files.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2022 at 12:21):

Yves Bertot said:

In my recent playing with coq-dpdgraph, I was disappointed that it was not easy to group objects by file or module. In fact, I would like to improve the way data is collected so that each object should have its long name associated to it. Then it would be possible to interact with automatic documentation tools to have navigation from the dependency graph to the beautified files.

That indeed makes a lot of sense, and in some other places @Yves Bertot we have the same need, so maybe it'd be interesting to actually share the data representation among tools?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2022 at 12:21):

I have a prototype that I call "coq-db" , so maybe once I have some time for coding on Feb we could do a session in the Hackathon?

view this post on Zulip Yves Bertot (Jan 25 2022 at 12:25):

Is coq-db visible somewhere?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2022 at 12:57):

It's private and broken currently, I need to get one day to push it sorry, but I won't have time until the ITP deadline pass

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2022 at 13:00):

But it is something very simple, indeed:

type 'a structured_doc =
  | Leaf of 'a list
  | Section of kind * 'a structured_doc

where kind can be a module, a proof, a section, that's not the actual type tho, let me grab it, I don't recall the exact definition now

Part one evolved from the coq-lsp prototype I did in 2017

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2022 at 13:02):

But if you agree @Yves Bertot we can schedule a session to discuss this in the Hackathon and I'll show the code I have and we can see how to share it

view this post on Zulip Bas Spitters (Jun 24 2022 at 07:55):

@Eske Nielsen recently added dpdgraph to concert, but this still depends on dumpgraph.
Has there been any progress on the issue in this thread?

view this post on Zulip Ali Caglayan (Jun 24 2022 at 09:46):

I think what we really want here is a dedicated tool to do this, rather than reintroducing a feature in coqdep.

view this post on Zulip Ali Caglayan (Jun 24 2022 at 09:47):

Since the internals of coqdep live in their own library, it shouldn't be too difficult to make a coqdumpgraph binary that constructs and outputs the graph.

view this post on Zulip Ali Caglayan (Jun 24 2022 at 09:47):

When it was removed from coqdep it was deemed "unused" but this clearly isn't the case.

view this post on Zulip Ali Caglayan (Jun 24 2022 at 09:47):

I do however agree that it had no business being in coqdep.

view this post on Zulip Ali Caglayan (Jun 24 2022 at 09:49):

I'll see if I can resurrect something today


Last updated: Feb 06 2023 at 13:03 UTC