Axiom
Project, 2024
AxiomAxiom
Timeline
1 Month, November 2024
Tools
Next.js
Typescript
Y.js
Socket.io
Express
SQLite
Prisma
Overview
Axiom is an IDE for SE212, the University of Waterloo's course for formal logic and proofs, for the software engineering department.
The course has a custom programming language for assignments and projects, and Axiom is a fully-featured editor designed specifically for this.
It'll be fully deployed on University servers for future software engineering cohorts to use!

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:

#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

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.

Boole editor
James editor

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

Rich Language Support
Syntax highlighting, autocomplete, go-to-defintion, hover tooltips, and more.
Intelligent Line Numbering
Continuity, incrementing, and decrementing for line numbers and references.
Collaboration In Workspaces
Work on projects with your group in sync, with visible cursors and selections.
Settings + Keybindings
Granular switches for language features, custom themes, and keyboard shorcuts.

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 monaco.languages.setLanguageConfiguration
  2. Next is syntax highlighting, where we need to write our tokenizer with monaco.languages.setMonarchTokensProvider
  3. Finally, we can set up autocomplete with monaco.languages.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!

  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:

  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.

  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

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!
  1. 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.
  1. You can only have one workspace open at a time
Invite collaborators interface
Create workspace interface

Implementation

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
};

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.

Context menu
Upload file

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 :)
Ishaan Dey
Updated 2/3/2025