Software tool for formal proof collaboration

Stream: Equational

[Iva Babukova]

Hi everybody,

I'm very interested in helping mathematicians organise formalisation projects by building productivity software tools that would allow them to more effectively collaborate on large-scale formal proofs.

My background is in scientific software development (mostly biology/ bioinformatics/ data science). I've worked at Harvard Medical School on open source software in the field of single cell transcriptomics, specifically on projects called Vitessce and Cellenics. I have a lot of experience designing and building software for researchers.

I follow the "lean startup" software product development methodology. I'm planning to put together a very minimally useful software product very quickly (in a matter of weeks). Before I even write any code I'd like to iterate on a couple of versions of mock-up designs (please see below for v1 wireframes):

Lean queue

I'd like to build a tool that fits well and improves on the existing formalisation collaboration workflow, which I understand is built on github, Blueprint/ dependency graph software and of course Zulip chat.

In the first iteration, I'd like to allow users to perform two actions:

• Submit "jobs" -- which I'd like to propose are initially only self-contained lemmas (with Mathlib as the only dependency), together with short informal description of what needs to be formalised.
• Allow users to claim these "jobs" and eventually resolve them as "done".

If this works well enough I will then get your feedback on various ideas for improvement and I'll start working on a feature roadmap.

More immediately, I'd really appreciate it if you could help me understand your individual workflows. I would really benefit from your personal perspectives on the following topics:

What are the current issues that you're facing when working on formalisation projects? How do these issues differ between "lean formaliser" and "task splitter" personas?

What are the limitations of existing tools that you work with on your formalisation projects (Github, Blueprint, Zulip, Loogle/Moogle, others?)

What do you think of the proposed wireframes? Am I prioritising the most essential feature set for the minimum viable product (MVP) of such a collaboration tool? Please remember that in the "lean startup" methodology the idea is to build a very scrappy MVP and then start adding features once the product gains initial userbase, based on the feedback from initial users.

Am I focusing on the right problem? Are there more pressing issues that a collaboration software should be addressing?

[Shreyas Srinivas]

I am planning to write this into the paper we will submit

[Shreyas Srinivas]

Currently we have automated a non trivial amount of management tasks for large projects using GitHub project, CI, and such.

[Shreyas Srinivas]

Loogle and Moogle are already available to any user through a variety of interfaces, the web, multiple vscode extensions, and the new LeanSearch tool

[Shreyas Srinivas]

Further Loogle can be locally run

[Shreyas Srinivas]

So I don't think search tools are really an issue at the moment.

[Shreyas Srinivas]

Secondly the mechanism we set up to propose and claim tasks already allows more general task definitions than lemmas and theorems

[Shreyas Srinivas]

The project dashboard already adds a nice interface to manage these tasks and move them appropriately and automatically with CI actions. The blueprint template is also set to get a number of updates.

[Shreyas Srinivas]

I don't see how any product can outdo the tight integration that GitHub projects offers on top of GitHub repositories.

[Shreyas Srinivas]

We also have a gitpod setup to instantaneously open branches and PRs, and the only limitation with our gitpod setup is having to wait for lake cache to fetch Mathlib oleans after loading the directory. But this is because of lake managing the dependencies of each project locally. Working with the FRO on improving lake is one avenue to contribute although I don't think this is easy at all. I can't speak for the FRO, but they might very well have their own plans and policies about this.

[Shreyas Srinivas]

Even if somehow we get some AI involved for task management (which I highly doubt makes sense given the precise nature of the task), GitHub's copilot will almost certainly outperform any external tool

[Shreyas Srinivas]

And further, if we ever run into the limits of GitHub projects, which we haven't so far, there is still Trello

[Shreyas Srinivas]

Therefore I can't in good conscience recommend competing with these rather well established products yet. Maybe when we get down to writing about our current processes, we will have a better view of the limitations. I would still expect that these can be handled by CI actions very similar to what we already have.

[Shreyas Srinivas]

I think it will take a much larger project with an order of magnitude more contributors, for the limitations of our present system as well as other existing tools to become apparent

[Shreyas Srinivas]

One place to gain a glimpse of our contributions process is the CONTIBUTING.md file on our repository. Although some instructions are specialized to this project, it gives a nice overview of what we are currently using.

[Shreyas Srinivas]

One thing I find sorely missing is a lot of standard programming style libraries in lean itself, that can help us read in and process files of other file formats and data. Lean already handles JSON and toml very well. But it lacks libraries for large scale data processing. It would also be nice if we could generate diagrams from within lean using a specialised DSL. Some of these abilities are already present in proof widgets, but we are using scripts in other languages for generating visualisations of our data. There is also the issue of lean lacking a nice web framework.

[Terence Tao]

Perhaps the one thing which is missing right now is the ability to open up a custom Lean playground web page associated to a given Lean formalization task, that handles all the library building etc. of the project in a backend invisible to the user. This opens up the possibility of casual contributions to a formalization project coming from someone who is passing by and is willing to spend a few minutes with a five-line formalization task, but is not motivated enough to overcome the friction costs of downloading a repository, fetching the cache, building the files, etc..

For Equational Theories, we are lucky that our core implications are so simple that we can place all the relevant definitions directly into the standard Lean playground (e.g., here), but this will almost certainly not be the case for a more typical project, e.g., the Carleson project. In principle the tools exist to set this up already (I keep hearing Gitpod being relevant for this, but I am unfamiliar with this tool), but if they were somehow integrated seamlessly with the rest of the project, that could help.

[Shreyas Srinivas]

For gitpod

[Shreyas Srinivas]

You can install the gitpod extension on your browser

[Shreyas Srinivas]

And because we have gitpod configured already for equational_theories, you will be able to open the repository in any branch with one click (and a small wait time once the editor opens for lake to fetch the mathlib cache)

[Shreyas Srinivas]

We can also just add the gitpod link by default to every PR that is created.

[Adam Kurkiewicz]

And how do mathematicians find working with git? In particular, in a situation where typical contribution is formalisation of a single lemma there will exist a simplified git workflow (one could create functionality for applying a custom git patch that only acts on the one lemma, and not on the entire file, as opposed to working with pull requests).

[Terence Tao]

Huh, okay, after clicking on a lot of "OK" and "Accept" buttons I seem to have managed to open a remote VScode session to a gitpod version of the repository, which looks more or less identical to my local repository. For someone like myself who is already committed to working on the project, a local repository seems better, but I could imagine a remote repository being slightly more convenient for a casual participant. If it is easy to add a gitpod link at relevant places in the project, I guess it couldn't hurt, though.

[Shreyas Srinivas]

I think those accepts and okays are part of the first time setup with gitpod. From the second time it is a one click process (with a bit of waiting because of lake cache)

One thing to note about gitpod is that it is a cloud service that allows 50 hours of free usage per month. I would guess that academic users can get more hours than that. For context, I would find 50 hours per month adequate for a semester long course with lean assignments with quite a bit to spare. My normal use case for gitpod is precisely what you describe: quickly opening a PR or branch in an editor

[Shreyas Srinivas]

Adam Kurkiewicz said:

And how do mathematicians find working with git? In particular, in a situation where typical contribution is formalisation of a single lemma there will exist a simplified git workflow (one could create functionality for applying a custom git patch that only acts on the one lemma, and not on the entire file, as opposed to working with pull requests).

If someone can simplify git CLI usage I think that would be greatly welcome. Git is solving a fairly complex problem and a lot of software infrastructure has been built to work with it and support it. Currently I recommend vscode's git support + the git graph extension

[Adam Kurkiewicz]

I really like the idea of a well integrated custom Lean playground for quick submissions -- but I think there are non-trivial issues to make something like this work well and at scale (although gitpod looks quite promising -- despite the 50h limit -- I haven't used it so far).

Specific issues with running Lean 4 in the browser are discussed here:

#lean4 > wasm build

For Lean 3 it was possible to run everything client-side in the browser, which meant that, for example, Kevin's Natural Number Game could be played by many players at the same time -- each time the code was compiled in the player's browser so compilation on a web server wasn't a bottleneck.

For Lean 4 it appears to be much harder to do as discussed in the thread linked earlier, which necessitates using a web-server at the backend. This leads to scalability issues, for example currently the NNG Lean 4 game states that their scalability limit "is about 70 simultaneous games".

[Adam Kurkiewicz]

Ideally we could get performant, well-polished WASM builds for Lean 4, but this appears non-trivial.

[Adam Kurkiewicz]

Creating a super-straightforward git workflow limited to individual lemmas would be much easier to do I think.

[Adam Kurkiewicz]

That's the Lean 4 Game Server at the moment, looks like it's at capacity:

Screenshot 2024-10-07 at 23.49.35.png

[Shreyas Srinivas]

A per lemma workflow would be unsuitable for this project, where we have had gigantic PRs containing thousands of lemmas

[Terence Tao]

It could perhaps have been usable as a human-only interface; automated submissions would have to use the "tradesman's entrance" for deliveries :laughing:

[Shreyas Srinivas]

Haha. More seriously, people have tried to outdo and simplify git for 20 years, with little success. The only other version control system that I know to actually have a lot of usage is perforce. But that's expensive.

There are ways to completely avoid the command line with git. For example you might see the version control icon on the left panel of the editor (it's the symbol that looks like a Y). It can handle basically everything one needs to do on git as a contributor. I also like the nice interactive interface that git graph gives me. I cannot recommend it enough.

[Shreyas Srinivas]

https://marketplace.visualstudio.com/items?itemName=mhutchie.git-graph

[Shreyas Srinivas]

I have the first suggestion for enhancing the workflow: A GUI way of claiming tasks, perhaps even from the project dashboard. I still want to explore trello + github for this. There are always going to be people who look at the instruction that asks them to comment propose PR #xyz and then comment propose #xyz or vice versa.

[Shreyas Srinivas]

Basically a gui option that triggers the same CI workflow we have.

[Terence Tao]

As a workaround, is it possible to configure the Github bot to take multiple forms of input, so for instance propose #xyz is interpreted as propose PR #xyz?

[Shreyas Srinivas]

that is possible, but it has the downside of being brittle.

[Shreyas Srinivas]

we are basically string pattern matching.

[Shreyas Srinivas]

CC: @Pietro Monticone

[Shreyas Srinivas]

with a graphical interface the possibility of these errors is entirely removed since users can only pick one of the available options.

[Johan Commelin]

I think mercurial is also reasonably popular.
And I'm secretly cheering for Pijul.

[Amir Livne Bar-on]

There's something non-trivial that went right in this project, that maybe can be automated. It felt (at least as a contributor) that project management and automation tools, and additional maintainers, appeared several times just before the active maintainers were overwhelmed.

The effect for contributors was that contributions never felt blocked for a long time.

Maybe we can automate suggestions for project management? E.g. a notification triggered by 5 open PRs that suggests moving to tasks, and setting up workflows and CONTRIBUTING.md. Or a trigger to suggest adding maintainers. Or when the community grows, adding a CoC and community management tools.

[Adam Kurkiewicz]

Shreyas Srinivas said:

I have the first suggestion for enhancing the workflow: A GUI way of claiming tasks, perhaps even from the project dashboard. I still want to explore trello + github for this. There are always going to be people who look at the instruction that asks them to comment propose PR #xyz and then comment propose #xyz or vice versa.

I think Iva is proposing something like this on slide 2 of her mock-up in the "Status" column, where one can claim a task through clicking "Pick":

Lean queue

[Shreyas Srinivas]

Amir Livne Bar-on said:

There's something non-trivial that went right in this project, that maybe can be automated. It felt (at least as a contributor) that project management and automation tools, and additional maintainers, appeared several times just before the active maintainers were overwhelmed.

The effect for contributors was that contributions never felt blocked for a long time.

Maybe we can automate suggestions for project management? E.g. a notification triggered by 5 open PRs that suggests moving to tasks, and setting up workflows and CONTRIBUTING.md. Or a trigger to suggest adding maintainers. Or when the community grows, adding a CoC and community management tools.

So the last 4 are supposed to be done before a project starts. We can simply improve the blueprint template for CoC and CONTRIBUTING.md. Moving tasks between columns is automatic at present

[Shreyas Srinivas]

Adam Kurkiewicz said:

Shreyas Srinivas said:

I have the first suggestion for enhancing the workflow: A GUI way of claiming tasks, perhaps even from the project dashboard. I still want to explore trello + github for this. There are always going to be people who look at the instruction that asks them to comment propose PR #xyz and then comment propose #xyz or vice versa.

I think Iva is proposing something like this on slide 2 of her mock-up in the "Status" column, where one can claim a task through clicking "Pick":

Lean queue

I get that, but replication of the entire project interface feels overkill, especially given how much it does and how much we have already automated it. The post also suggests that Iva is looking at a broad range of options for features to contribute

[Shreyas Srinivas]

Johan Commelin said:

I think mercurial is also reasonably popular.
And I'm secretly cheering for Pijul.

Mercurial used to be popular, but not anymore. As of 2023, it is less popular than even SVN: https://stackoverflow.blog/2023/01/09/beyond-git-the-other-version-control-systems-developers-use/

[Shreyas Srinivas]

My point is, working on DevOps tools within the framework of GitHub + GitHub projects and using actions is a better avenue for contributions than reinventing the wheel, especially since there is a lot to reinvent within the wheel

[Shreyas Srinivas]

Also, Iva proposes a minimally usable product. Given the existence of tools like Trello and GitHub, this is a very hard sell, because the minimum usable product that works better than existing tools is already a tremendously complex one, that is replicating a lot of functions that we are currently taking for granted with our setup.

[Pietro Monticone]

Terence Tao said:

As a workaround, is it possible to configure the Github bot to take multiple forms of input, so for instance propose #xyz is interpreted as propose PR #xyz?

Sure, I’ll do it later today or tomorrow.

[Iva Babukova]

Shreyas Srinivas said:

My point is, working on DevOps tools within the framework of GitHub + GitHub projects and using actions is a better avenue for contributions than reinventing the wheel, especially since there is a lot to reinvent within the wheel

I definitely wouldn't want to reinvent the wheel, this is why I stopped myself from building something before I hear your thoughts on what the biggest blockers to collaboration currently are.

Adam Kurkiewicz said:

Shreyas Srinivas said:

I have the first suggestion for enhancing the workflow: A GUI way of claiming tasks, perhaps even from the project dashboard. I still want to explore trello + github for this. There are always going to be people who look at the instruction that asks them to comment propose PR #xyz and then comment propose #xyz or vice versa.

I think Iva is proposing something like this on slide 2 of her mock-up in the "Status" column, where one can claim a task through clicking "Pick":

Lean queue

Yes, this is exactly what I was thinking of. But I wouldn't want to re-implement trello or github or any other existing platform, I was more thinking of something light that eventually connects the tools that you already use in your workflow in order to make the whole process much more streamlined and remove current bottlenecks.

[Evgenia Karunus]

Terence Tao said:

Perhaps the one thing which is missing right now is the ability to open up a custom Lean playground web page associated to a given Lean formalization task, that handles all the library building etc. of the project in a backend invisible to the user

Gitpod was already mentioned - Github Codespaces can do it too, and probably it's better to let people use a single site for everything they do with Lean, Github. It's pretty straightforward to set it up with any Lean project (link).
Re:submitting PRs via git - Github Codespaces make it a straigthforward UI-only process too (link).