monotonicity

A city-building and transport simulation game written in Lean

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  10. 10
  11. 11
  12. 12
  13. 13
  14. 14
  15. 15
  16. 16
  17. 17
  18. 18
  19. 19
  20. 20
  21. 21
  22. 22
  23. 23
  24. 24
  25. 25
  26. 26
  27. 27
  28. 28
  29. 29
  30. 30
  31. 31
  32. 32
  33. 33
  34. 34
  35. 35
  36. 36
  37. 37
  38. 38
  39. 39
  40. 40
  41. 41
  42. 42
  43. 43
  44. 44
  45. 45
  46. 46
  47. 47
  48. 48
  49. 49
  50. 50
  51. 51
  52. 52
  53. 53
  54. 54
  55. 55
  56. 56
  57. 57
  58. 58
  59. 59
  60. 60
  61. 61
  62. 62
  63. 63
  64. 64
  65. 65
  66. 66
  67. 67
  68. 68
  69. 69
  70. 70
  71. 71
  72. 72
  73. 73
  74. 74
  75. 75
  76. 76
  77. 77
  78. 78
  79. 79
  80. 80
# MonotoniCity

A city-building and transport simulation game written in Lean

## Building

To build this using Nix (least painful trust me), just run `nix build`.

On NixOS you can also build this by hardcoding the directory of `libraylib.so` in `lakefile.toml` and running `lake build`, which can be much faster due to caching.

Otherwise, install Raylib and run `lake build` and hope for the best. It probably won't work, but you can give it a try.

To build a (huge) precompiled bundle that can run on any Linux distro, run `nix bundle .#packages.x86_64-linux.default`.

I recommend running the game with `rlwrap` for a slightly nicer console.

## Random notes

Rewrite (a small subset of) OpenTTD in Lean!

- Focus on road vehicles for now for simplicity
- Top-down rectangular grid instead of isometric
- Basically it'll be a probalistic cellular automata
- Use https://github.com/funexists/raylean/

So anyways we have a rectangular grid of points 5m apart and you can add a directed road between a point and any of its 8 neighbors (24 once I add bridges and tunnels, or maybe I should add them right from the beginning?). At any time, at most one vehicle occupies each point.

Buildings are rectangles with top right and bottom left corners in this grid.

By default, vehicles move at a realistic speed (3 ticks per second) but we can run the simulation faster too

Two kinds of roads, regular and highway. Vehicles can move two segments at a time on highways but only in the same direction (TODO: how to make the pathfinder exit on a multilane highway?)

If only one possible road out of a point, then the vehicle just goes ahead. Otherwise it runs a BFS pathfinder to its destination and checks if each road going out is occupied in order of distance until it finds one that's not (TODO: don't use a road if its distance exceeds the shortest path by a huge factor?)

It's probalistic because the order that the vehicles are processed during each tick is random, so for instance a random vehicle moves at a 4-way stop rather than the one that has been there the longest. This also makes merges random. You can use a yield sign to push a vehicle to the bottom of this order. A vehicle cannot move to a spot that is occupied during the current grid state or the next state (TODO: handle crossing diagonal roads)

Traffic lights are kinda janky but shouldn't be too hard to support.

Vehicles seat exactly one person and at the beginning of the day they randomly leave houses or apartments for workplaces in the city and there are also trucks between factories and stores and stuff

Time starts at 8 AM and ends at midnight each day

The internal data representation of the game is a 2D vector for the grid for fast access for info about a point and arrays of vehicles, buildings etc to easily iterate over all those objects. To save the game we dump all these to JSON and vice versa for loading a save (unfortunately this bloats up the binary ugh). I don't really need to plan this out in advance but rather just add more fields as needed

First step: render the grid using raylib

Street names


TODO: bundle seems to be missing deps?

NFO: Initializing raylib 6.0
INFO: Platform backend: DESKTOP (GLFW)
INFO: Supported raylib modules:
INFO:     > rcore:..... loaded (mandatory)
INFO:     > rlgl:...... loaded (mandatory)
INFO:     > rshapes:... loaded (optional)
INFO:     > rtextures:. loaded (optional)
INFO:     > rtext:..... loaded (optional)
INFO:     > rmodels:... loaded (optional)
INFO:     > raudio:.... loaded (optional)
Fontconfig error: Cannot load default config file: No such file: (null)
Gtk-Message: 19:24:22.735: Failed to load module "colorreload-gtk-module"
Gtk-Message: 19:24:22.735: Failed to load module "window-decorations-gtk-module"
WARNING: GLFW: Error: 65542 Description: EGL: Failed to get EGL display: Success
WARNING: GLFW: Failed to initialize Window
WARNING: SYSTEM: Failed to initialize platform
INFO: TIMER: Target time per frame: 16.667 milliseconds


https://www.raylib.com/cheatsheet/cheatsheet.html


The street names are from https://github.com/rossburton/barnum/blob/master/source-data/street-names.txt


## Why the name?

`monotonicity` is a tactic in Lean.