Initial commit

Changes

9 changed files (+247/-0)

• .gitignore (new)
  • @@ -0,0 +1,2 @@
    + /.lake + result
• Main.lean (new)
  • @@ -0,0 +1,84 @@
    + import Lean.Data.Json + import Raylean + + open Raylean Types + + def screenWidth := 800 + def screenHeight := 450 + + private def initialBallPosition : Vector2 := { x := screenWidth.toFloat / 2, y := screenHeight.toFloat / 2 } + + inductive Move where + | up + | down + | left + | right + | stay + + def updateBallPosition (d : Move) (p : Vector2) : Vector2 := match d with + | Move.right => { p with x := p.x + 2.0 } + | Move.left => { p with x := p.x - 2.0 } + | Move.up => { p with y := p.y - 2.0 } + | Move.down => { p with y := p.y + 2.0 } + | Move.stay => p + + def getMove : IO Move := do + if (← isKeyDown Key.right) then return Move.right + else if (← isKeyDown Key.left) then return Move.left + else if (← isKeyDown Key.up) then return Move.up + else if (← isKeyDown Key.down) then return Move.down + else return Move.stay + + def doRender : IO Unit := do + let mut ballPosition := initialBallPosition + while not (← windowShouldClose) do + let d ← getMove + ballPosition := updateBallPosition d ballPosition + renderFrame do + drawFPS (screenWidth - 100) 10 + clearBackground Color.white + drawText "Move the ball with arrow keys" 10 10 20 Color.blue + drawCircleV ballPosition 50 Color.red + closeWindow + + + structure Vehicle where + pos : Nat × Nat + dest : Nat × Nat + + + inductive Road + | none + | low + | high + deriving Lean.ToJson, Lean.FromJson + + structure Point where + roads : Vector Road 24 + occupant : Option Nat + + def Grid h w := Vector (Vector Point w) h + + def Tick (g : Grid h w) : Grid h w := Id.run do + return g + + + structure State where + datetime : Std.Time.PlainDateTime + height : Nat + width : Nat + grid : Grid height width + -- deriving Lean.ToJson, Lean.FromJson + + + def myroad : Road := .low + + def serialized := Lean.toJson myroad |>.compress + + def blah : Except String Road := Lean.Json.parse serialized >>= Lean.fromJson? + + + def main : IO Unit := do + initWindow 1280 720 "LeanTTD" + setTargetFPS 60 + doRender
• README.md (new)
  • @@ -0,0 +1,38 @@
    + # LeanTTD + + 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 + + ## Building + + Hmm raylib_bindings.c needs a patch + + Write a flake.nix for this? Raylean looks pretty nasty to build
• flake.lock (new)
  • @@ -0,0 +1,27 @@
    + { + "nodes": { + "nixpkgs": { + "locked": { + "lastModified": 1781577229, + "narHash": "sha256-lrp67w8AulE9Ks53n27I45ADSzbOCn4H+CNW1Ck8B+8=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "567a49d1913ce81ac6e9582e3553dd90a955875f", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "nixpkgs": "nixpkgs" + } + } + }, + "root": "root", + "version": 7 + }
• flake.nix (new)
  • @@ -0,0 +1,36 @@
    + { + description = "An OpenTTD-like game written in Lean"; + + inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; + + outputs = + { self, nixpkgs }: + let + system = "x86_64-linux"; + pkgs = nixpkgs.legacyPackages.${system}; + in + { + packages.${system}.default = pkgs.leanPackages.buildLakePackage { + pname = "leanttd"; + src = self; + version = "0.1"; + lakeHash = "sha256-d5tV9nqv5XwBKNBBxsnEPujbjpR9TgdTp5NUV3bX10g="; + buildInputs = [ pkgs.raylib ]; + # This fixes a linker error + hardeningDisable = [ "bindnow" ]; + postConfigure = '' + # Patch Raylean to fix a compilation error + patch -p1 < ./raylean.patch + # Make sure the linker can find libraylib.so + substituteInPlace lakefile.toml --replace-fail \ + '["-lraylib"]' \ + '["-L${pkgs.raylib}/lib", "-lraylib"]' + ''; + }; + apps.${system}.default = { + type = "app"; + program = "${self.packages.${system}.default}/bin/leanttd"; + }; + formatter.${system} = pkgs.nixfmt-tree; + }; + }
• lake-manifest.json (new)
  • @@ -0,0 +1,26 @@
    + {"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/funexists/raylean", + "type": "git", + "subDir": null, + "scope": "funexists", + "rev": "580d008ec18413b0ed35bd4d20f9a5044f650c2c", + "name": "raylean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/funexists/lens-demo.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0c90e83fd65f3b845dc46c1454309e0dbda25a71", + "name": "«lens-demo»", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.28.0", + "inherited": true, + "configFile": "lakefile.lean"}], + "name": "LeanTTD", + "lakeDir": ".lake", + "fixedToolchain": false}
• lakefile.toml (new)
  • @@ -0,0 +1,12 @@
    + name = "LeanTTD" + version = "0.1.0" + defaultTargets = ["leanttd"] + + [[lean_exe]] + name = "leanttd" + root = "Main" + moreLinkArgs = ["-lraylib"] + + [[require]] + name = "raylean" + scope = "funexists"
• lean-toolchain (new)
  • @@ -0,0 +1,1 @@
    + leanprover/lean4:v4.30.0
• raylean.patch (new)
  • @@ -0,0 +1,21 @@
    + diff --git a/.lake/packages/raylean/c/raylib_bindings.c b/.lake/packages/raylean/c/raylib_bindings.c + index 902a945..7539506 100644 + --- a/.lake/packages/raylean/c/raylib_bindings.c + +++ b/.lake/packages/raylean/c/raylib_bindings.c + @@ -314,11 +314,11 @@ static inline Camera2D camera2D_of_arg(lean_obj_arg camera) { + return (Camera2D){offset, target, rotation, zoom}; + } + + -lean_obj_res getRandomValue(uint32_t min, uint32_t max) + - __attribute__((optnone)) { + - // BUG: This always seems to return `min` + - return lean_io_result_mk_ok(lean_box_uint32(GetRandomValue(min, max))); + -} + +// lean_obj_res getRandomValue(uint32_t min, uint32_t max) + +// __attribute__((optnone)) { + +// // BUG: This always seems to return `min` + +// return lean_io_result_mk_ok(lean_box_uint32(GetRandomValue(min, max))); + +// } + + lean_obj_res initWindow(lean_obj_arg width, lean_obj_arg height, + b_lean_obj_arg title) {