Gregory Malecha (Jan 24 2022 at 21:26): 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?
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
Gregory Malecha (Jan 25 2022 at 02:12):Thanks!
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."
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.
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
Karl Palmskog (Jan 25 2022 at 08:45):thanks for pointing that out, I will put this as TODO for the hackathon
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
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.
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?
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?
Yves Bertot (Jan 25 2022 at 12:25):Is coq-db visible somewhere?
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
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
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
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?
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.
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.
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.
Ali Caglayan (Jun 24 2022 at 09:47):I do however agree that it had no business being in coqdep.
Ali Caglayan (Jun 24 2022 at 09:49):I'll see if I can resurrect something today
Last updated: Sep 15 2024 at 13:02 UTC