Christian Doczkal (Dec 14 2020 at 11:31): Christian Doczkal (Dec 14 2020 at 11:31):I just noticed that coqdep on coq-8.12 appears to no longer accept the -dumpgraph option. All I could find in the changelog is:
Also, several deprecated options have been removed: -w, -D, -mldep, -prefix, -slash, and -dumpbox.
Which does not mention the removal of -dumpbox, but the mentioned PR (#11523) seems to indeed remove the aforementioned options. I don't know where they have been marked as "broken" but they worked well enough for us to generate our library graph: https://perso.ens-lyon.fr/damien.pous/covece/graphs/. So how are we supposed to generate our library graphs in the future? For now I still have a copy of 8.11 around ...
Enrico Tassi (Dec 14 2020 at 12:23):Maybe you can use this thing https://github.com/math-comp/math-comp/blob/master/etc/utils/dependtodot.ml
Enrico Tassi (Dec 14 2020 at 12:24):https://github.com/math-comp/math-comp/blob/master/etc/utils/builddoc_lib.sh#L75-L83
Karl Palmskog (Dec 14 2020 at 12:28):the removal was discussed here: https://coq.discourse.group/t/tool-for-drawing-coq-project-dependency-graph/653/4
the problem is that now everyone and their brother has to figure out which script to use out of the many options...
Christian Doczkal (Dec 14 2020 at 12:42):Great, there used to be a solution that worked "out of the box" and now I am supposed to compare 5-10 home-grown solutions. I'm inclined to keep 8.11 around until a (clear) winner has emerged or this IMHO unfortunate decision gets reverted. :angry:
Christian Doczkal (Dec 14 2020 at 12:48):After the coq-native story from last week this is really souring my mood.
Théo Zimmermann (Dec 14 2020 at 13:41):Christian Doczkal said:
All I could find in the changelog is:
Also, several deprecated options have been removed: -w, -D, -mldep, -prefix, -slash, and -dumpbox.
Which does not mention the removal of
-dumpbox
Hum :eyes:
Christian Doczkal (Dec 14 2020 at 13:46):See, I was so annoyed that I confused -dumpgraph[box] and -dumpbox, which to the best of my knowledge never existed.
Théo Zimmermann (Dec 14 2020 at 13:47):It's impressive that this broken changelog has not been fixed despite my comment about that in the aforementioned Discourse thread.
Christian Doczkal (Dec 14 2020 at 13:53):Well, in that thread also quite a few people reported that they were in fact using this feature, and you suggested putting the feature back, but this seems to also not have happened.
Théo Zimmermann (Dec 14 2020 at 13:58):Yes. The conclusion is that it is hard to make other people do work by just asking. The most efficient way to have the removal reverted would probably be to open a PR (if it's easy to revert just the removal of this option and not all the rest). The case for removal was reduce maintenance but the case for reintroducing is just as clear (used by many people).
Christian Doczkal (Dec 14 2020 at 14:04):Well, maybe someone who already has a working OCaml development setup might be willing to do it. :eyes:
Théo Zimmermann (Dec 14 2020 at 14:17):Don't count on me for that. Then, the next best option is to open an issue so that other devs pick it up.
Emilio Jesús Gallego Arias (Dec 14 2020 at 14:51):Ummmmm.... I guess the main rationale indeed was that we already had too many tools and the one in coqdep was basically not being taken care by anyone. I guess it'd be fine to add such functionality to coq, but IMHO it should be its own tool, and hopefully try to unify / encompass all current approaches.
Karl Palmskog (Dec 14 2020 at 14:55):I agree a "unified" standalone tool is ideal, but until this tool appears, isn't it better to reinstate the -dumpgraph so everybody doesn't have to try out all these different alternatives?
Christian Doczkal (Dec 14 2020 at 14:57):@Emilio Jesús Gallego Arias , I don't see the rationale for a different tool. coqdep is the tool that computes the dependencies between the different files of coq development. So -dumpgraph is basically just a (slightly) different output format for the information computed by coqdep...
Emilio Jesús Gallego Arias (Dec 14 2020 at 15:33):In this sense I think that the "unix" philosophy of having well-delimited tools better suits us, so even if we re-instantiate the old "tool" [which was just a bunch of lines of codes], it should come as its own standalone tool, and have a maintainer.
Emilio Jesús Gallego Arias (Dec 14 2020 at 15:35):Clearly there is a rationale as seen by the quite abundant proliferation of different approaches, but indeed, by moving the "output a graph" part to its own tool, the maintainer(s) can proceed as they desire in terms of features etc...
Théo Zimmermann (Dec 14 2020 at 15:51):The need for a maintainer is not clear if the tool has worked without being broken for a long time and if there is no feature to add.
Enrico Tassi (Dec 14 2020 at 15:52):The PR says:
I wonder how "unused" was evaluated...
Pierre-Marie Pédrot (Dec 14 2020 at 15:54):You can ask the same question about "broken".
Pierre-Marie Pédrot (Dec 14 2020 at 15:57):I mean, we all know that coqdep is a syntactic approximation, but the graph output is no more broken than the algorithm we rely on to compute Require dependencies for the build.
Pierre-Marie Pédrot (Dec 14 2020 at 15:57):So, in that view, we should probably remove Require as well.
Yannick Forster (Mar 17 2021 at 16:31):Can somebody point to a script which does the job? I tried MakefileViz, makefile2graph, and makefile2dot. MakefileViz does not work for Coq Makefiles, makefile2graph wants to recompile everything (which I want to avoid) and makefile2dot does not compile for me.
Christian Doczkal (Mar 17 2021 at 17:03):@Yannick Forster , I found it easiest to just install coq-8.11 in some OPAM switch and run the coqdep from there ...
Christian Doczkal (Mar 17 2021 at 17:06):The good news is, that reintroducing the feature has been milestoned for 8.14_rc1 : https://github.com/coq/coq/issues/13636 The bad news is, that this has not (yet) led to someone actually creating a PR.
Pierre-Marie Pédrot (Mar 18 2021 at 15:52):I am having a look at this, and it is not as easy as I thought
Yannick Forster (Mar 18 2021 at 16:06):Thanks @Christian Doczkal, that's clever! I in fact already have a coq-8.11 switch
Yannick Forster (Mar 18 2021 at 16:06):And thanks Pierre-Marie, I really miss this feature!
Pierre-Marie Pédrot (Mar 18 2021 at 16:08):Might be actually easier to implement it from scratch or as a separate tool.
Pierre-Marie Pédrot (Mar 18 2021 at 16:08):You want to be able to get the data from the raw v files, right?
Pierre-Marie Pédrot (Mar 18 2021 at 16:09):A correct tool for vo files wouldn't fit the bill, if I read correctly the above.
Christian Doczkal (Mar 18 2021 at 16:10):Well, I want the data that coqdep generates from the .v files in order to organize the build in the dot format. The data must be there...
Pierre-Marie Pédrot (Mar 18 2021 at 16:11):Yes, but not as a proper graph.
Pierre-Marie Pédrot (Mar 18 2021 at 16:11):I'll see what I can do.
Christian Doczkal (Mar 18 2021 at 16:14):Admittedly, I haven't looked at the code yet, but the output of coqdep for make is fairly close, it just mixes .v and .vo and may contain (unwanted) transitive "edges".
Guillaume Melquiond (Mar 18 2021 at 16:19):Transitive edges are not an issue. Since the goal is to produce a file for the Graphviz tools, we might just as well assume that tred is installed. coqdep does not even have to remove the transitive edges.
Yannick Forster (Mar 18 2021 at 16:25):For me it would indeed be better if I can just print the dependency graph of a project without compiling it. If it's a lot easier to have a solution based on .vo files that would still be better than nothing though.
Emilio Jesús Gallego Arias (Mar 18 2021 at 18:09):Not sure re-adding the old hack is a good idea, first, because we have too many tools already doing the same, second, graphviz does directly support make files IIANW so you could do that easily IMHO
Emilio Jesús Gallego Arias (Mar 18 2021 at 18:09):What does math-comp use?
Emilio Jesús Gallego Arias (Mar 18 2021 at 18:10):I we re-add this tool then the others should be deprecated
Enrico Tassi (Mar 18 2021 at 18:19):Emilio Jesús Gallego Arias said:
What does math-comp use?
Yet another "home grown" hack https://github.com/math-comp/math-comp/blob/master/etc/utils/dependtodot.ml
Enrico Tassi (Mar 18 2021 at 18:21): Emilio Jesús Gallego Arias (Mar 18 2021 at 18:23):It'd be good to consolidate them, we already maintain coq-dpdgraph which seems to be an opam install away.
Enrico Tassi (Mar 18 2021 at 18:23):Does it do a .dot?
Emilio Jesús Gallego Arias (Mar 18 2021 at 18:29):coq-dpdgraph , yes it does
Enrico Tassi (Mar 18 2021 at 18:40):Reading the doc it seems it generates a graph where the nodes are you theorems, not your files.
Enrico Tassi (Mar 18 2021 at 18:50):FTR, I did point you to the wrong scripts for math-comp. The current one is yet another home grown script https://github.com/math-comp/math-comp/blob/master/etc/buildlibgraph which reads the output of coqdep and build a .js file for cytoscape, which is rendered like this: https://math-comp.github.io/htmldoc_1_12_0/libgraph.html
Christian Doczkal (Mar 19 2021 at 08:18):Enrico Tassi said:
Reading the doc it seems it generates a graph where the nodes are you theorems, not your files.
I can confirm this. So I think this tool serves a different purpose. Also, IIRC, it uses the .vo files.
Yannick Forster (Mar 19 2021 at 08:22):Yes, coq-dpdgraph is not ideal, because one has to compile everything first. One use case for the file dependency graph I have is to figure out where a dependency is coming from when debugging universe issues. And the whole point when having universe issues is that I cannot compile the development.
Yannick Forster (Mar 19 2021 at 08:40):I played around a little with the buildlibgraph script. I can adapt it to print the nodes of a graph, but I can't figure out how to get the edges in the resulting dot file as well. But I'm happy to test more proposals how to re-obtain a graph-printing feature
Yannick Forster (Mar 19 2021 at 08:42):@Emilio Jesús Gallego Arias I tried graphviz-based tool to extract graphs from Makefiles, but with no success. Do you have a pointer to the feature?
Enrico Tassi (Mar 19 2021 at 09:09):Yannick Forster said:
I played around a little with the
buildlibgraphscript. I can adapt it to print the nodes of a graph, but I can't figure out how to get the edges in the resultingdotfile as well. But I'm happy to test more proposals how to re-obtain a graph-printing feature
The lua script? the doc at the bottom is outdated, since we don't build the dot anymore the main dispatching is gone. if you replace at the very bottom cytoscape() with dot() it works here:
coqdep -R . mathcomp */*.v | grep -v vio: > depend
cat depend | /tmp/buildlibgraph > depend.dot
xdot depend.dot
As you can see a plain graph is too complex for mathcomp, hence the cytoscape thinghy where you can actually play with the nodes. A few years back it was the only free js layout library I could find, maybe today there is better stuff out there.
Yannick Forster (Mar 19 2021 at 09:28):Ha, thanks. I figured out that cytyoscape() has to be replaced by dot(), and there is a hard-coded mathcompstring somewhere in the script, not sure that's actually problematic. I actually had a typo in one of the -Q directives for coqdep, that's why I got no edges. So: Using buildgraphlib works for me
Yannick Forster (Mar 19 2021 at 09:31):Okay, but the dot output for coq-library-undecidability is pretty unreadable. How do you get the html file from the js file for cytoscape?
Enrico Tassi (Mar 19 2021 at 09:37):put the .js in this directory and it should work https://github.com/math-comp/math-comp.github.io/tree/master/htmldoc_template
Yannick Forster (Mar 19 2021 at 09:56):Okay, that's working really well. Is the script that hacky? If it's really hard to re-integrate the dumpgraph option into coqdep, for my usecase having a disentangled, standalonebuildlibgraph script would be perfectly fine
Enrico Tassi (Mar 19 2021 at 10:49):If there is some interest we can put it on coq-community. I won't have much time to improve it myself, but I'm pretty sure others will be able to make the web part better (I really suck at that).
Emilio Jesús Gallego Arias (Mar 19 2021 at 15:11):@Yannick Forster it is not so hard to re-integrate back, the thing is that we rather try to consolidate all the scripts / tools , so we have a single point for users, improvements, etc....
Emilio Jesús Gallego Arias (Mar 19 2021 at 15:12):Indeed if requiring the vo is a problem, we could consider then having a syntactic-based tool, but let's document it officially in the manual and deprecate all others
Emilio Jesús Gallego Arias (Mar 19 2021 at 15:13):This https://metacpan.org/pod/Makefile::GraphViz seems to work, however not sure it is worth it.
Yannick Forster (Mar 19 2021 at 17:19):I've never used cpan before and did not manage to set it up properly to run the script, unfortunately
Yannick Forster (Mar 19 2021 at 17:20):@Enrico Tassi i like the idea to move the script to Coq community. The dot part is sufficient for me, but likely on the long run some options regarding the output format (dot, js, etc) would be nice.
Last updated: Oct 13 2024 at 01:02 UTC