Project: Integrate Paperproof with Coq

[lakesare]

Description

Are there visualisations similar to Paperproof in other proof assistants? Coq has ProofTree (2011) and Traf (2018), however both of these systems were rather experimental/proof-of-concept works, and they are not actively supported at the moment. We think other proof assistants could benefit from Paperproof, and this project is concerned with making Paperproof work for Coq.

Like mentioned in our Lean Together 2024 talk, Paperproof is built in such a way that integrating it with other proof assistants and other editors is straightforward.

If you look at our root folder, you will see /lean, /extension and /app subfolders.

• In /lean folder, we keep our Lean parser;
• in /extension folder, we keep code for our VSCode extension; and
• in /app, we keep our rendering engine written in React

In order to make Paperproof work with Coq, you would need to write Coq parser, and slightly adjust Coq's VSCode extension, like shown on the following image.

To get you started with this project, we would suggest you to take a look at Traf - you should be able to glean some inspiration from their implementation of Coq parser

Skills Required

• Coq (required)
• Javascript (nice to have)

---

Note: we actively welcome contributors to this issue, and we should be able to help you out if you decide to take it up.