Next Coq UI discussion: Monday, October 2 · User interfaces devs & users

Let's meet from 3:30 - 5 PM, Paris time, on Monday, October 2. (That's 9:30 - 11 AM in Philadelphia.) Same Zoom link as usual.

We'll use this session for presentations of ongoing projects by academic teams. Please let me know if you want to present something!

  - Benjamin

Jelle Wemmenhove (Sep 07 2023 at 13:14):

@Jim Portegies and I would like to present the project we are working on called Waterproof. It is an adoptation of Coq that we use to help students learn how to write proofs in the Analysis 1 course at our university. By writing proofs in the program, they can get feedback much quicker than with regular homework exercises.

The program consists of two components: a custom UI and a custom Coq library. The UI takes the form of a VSCode extension that uses coq-lsp, we also use the new .mv files for documents that consist of Coq code and human readable text. We added some more quality-of-life features for students that, for example, allow them to quickly insert mathematical symbols.

The custom library provides tactics for writing Coq proofs that more closely resemble the style of regular math proofs. For example, the custom tactic notations take the form of full English sentences, and we put more focus on the types that carry the relevant mathematical information instead of the terms. The manipulation of terms is handled by a customizable automation system instead.

Benjamin Pierce (Sep 07 2023 at 16:20):

Emilio Jesús Gallego Arias (Sep 14 2023 at 16:27):

@Benjamin Pierce if there is time we'd like to do a jsCoq 2.0 demo, IMHO 10 minutes for the demo (+ questions) would be enough; we can always add the demo to the queue for the next meeting.

Benjamin Pierce (Sep 16 2023 at 20:58):

Théo Zimmermann (Oct 04 2023 at 12:29):

@Jim Portegies and @Jelle Wemmenhove: following your presentation of Waterproof, I'm interested in experimenting with the VS Code extension without the coq-waterproof library. As I mentioned during the talk, this would help if Waterproof was available somewhere besides the VS Code marketplace. This can be OpenVSX (ideal, because then it is accessible to anyone using a non-Microsoft-blessed version of VS Code) or even as a vsix file attached to a release on GitHub. Currently, we can download the vsix file from the Microsoft Marketplace website, but even this is difficult. On the command-line, I found the direct download URL to be https://marketplace.visualstudio.com/_apis/public/gallery/publishers/waterproof-tue/vsextensions/waterproof/0.9.8/vspackage, but after downloading it just a few times, the marketplace is already blocking me ("Request was blocked due to exceeding usage of resource 'Count' in namespace 'AnonymousId'."). In other words, Microsoft is not friendly to people wanting to use extensions published in their marketplace with a VS Code version that was not built by them.

Théo Zimmermann (Oct 04 2023 at 12:31):

By the way, you may be interested in joining the new #Teaching [with] Coq stream. (At least, this is where I would naturally go to discuss my experiments around using coq-lsp or Waterproof for teaching.)

Jim Portegies (Oct 05 2023 at 15:26):

Karl Palmskog (Oct 05 2023 at 15:57):

@Jim Portegies is both the UI and the plugin/language called simply "Waterproof"? Or can they be referred to more precisely as something like "the Waterproof proof language" and "the Waterproof interface"? I ask because then it could make sense to list Waterproof under several headings at https://github.com/coq-community/awesome-coq

Jim Portegies (Oct 11 2023 at 14:20):

@Karl Palmskog , thank you for your question, it would be nice if we could be listed under awesome-coq. We would be happy with the designations "Waterproof proof language" and "Waterproof editor". Thanks!

Stream: User interfaces devs & users

Topic: Next Coq UI discussion: Monday, October 2

Benjamin Pierce (Aug 30 2023 at 19:34):