Olorin is a graphical frontend for Narya that allows the user to prove simple statements in predicate logic. It runs in a web browser, but once loaded it works offline without a server connection. See the "about" page for more information.
Olorin contains Narya as a git submodule, along with custom code in OCaml (compiled with js_of_ocaml) plus pure JavaScript that manages the graphics and browser interaction. To build it you need:
- An OCaml/opam environment with everything required to build Narya (see Narya's own build instructions). This compiles the proof checker to JavaScript.
- Node.js and npm, for the JavaScript client and the build/test tooling.
One-time setup, from the repository root:
git submodule update --init --recursive # fetch the Narya submodule
dune build olorin.opam # generate the opam file
opam install . --deps-only # install the OCaml dependencies (incl. Narya's)
npm install # install the JavaScript dependencies
npm install also installs the build tools (webpack) and the test runner (@playwright/test); see Testing for the extra one-time step of downloading a browser.
After the one-time setup above, build everything the browser needs into static/ with:
npm run build:static
This compiles the OCaml to JavaScript (dune build), bundles the client with webpack (npm run build), and copies the runtime assets — olorin.bc.js, z3-built.js/z3-built.wasm, and coi-serviceworker.js — into static/. This is the only command you need to rebuild after changing anything.
If you have only changed JavaScript or CSS (not the OCaml), you can skip the OCaml step and just run npm run build, which refreshes static/main.bundle.js. (In both cases you may need to Shift+Reload the page to pick up the new files.)
Once static/ has been built, it is self-contained: serve that directory with any static file server. For local use on the same machine:
npx http-server static -o -p 9999
The Algebra and Inequality worlds use Z3, whose WebAssembly build is multithreaded and therefore needs SharedArrayBuffer. The browser only exposes SharedArrayBuffer when the page is both cross-origin isolated (the Cross-Origin-Opener-Policy/Cross-Origin-Embedder-Policy headers) and in a secure context (https://… or http://localhost). http://localhost is a secure context, and coi-serviceworker.js supplies the isolation headers (by reloading the page once to turn them on), so a plain http-server works there.
A bare-IP LAN URL such as http://192.168.1.5:9999 is not a secure context, so SharedArrayBuffer is unavailable no matter what — and coi-serviceworker.js can't help (service workers don't even register on a non-localhost http origin). Z3 then fails with pthread_create: environment does not support SharedArrayBuffer. To run Olorin over a LAN, serve it over HTTPS instead:
npm run serve
This serves static/ over HTTPS with the cross-origin-isolation headers, using an auto-generated self-signed certificate (in the gitignored .certs/, with a SAN covering localhost and your detected LAN IPs) and binding all interfaces. Open the printed https://<your-LAN-IP>:8443/ URL on each device and accept the self-signed-certificate warning once. (Pass a port and/or root dir as arguments, e.g. npm run serve -- 9443.)
Alternatively, serve from any custom server that sets the cross-origin headers itself over HTTPS, in which case coi-serviceworker.js is unnecessary.
The runtime assets (main.bundle.js, olorin.bc.js, z3-built.*, coi-serviceworker.js) are not checked into git, so a fresh checkout has none of them until you build — npm run build:static puts them all in static/.
For development, you can instead symlink the generated files into static/ rather than copying them, so OCaml changes take effect as soon as you re-run dune build (and JavaScript changes as soon as you re-run npm run build), without re-running the full build:static:
cd static
ln -s ../_build/default/bin/olorin.bc.js .
ln -s ../node_modules/coi-serviceworker/coi-serviceworker.js .
ln -s ../node_modules/z3-solver/build/z3-built.* .
Olorin has a Playwright suite that drives the real built app in headless Chromium (selecting levels, dragging rules, wiring ports, etc.); see test/README.md for details.
One-time setup (in addition to npm install above):
npx playwright install chromium # download the browser
On Linux you may also need its system libraries: npx playwright install-deps (requires sudo).
The tests run against the built static/ directory. The simplest way to run them is:
npm test
which rebuilds static/ (via build:static, so the dune build is incremental — fast unless something actually changed) and then runs the suite, so you never test a stale build. If you've already built and want to skip straight to the tests, run npm run test:e2e instead. The runner automatically starts a static server with the correct cross-origin headers (test/server.js, on port 8123) for the duration of the run. Use npm run test:e2e:headed to watch the tests in a visible browser.
Run the suite via npm run test:e2e (not a bare playwright test): the npm script uses the project's local @playwright/test, whereas a global playwright is the browser-automation package only and will report error: unknown command 'test'.
One of the specs proves every level: for each one it restores a known-good proof and asserts the app still marks it complete, so a change to the rules, the typechecker, or the proof-restoring logic that breaks a level fails the build. Those proofs live in test/fixtures/proofs/, one file per level, named by a hash of the level's statement rather than by its number — so inserting, moving, or renumbering levels in client/levels.js never invalidates them. Only editing a statement retires its fixture, which is as it should be: the old proof may no longer prove it.
Fixtures are captured by solving a level in a real browser and saving the result, and are only written once the app confirms the proof is complete, so they're correct by construction. With static/ built, the auto-solver does as many as it can:
npm run gen:fixtures # solve every level the strategies can
node test/generate-fixtures.js --only 1-2-1,1-2-2 # just these levels
node test/generate-fixtures.js --list # which levels are covered (no browser needed)
Its strategies are propositional (∧-elimination and modus ponens forwards; ⊤/∧/∨/⇒ introduction backwards), so most levels have to be proved by hand instead: solve one in the app, click Export, save the JSON, and file it with
node test/add-fixture.js exported.json
which reads the level out of the proof itself — there's no level name to type, and no way to file a proof under the wrong level. Levels with no fixture yet are reported by the suite as a tracked TODO rather than a failure, so coverage grows a level at a time. See test/README.md for the details.
A world in client/levels.js may carry a courses list naming the courses it belongs to, which makes it that course's rather than the game's. Which code lets a student into a course is the COURSE_CODES table beside the levels, mapping each code to the course it is for; a student opens the game with it in the URL, as .../?code=math360fall2026.
The code is remembered, so the link is needed only once; a code in the URL always wins and takes the remembered one's place, which is how a student changes courses — or leaves one, with an empty ?code=, since no course claims that.
Without a code — or with one no course claims — a course's worlds are not in the game at all: they aren't in the chooser, and they neither gate another world nor are gated by one, so adding a course changes nothing for everyone else.
With a valid code, that course's worlds are there (another course's still aren't), and the rest of the game opens differently for someone who came for a term's work rather than to play through:
- every world outside any course is unlocked at novice from the start, every level of it;
- a world no longer waits on a difficulty above the one being opened (rule 3 of the unlock rules), so reaching a later world doesn't mean going up a difficulty in an earlier one.
The unlock rules never reach across the line between the game and a course: a course's worlds gate none of the game's own, and the game's own gate none of a course's, so a course starts at its own first level. Within a world, and among the worlds of one course, everything unlocks as it always does.
Higher difficulties are earned differently there, for the same reason. In the game proper a difficulty is opened a world at a time, by the worlds behind it; a course has none, so its own work is what opens it: one of its worlds opens at a difficulty once it is 80% complete at the difficulty below, and a level of it opens at a difficulty once that level has been solved at the difficulty below.
The above instructions compile a version of Olorin that runs entirely client-side in the user's browser, saving the list of completed levels locally in the browser. There is also a version that stores that information on a server associated with the user's email address; this is intended mainly for students in a class, so that the instructor can download a spreadsheet of grades by student and level. To compile this version of Olorin, simply change the definition SERVER = false in client/main.js to say true instead, and proceed as above.
The server program is in the server/ directory; place server.js in a directory on your server that contains a subdirectory static with the same files from static as before, and run it with node. It's designed to communicate with a couchdb database using cradle, so you'll need to install those things on your server too (for cradle you can use npm), and it expects a JSON file in its directory called config.json that defines the username and password for the couchdb instance (it assumes localhost and the standard port).
There is also an sslserver.js that's designed to use a self-signed certificate (for encryption, not identity verification) and serves the grade-downloading page for instructors, expecting to find grades.html and grades.bundle.js from static in an sslstatic subdirectory. It expects config.json to also define the keyfile and crtfile.