lean blueprint dependency graph

Stream: general

[Yakov Pechersky]

I would like to use the framework provided by the Lean blueprint package (tex building, dep graph management, links to descriptions) for a non-lean technical and scientific project. Are there any good tips for doing so? On particular, I'd like to start out with a dep graph first and flesh out the descriptions later. @Patrick Massot

[Patrick Massot]

I've been meaning to make a separate plugin without Lean stuff forever, but it simply never reaches the top of the priority pile. In principle this isn't difficult at all, you can simply get the code at https://github.com/PatrickMassot/leanblueprint/ and remove all Lean stuff. What would be even nicer (but would take a lot more time) would be to avoid creating duplicated code by having a non-Lean plasTeX plugin and then the leanblueprint one working on top of this general purpose one.

[Matej Penciak]

Sorry to dredge up this old conversation, but I wanted to get leanblueprint working on a non-Lean 3 (actually a Lean 4) formalization project, so I made a fork that I think gets rid of all the Lean stuff: https://github.com/mpenciak/noleanblueprint.

I kind of just followed my nose for the most part and got rid of the leanproject specific stuff, so I don't know if I did it absolutely correctly.

[Matej Penciak]

It works well enough for my purposes so far though (we're using it in the https://github.com/yatima-inc/ZKSnark.lean repo)

[Patrick Massot]

Could you at least open an issue in the leanblueprint repo so that I don't forget? Right now I don't have any time for this.

[Colleen Robles]

Hi, I'm try to create a blueprint for a project following the instructions at
https://github.com/leanprover-community/liquid/tree/master
just the PDF version (not the html). I can't get the dependency graph. I'm compiling with XeLaTex in TexShop on a Mac. Any idea what I might be doing wrong? or have overlooked?

[Patrick Massot]

There is no pdf output for the dependency graph, it appears only in the html version.