Tools like leanblueprint for other proof assistants, especially Coq?

Question

In my (relatively little) experience with Lean, one of the things I’ve appreciated most is the leanblueprint tool. For those not familiar with it, it’s a tool for planning a Lean development and tracking its progress. Roughly, your “blueprint” consists of a LaTeX writeup of the mathematical content of the project (as sketchy or detailed as you want), in which you annotate some theorems, definitions, etc with identifiers from the Lean development. Then leanblueprint compiles this to a webpage (well, a set of interlinked html files) including a dependency graph of the marked definitions and results (example), colour-coded to show which are successfully completed in the formalisation, and linked to their text in the writeup. For a longer writeup see Terence Tao’s blog.

It’s a fantastic help for large developments, and pretty useful even for small ones. I found it useful enough that going back to Coq (where I mostly work) I miss it and have found myself trying to approximate its features with some very crude and ad hoc scripts. I’m not aware of any comparable existing tools, but I may be missing them by not searching for the right keywords. Hence my question: Are there any similar tools for Coq (or other proof assistants) that I’ve missed?

The key combination of features I’m interested in is providing an overview of dependencies and progress-tracking at the level of definitions/results, not just files/modules, for planned development and work in progress, not just for material that’s already successfully formalised. The integration with a human-readable text is nice, but less my focus here.

The closest tool I’m aware of for Coq is coq-dpdgraph, but that’s designed mainly for tracking/analysing dependencies within a formalisation, not for forward planning or a status overview.

Answer 1

TL;DR: porting the Lean blueprint tool to Coq would probably be at most two days of work, at least if you only want the core functionality.

The leanblueprint tool actually contains very little Lean-specific code. You could easily make a Coq version. First it relies on plasTeX which has nothing to do with Lean, it is a LaTeX compiler written in python, which is also used by the Stacks project for instance (the algebraic geometry website, no link with StackExchange). Then a first plasTeX plugin, plastexDepGraph handles defining dependencies between LaTeX declarations and drawing a graph. This is again completely independent from Lean.

It is only the second plasTeX plugin, leanblueprint that contain Lean-specific code. There are two main pieces to this second plugin. The first one is a command line interface that helps creating blueprints in an existing Lean project. That one indeed has some pretty specific Lean code, including things setting up GitHub continuous integration. The second main piece of the second plugin is adding to the dependency graph information about what is already formalized. The core of this is trivial to adapt to other proof assistants. What really depends on the proof assistant is how to link to the formalization code.

Answer 2

An interesting tool, tho quite primitive compared to lean-blueprint is coq-lsp, which supports both literate Markdown and TeX.

This is a different idea, but could be useful. I think also Alectryon could be pretty useful in this context.

Answer 3

As far as I know, there are two things in the Coq ecosystem, none of which exactly fit your needs.

The first is the coq-dpdgraph library, which you already found. It might still provide some/all of the dependency information you might need, though?

The second is the coqdep command line tool, which is primarily used for the build system (in particular, your files do not need to compile to obtain a dependency graph, which can be very useful during development). In particular, it used to have a dumpgraph option which would generate a dot file with the dependency information. But that option was removed, and despite some interest in it has not been revived as of today. There are multiple scripts out there that generate similar dependency information in graph-like form from the raw output of coqdep (see here or here, mathcomp has a particularly fancy version of it too). But in any case this is about file-level dependency and does not support the white/blue/green colouring of blueprint files.

So I think a tool of this kind would be a very nice addition to the Coq ecosystem, and filling in a need that is not really addressed today!