SE212 is a course at the University of Waterloo on formal logic, proof systems and styles, rudimentary model theory, logic-based specification, correctness proofs, and their applications in software engineering.
It has a custom language called George. Here's an example of a natural deduction proof:
#check ND
forall x . P(x) => Q(x), exists x . P(x) |- exists x . Q(x)
1) forall x . P(x) => Q(x) premise
2) exists x. P(x) premise
3) for some xu assume P(xu) {
4) P(xu) => Q(xu) by forall_e on 1
5) Q(xu) by imp_e on 3,4
6) exists x . Q(x) by exists_i on 5
}
7) exists x . Q(x) by exists_e on 2, 3-6
A few students over the past few years created 2 editors for George: Boole and James. They're both a great step up from plaintext editing since they come with syntax highlighting, autocomplete, a file explorer, and a few other features.
While these options are fine, I found it evident that there's a ton of improvements and features that could be added to significantly improve the experience. Thankfully I've gotten pretty familiar with editors, especially with Monaco (the same library that VSCode uses), since I built Sandbox last summer.
The frontend is a Next.js app that communicates with the backend, which runs both an HTTP server and a socket.io server. The database is SQLite.
The editor in Axiom uses the same library as VSCode, giving us familiar keyboard shortcuts and features out of the box. But how do we add rich support for a completely new language?
Luckily, the Monaco editor has a very detailed languages API.
monaco.languages.register
and monaco.languages.setLanguageConfiguration
monaco.languages.setMonarchTokensProvider
monaco.languages.registerCompletionItemProvider
It'd be nice to have go-to-definition since rules reference line numbers (⌘+Click
), and Monaco has a definitions provider for this!
monaco.languages.registerDefinitionProvider("george", {
provideDefinition: (model, position) => {
// Specifically handles line references that appear after the "on" keyword
// Supports both single line references (e.g. "1") and ranges (e.g. "6-12"),
// returning their definitions within the current proof section
},
});
Let's focus specifically on line numbering. A few pain points:
For the first point, we can add a key handler for Enter
so new lines automatically have the incremented line number with correct indentation. The second point falls under the same key event, but we'll need to iterate through the lines and update them according to the change.
editor.onKeyDown((e) => {
if (e.keyCode === monaco.KeyCode.Enter) {
// Handle auto-indentation when cursor is between empty braces {}
// Handle numbered lines (e.g., "1) some content")
// Find section boundaries marked by #q, #u, #a, or #check
// Search backwards for the nearest boundary
// Search forwards for the next boundary
// Find all sequential numbered lines that follow the current line
// Insert new line with incremented number and update following lines
// Update line numbers and references in all following lines
}
});
The third point is a little more tricky, as text deletion can be done in many ways, and handling every edge case is impractically complex. I chose to not have auto-decrementing by default, but rather making it more intentional through the shortcut ⌘+X
. This also decrements line number references in rules!
editor.addCommand(monaco.KeyMod.CtrlCmd | monaco.KeyCode.KeyX, () => {
// Store the selected text before deletion
// Get current section boundaries
// Find section boundaries
// Update line references and numbers
// Update line numbers for following lines
// Update references in "on" statements
// Push edits to execute all operations
});
Lastly, we can add hover tooltips on rules with monaco.languages.registerHoverProvider
.
If you're interested in the full implementation, check out this file in the Github repo: frontend/lib/lang.ts
When building Sandbox, I used Liveblocks to handle real-time collaboration on the Monaco editor. This project, however, has real-time collaboration implemented from scratch with Y.js and Socket.io.
The collaboration system is based on Workspaces.
Workspaces are shared folders for multiplayer collaboration. You can create workspaces based on course assignments or projects. You can invite and manage collaborators. You can view your invitations in Settings.
The backend keeps track of active workspaces and connections in-memory, along with their collaborative documents.
const workspaces = new Map<string, Workspace>();
const fileAwareness = new Map<string, Map<string, Map<string, AwarenessState>>>();
const clientFiles = new Map<string, { workspaceId: string; path: string }>();
The collaborative documents are from Y.js, and clients are kept in sync with a pub/sub architecture. The library has some useful utility functions for this, including encodeStateAsUpdate
and applyUpdate
. We also store awareness data (cursor position and highlights) for each file.
We're managing socket.io connections using rooms for workspaces.
socket.on("joinRoom", async ({ workspaceId, path }) => {
// Check if user has permission to access this workspace
// Initialize workspace if needed
// Load requested file
// Send current doc state
// Update client's current file
// Send current awareness states for this file
});
socket.on("leaveRoom", ({ workspaceId }) => {
// Remove client from room
// Notify others that user left
// Clean up awareness data & maps
// Delete workspace in memory if no connected clients left
});
On the client side, we need to manage collaborative documents and synchronization with the server. It's important to be careful here since awareness data is linked to a document, not the parent workspace.
export const setupCollaboration = async ({...}) => {
// Join collaboration room for this specific file
// Initialize Yjs document and text type
// Synchronize initial state by:
// 1. Getting existing document updates
// 2. Fetching current file content
// Apply synchronized state to the document
// Ensure document content matches server content
// Set up awareness protocol for cursor positions and user presence
// Initialize local user state with random cursor color
// Bind Monaco editor to Yjs document with awareness
// Handle incoming document updates from other users
// Broadcast local document changes to other users
// Broadcast awareness changes (cursor position, selection) to other users
// Update cursor position in awareness when local user moves cursor
};
The settings modal has options to toggle autocomplete, accept suggestions on Enter
, intelligent line numbering features, and more. All major actions (proof checking, toggling panels, etc.) have keyboard shortcuts for maximum productivity.
There's also fully customizable theming, with support for both light and dark mode. Presets are coming soon!
The panels are fully resizable and collapsible. There's tabs to support opening multiple files, uploading, downloading, and much more.
The project is fully open source on Github. There's also a local-only deployment at se.ishaand.com.
Unfortunately, working with the University to deploy the project for my software engineering cohort took a little longer than expected, so it'll instead be ready for the next cohort and future students to come.
Thanks to those who helped with some parts along the way!