There are 193 `.v`

files 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.

@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)

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.)

@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.

OK, I could do a pull request with a basic plot/graph this weekend, and it could be tweaked later.

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.

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

Karl Palmskog said:

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.

Perhaps the simplest is to just add href links in the pdf ?

Where the graph(s) can be found? Or I'm asking too early?

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

May I ask for the graph? (I mean, maybe it's already generated but not in the repository and/or the pdf.)

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