MonotoniCity
MonotoniCity is a city-building and transport simulation game written using the Lean proof assistant, kinda like a mix of OpenTTD and Simcity with a hint of OpenRCT2. The GUI is implemented using Raylean, which I'm also a contributor to.
Build roads! Controlled-access highways! Roundabouts! Diverging diamond interchanges! Stack interchanges! (Just don't build cloverleaves, they suck) Tunnels! Connect up industries! Write custom scripts in Lean!
Lean? Isn't that a math tool or a drug?
Yeah, Lean is most commonly used for math proofs, but it also has many powerful programming capabilites which are extremely helpful for proof automation. And yes, it's very addictive.
To play MonotoniCity on Linux, simply download a prebuilt AppImage. If you're on a different OS or would like to compile the game, skip to the build instructions at the bottom
Gameplay
MonotoniCity has both a console and a GUI window. The console is pretty useless, except for the help command which lists all the hotkeys.
Each cell of the game grid is 5m wide and the grid lines are drawn every 10 cells. The big colored boxes are buildings, and the green and red boxes on the sides are entrances and exits respectively. Roads are one-way so make sure your roads go into the entrance and out of the exit.
The amazing world of MonotoniCity is inhabited by peeps. Each peep lives in a house or apartment and has a workplace that they commute to.
What the heck is a peep?
This is a peep:
You should connect up houses and apartments to the various commerical buildings. Monotonicity also has several OpenTTD-style industry chains:
- Farm → Grocery store
- Mine → Industrial plant → Factory → Shop
- Bank ↔ Bank
The graphics suck!
It's abstract art.
Where's the music?
There's no soundtrack currently but you can play some nice tracks from the Simutrans soundtrack using mpv --playlist=soundtrack --loop-playlist --no-video. For a fully authentic audio experience, play this game while sitting at a noisy intersection outside.
Where are the gas stations?
Gas stations? This is the 21st century, not the 20th! All peeps are 100% electric and hundreds of kilometers of battery life.
But where do they get the electricity from?
Oh, there are super fast chargers at every building entrance. And all the buildings have solar panels on the roof. Hooray for clean energy!
Why are there no trains and only cars? This is clearly designed to create miserable, unwalkable, excessively sprawled cities!
Who said they're cars? The peeps are clearly yellow chick marshmallow things.
How do I write custom scripts?
The easiest way is to add a new Action in the game code. You can also write scripts in other programming languages and use the MonotoniCity console, but the performance will be worse and you won't get nice transactions with rollbacks like in Lean.
Why the name?
monotonicity is a tactic in Lean.
Building
To build this using Nix (least painful trust me), just run nix build. It'll probably take at least half an hour since the version of Lean in nixpkgs is too old so first it compiles the latest Lean.
On NixOS you can also build this by hardcoding the directory of libraylib.so in lakefile.toml (for instance moreLinkArgs = ["-L/nix/store/2ndddyrjb1ahx05kmsjqvzkagz1bdmpk-raylib-6.0/lib", "-lraylib"]) and running lake build, which is much faster due to caching.
Otherwise, try running the build.sh script written by Paul Cadman.
To build an AppImage that can run on any Linux distro, run nix bundle --bundler github:NixOS/bundlers#toAppImage --impure.