Background

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:

1#check ND
2
3forall x . P(x) => Q(x),  exists x . P(x) |- exists x . Q(x)
4
51) forall x . P(x) => Q(x) 	   premise
62) exists x. P(x) 	           premise
73) for some xu assume P(xu) {
8   4) P(xu) => Q(xu)           by forall_e on 1
9   5) Q(xu)                    by imp_e on 3,4
10   6) exists x . Q(x)          by exists_i on 5
11   }
127) exists x . Q(x)             by exists_e on 2, 3-6

Motivation

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.

Architecture

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.

Features

Editor

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.

Basic Features

1. Set up the language configuration with monaco.languages.register and setLanguageConfiguration
2. Next is syntax highlighting, where we need to write our tokenizer with setMonarchTokensProvider
3. Finally, we can set up autocomplete with registerCompletionItemProvider

Deeper Features

It'd be nice to have go-to-definition since rules reference line numbers (⌘+Click), and Monaco has a definitions provider for this!

1  monaco.languages.registerDefinitionProvider("george", {
2    provideDefinition: (model, position) => {
3      // Specifically handles line references that appear after the "on" keyword
4      // Supports both single line references (e.g. "1") and ranges (e.g. "6-12"),
5        // returning their definitions within the current proof section
6    },
7  });

Let's focus specifically on line numbering. A few pain points:

1. We need to manually type out every line number
2. If I want to add lines in the middle of my proof, I need to manually increment every following line
3. Same issue as above except for deleting lines

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.

1  editor.onKeyDown((e) => {
2    if (e.keyCode === monaco.KeyCode.Enter) {
3      // Handle auto-indentation when cursor is between empty braces {}
4      // Handle numbered lines (e.g., "1) some content")
5        // Find section boundaries marked by #q, #u, #a, or #check
6        // Search backwards for the nearest boundary
7        // Search forwards for the next boundary
8        // Find all sequential numbered lines that follow the current line
9        // Insert new line with incremented number and update following lines
10          // Update line numbers and references in all following lines
11    }
12  });

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!

1editor.addCommand(monaco.KeyMod.CtrlCmd | monaco.KeyCode.KeyX, () => {
2    // Store the selected text before deletion
3    // Get current section boundaries
4    // Find section boundaries
5    // Update line references and numbers
6      // Update line numbers for following lines
7      // Update references in "on" statements
8
9    // Push edits to execute all operations
10  });

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

Workspaces

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.

Properties

1. Permissionless

• Any user in a workspace has equal permission to invite users, revoke invitations, remove collaborators, edit files, and delete the workspace
• Only invite users you trust!

2. Unique folder

• You can only have one workspace for a folder. For example, you cannot have more than one workspace for Project 1.
• You can not accept an invitation to a workspace for a folder that you already have access to.

3. You can only have one workspace open at a time

Implementation

The backend keeps track of active workspaces and connections in-memory, along with their collaborative documents.

1const workspaces = new Map<string, Workspace>();
2const fileAwareness = new Map<string, Map<string, Map<string, AwarenessState>>>();
3const 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.

1socket.on("joinRoom", async ({ workspaceId, path }) => {
2  // Check if user has permission to access this workspace
3  // Initialize workspace if needed
4  // Load requested file
5  // Send current doc state
6  // Update client's current file
7  // Send current awareness states for this file
8});
9
10socket.on("leaveRoom", ({ workspaceId }) => {
11  // Remove client from room
12  // Notify others that user left
13  // Clean up awareness data & maps
14  // Delete workspace in memory if no connected clients left
15});

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.

1export const setupCollaboration = async ({...}) => {
2  // Join collaboration room for this specific file
3
4  // Initialize Yjs document and text type
5
6  // Synchronize initial state by:
7  // 1. Getting existing document updates
8  // 2. Fetching current file content
9
10  // Apply synchronized state to the document
11
12  // Ensure document content matches server content
13  // Set up awareness protocol for cursor positions and user presence
14  // Initialize local user state with random cursor color
15  // Bind Monaco editor to Yjs document with awareness
16  // Handle incoming document updates from other users
17  // Broadcast local document changes to other users
18  // Broadcast awareness changes (cursor position, selection) to other users
19  // Update cursor position in awareness when local user moves cursor
20};

Settings

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!

More UI Features

The panels are fully resizable and collapsible. There's tabs to support opening multiple files, uploading, downloading, and much more.

Results

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.

Collaborators

Thanks to those who helped with some parts along the way!

• Rajan and Ian helped with the backend implementation, testing, and bug fixes
• Akshar created the custom theme system and suggested our default syntax highlighting colours
• Elijah worked a bit on initialization and gave us moral support :)