Pierre Castéran (Dec 09 2022 at 07:56): Pierre Castéran (Dec 09 2022 at 07:56):There are 193 .vfiles in the Hydra-battles project (including the 45 files from Russel's legacy).
Displaying the whole dependency graph may cause readability issues. Is it possible to split the whole library into "clusters"
and organize the presentation into maps of each cluster (and a large scale map of clusters) ?
For instance, the Ackermann sub-library contains clusters about first-order logic, PA, gödel encoding, PR functions.
Karl Palmskog (Dec 09 2022 at 07:59):@Pierre Castéran you mean something like this, but possibly in different graphs/files? https://runtimeverification.github.io/vlsm-docs/latest/coqdoc/map.svg (green stuff is general library, purple is the domain-specific code)
Karl Palmskog (Dec 09 2022 at 08:02):these file-level dep graphs can be produced using scripts/makefiles and scoped quite easily to a library or sublibrary (for example, based on full filenames or filename prefixes, etc.)
Pierre Castéran (Dec 09 2022 at 08:12):@Karl Palmskog Looks nice. I would just add « global » graphs, like « the PA cluster depends on the FOL cluster ». But it’s not urgent, I’m now working on bulletization/presentation of Ackermann and goedel.
Karl Palmskog (Dec 09 2022 at 08:26):OK, I could do a pull request with a basic plot/graph this weekend, and it could be tweaked later.
Karl Palmskog (Dec 09 2022 at 09:32):also, do we want these graphs included in the PDF proper? It's easy enough to put .svg files together with the HTML deployment on each push to master, but including in LaTeX is a bit more work.
Karl Palmskog (Dec 09 2022 at 09:33):the top-level project dependency graph is actually given by either (1) the .opam files, or (2) the dune files ((package ...)). I don't know an easy way to extract out the information from there
Pierre Castéran (Dec 09 2022 at 10:16):Karl Palmskog said:
also, do we want these graphs included in the PDF proper? It's easy enough to put
.svgfiles together with the HTML deployment on each push tomaster, but including in LaTeX is a bit more work.
Perhaps the simplest is to just add href links in the pdf ?
Lessness (Dec 20 2022 at 01:28):Where the graph(s) can be found? Or I'm asking too early?
Karl Palmskog (Dec 20 2022 at 08:30):I got a bit stuck with the CI part of the graphing. It's easy to add scripts to generate, but it needs a bunch of tools that need to be added to CI for inclusion of graphs in the pdf. I think I will do it in two separate PRs, and ask for Nix help in the second PR
Lessness (Dec 28 2022 at 22:01):May I ask for the graph? (I mean, maybe it's already generated but not in the repository and/or the pdf.)
Karl Palmskog (Dec 28 2022 at 22:42):I didn't figure out the colors yet, but here's an SVG (click on "Raw"): https://gist.github.com/palmskog/058996c24f8536c9679ae97df134169f
Last updated: Jun 11 2023 at 01:30 UTC
