Zulip Chat Archive

Stream: FLT

Topic: Project overview and coordination


Dragan Okanovic (May 01 2024 at 11:16):

Hi, I was wondering if the FLT project could use help on the "project management/overview" side.

I was looking at the FLT blueprint, and questions such as "who is/will be working on this chunk", "what's currently actually in progress", "what are the approximate timelines", "what PR or Zulip thread to follow for any specific chunk"... were difficult to infer. I imagined a scenario where all this information was available from the blueprint itself and could be easily answered and navigated to -- if these sorts of features are something that you feel might be useful, I'd be happy to explore how to enhance the blueprint and make it more information-rich and interactive.
(Tagging @Pietro Monticone as I saw his name on Github in relation to the blueprint.) Thank you for your consideration; happy to chat more.

Kevin Buzzard (May 01 2024 at 11:28):

yeah I've been doing other things this morning. The idea is to run it the way that other projects have been run recently. The answer to all your questions is "look at the thread on this stream which doesn't exist yet". See for example this post on another project.

Kim Morrison (May 01 2024 at 11:33):

@Kevin Buzzard, you might address this specifics of this offer --- I think software tooling to allow people to claim and unclaim things from the "what next" list could be helpful.

Although simply posting each bullet point as a separate post and using zulip emojis may be sufficient!

Kevin Buzzard (May 01 2024 at 11:50):

@Dragan Okanovic I am still really frustrated right now by the fact that loads of links are broken for me (but not for everyone) and I'm finding it very difficult to navigate around my own project; this is something to do with cookies apparently, but I've tried clearing lots of cookies and this hasn't solved the problem.

How about I get this sorted out and then I show you what my (naive) plans are by actually posting the first "outstanding tasks" post, and then you can take a look at what's going on and tell me a better way to manage things.

Kevin Buzzard (May 01 2024 at 12:03):

https://leanprover.zulipchat.com/#narrow/stream/416277-FLT/topic/Outstanding.20Tasks.2C.20V1/near/436488903

Kevin Buzzard (May 01 2024 at 12:04):

I had to close every github-related tab on my browser to get things working, so sorry to all the people I was in the middle of reviewing PRs for :-/

Dragan Okanovic (May 01 2024 at 12:25):

I didn't mean to put additional unnecessary pressure; I apologize for the somewhat unfortunate timing with my message.

My proposal would be to assign a "ticket" to each node in the blueprint.

Each ticket would have:

  • an ID (so it can be easily referenced in conversation and with URLs)
  • description and additional details (what's already in the blueprint basically)
  • current assignee(s) (people that "claimed" work items)
  • status (what colors in the blueprint signify), but maybe also with a short summary of the current state
  • a link to a running Zulip thread specific to that ticket only
  • optional: start and end date

All this information could live within the FLT Github repo, i.e. that would still be a single source of truth. We could update details via PRs, or we could try to make an actual blueprint interactive and be able to make updates from its UI directly (automatically creating and merging PRs behind the scenes).

We could even set up things so that each Github PR that references a particular ticket ID, gets linked to it as well and can be discovered from within the ticket.

Kim Morrison (May 01 2024 at 12:26):

Yeah, recording these details in the blueprint repo is way too much overhead.

Kim Morrison (May 01 2024 at 12:26):

I think we should look at what worked well for PNT, and then incrementally improve from there.

Kim Morrison (May 01 2024 at 12:27):

Adding and removing emojis on zulip is about the level of activation energy appropriate for claiming and releasing tasks.

Kim Morrison (May 01 2024 at 12:27):

But it would be better if this could be integrated into something dependency-graph-like.

Dragan Okanovic (May 01 2024 at 12:33):

I see. Here's what I can try to do as the next steps:

  • talk with Alex about PNT and learn more about where the friction was
  • make a proof of concept and come back to seek for some additional feedback

Any other recommendations, or people that I should talk to about this kind of work in general?

Kevin Buzzard (May 01 2024 at 12:43):

One idea (currently only partly implemented) was a GitHub issue for each node which was, or was about to be, or obviously a million miles away from being, able to be worked on by the community

Kevin Buzzard (May 01 2024 at 12:44):

That's what the "discussion" links to in the blueprint graph if you're lucky enough to find a node for which I've implemented a discussion issue

Kevin Buzzard (May 01 2024 at 12:49):

PS Dragan -- no need to apologise! I've just had a completely frantic April and am moving into a busy May but I had promised the community we'd be going live so here we are. I've never run anything like this before and am very open to hearing opinions on how to do it.

Dragan Okanovic (May 01 2024 at 12:55):

I love the idea of using native Github issues (https://github.com/features/issues) -- they do have pretty great features and be customized a lot (able to cover everything I've mentioned previously), and they could live together as part of the repo, but still not within its code, which is ideal. If we were to utilize Github issues, the only remaining piece would be linking them to the blueprint graph, which shouldn't be too difficult.

Patrick Massot (May 01 2024 at 13:17):

Providing a link from a node to a GitHub issue is already possible, as Kevin explained. The GitHub issue can then have a link to a Zulip discussion. Adding the possibility to also put a direct link to Zulip from the graph would be trivial, just copy-pasting the code that creates links to GitHub, but this would clutter the interface even more.

Patrick Massot (May 01 2024 at 13:20):

Dragan, it’s nice to be enthusiastic, but maybe spending ten minutes reading the documentation of leanblueprint would help avoiding suggesting to add features that already exist. Clicking on the Legend link in the graph would probably also help you.

Patrick Massot (May 01 2024 at 13:23):

Note also that, obviously, there have been a lot of previous discussion about all this during other projects. The current workflow is a delicate balance between information and overhead. It doesn’t mean it won’t change in the future. But assuming nobody ever thought about what you wrote is maybe a bit hasty.

Dragan Okanovic (May 01 2024 at 13:32):

@Patrick Massot I was only basing my writing on what I could see so far - no links from within the blueprint, not really utilizing project management features and doing things manually… technical capabilities were never really questioned.
The enthusiasm was directed exactly toward exploring an opportunity to learn if a fresh project such as FLT could benefit more over time from having some additional things put in place.
If there are other success stories that tried similar things, I’d love to learn about them.

Utensil Song (May 01 2024 at 13:53):

Some previous (long) discussions:

Some related issues: PatrickMassot/leanblueprint#9 PatrickMassot/leanblueprint#6

Utensil Song (May 01 2024 at 14:02):

Many solutions were suggested, some are over-engineered. It's indeed "a delicate balance between information and overhead" as Patrick suggested.

Besides blueprint and issues providing existing information ("map", "done", "claimed", "ongoing", etc.), the "Outstanding Task" mechanism is very useful for directing things towards the future ("next step", "need help", "to claim"), they work together like (relatively) static/organized part and the dynamic/inspiring part, moving the project forward. They can be seen as the Yang and Yin parts of the mechanism.

One possible missing link is that claiming requires a PR to add the issue to the corresponding node, unlike e.g. Giscuss would automatically create a discussion for a blog post. But this can be as lightweight as using a special label for these PRs, so they can be easily created and quickly merged.

Patrick Massot (May 01 2024 at 14:26):

Utensil, thanks for reminding me of those open issues. Do you agree they can safely be closed? There may be a couple of things left but at this stage it would probably be much clearer to open separate issues for those.

Utensil Song (May 01 2024 at 14:28):

Yes, many features are already implemented, the rest could be safely archived. If any of them seem useful again, I'll open separate issues. Thanks~

Patrick Massot (May 01 2024 at 14:29):

Ok, done.

Patrick Massot (May 01 2024 at 14:31):

Dragan’s message also makes me realize that the new documentation does not include links to existing blueprints and other places discussing this framework such as Terry’s very nice blog post. I’m pretty sure there used to be some links, I don’t know what happened. I’ll put them back.

Patrick Massot (May 01 2024 at 14:52):

I added a semi-random list of examples at the beginning of the README. I’d be happy to add or remove entries if someone feels forgotten or doesn’t want to appear there.

Pietro Monticone (May 01 2024 at 15:00):

Patrick Massot said:

I added a semi-random list of examples at the beginning of the README. I’d be happy to add or remove entries if someone feels forgotten or doesn’t want to appear there.

Thanks. I've just opened a PR adding FLT3 to the list.

Patrick Massot (May 01 2024 at 15:03):

I merged it. This list looks like our community is completely obsessed with FLT but I guess it’s partly true.


Last updated: May 02 2025 at 03:31 UTC