How to make blueprint

Stream: new members

[Junqi Liu]

I saw that your dependency graph of FLT-regular prime is so beautiful! Does anyone know how to draw it?

[Yaël Dillies]

Yes, you look at eg https://github.com/YaelDillies/LeanAPAP, copy-paste the blueprint folder, copy-paste the .github/workflow folder, copy-paste the docs folder, copy-paste tasks.py, edit things as you like (in particular replacing LeanAPAP by your project name), enable Github pages on your repo, and :tada:

[Riccardo Brasca]

cc @Luigi Massacci

[Luigi Massacci]

I think you meant to cc @Pietro Monticone?

[Riccardo Brasca]

ahahaha sorry, too many italian students :D

[Patrick Massot]

This is a very outdated answer. Please don’t do that kind of copy-paste anymore. Follow the instructions at https://github.com/PatrickMassot/leanblueprint/blob/master/README.md and report any issue there if needed.

[Rémy Degenne]

@Patrick Massot could you have a look at the pr https://github.com/PatrickMassot/leanblueprint/pull/15 about these instructions?

[Pietro Monticone]

And this one too if possible https://github.com/PatrickMassot/leanblueprint/pull/16