2026-07-15 07:06 UTCIn-site rewrite3 min readUpdated: 2026-07-15 07:13 UTC

Show HN: Lean64 – doom64 style FPS on Lean 4

Lean64 is a barebones 3D first-person shooter implemented in Lean 4, inspired by Doom 64. It is a clean-room experiment, not a port, featuring original art and sound. The game includes full combat, AI, weapons, maps, HUD, and audio, all written in Lean with a minimal C shim for rendering and input.

SourceHacker News AIAuthor: threepts

Notifications You must be signed in to change notification settings

Fork 0

Star 0

BranchesTags

Open more actions menu

Folders and files

NameName

Last commit message

Last commit date

Latest commit

History

1 Commit

assets

ffi

.gitignore

Demo.lean

LICENSE

Launcher.lean

Main.lean

README.md

lake-manifest.json

lakefile.lean

lean-toolchain

lean64-barrel.gif

lean64-boss.gif

lean64-cache.gif

lean64-campaign.gif

lean64-chaingun.gif

lean64-difficulty.gif

lean64-impact.gif

lean64-intermission.png

lean64-key.gif

lean64-level.png

lean64-map.png

lean64-map2-automap.png

lean64-map2.png

lean64-pause.png

lean64-rush.gif

lean64-secret.png

lean64-title.png

lean64-x-5s-60fps.mp4

lean64-x.gif

lean64.png

Repository files navigation

A barebones, windowed 3D first-person game implemented in Lean 4. This is a clean-room Doom-style experiment, not a source port of Doom64EX and not a replacement for the copyrighted Doom 64 data files.

Watch the 5-second 1080p60 gameplay clip with audio

Run it

Install elan, then:

lake build lake exe lean64

For the deterministic five-second 60 FPS highlight loop with synchronized audio:

lake build lean64demo lake exe lean64demo

Controls:

Enter: deploy from the title screen or continue to Map 2

1 / 2 / 3 on the title screen: Easy, Hard, or Nightmare

W / S: move forward and backward

A / D: strafe

mouse or arrow keys: yaw and pitch the camera

Shift: sprint

Space: fire

E: use doors and switches

1 / 2: select the double-barrel shotgun or collected chaingun

Tab or M: toggle the automap

P: pause or resume

R: restart after victory or death

Esc or Q: quit

What is implemented

a Win32/OpenGL presentation path with a retained software renderer for tests and screenshots

3D vectors, camera-space transforms, and perspective projection in Lean

triangle mesh construction, camera state, and render submission authored in Lean

GPU depth testing, distance fog, and procedural repeating material textures for the live game

a barycentric software rasterizer and per-pixel depth buffer retained as a reference backend

distance-aware muzzle illumination that briefly warms nearby world geometry and monsters

procedural brick, riveted-metal, dirty-floor, ceiling, and emissive materials

a two-map mini-campaign with distinct red-brick and teal-metal arenas

campaign transitions that carry health, weapons, ammunition, difficulty, and score forward

alternating Map 2 bulkheads that create a zig-zag combat gauntlet into a stronger Warden finale

two staged encounter rooms joined by an interactive rising bulkhead

classic red-key progression with a collectible 3D access card and locked bulkhead

multi-part monster meshes with bodies, heads, limbs, glowing eyes, pain flashes, and timed collapse deaths

dormant/alert monster awareness, pursuit, obstacle collision, melee attacks, and player damage

ranged monster fireballs with travel, collision, and impact damage

telegraphed ranged attacks with interruptible charge-up effects

a heavy final-arena warden with a unique horned mesh, eight health, boss bar, purple reactor attacks, and bonus score

shootable explosive barrels with splash damage, player damage, debris, and chain reactions

world-space blood sprays, metal sparks, explosion debris, persistent blood pools, and capped wall-impact marks

first-person movement, collision, yaw, pitch, sprinting, and unobstructed hitscan shooting

movement-driven view bob, weapon sway, faster sprint cadence, and a decaying shotgun recoil kick

captured relative mouse-look with automatic cursor restoration

a two-shell super shotgun with held-fire cadence, hard recoil, muzzle smoke, opening breech, visible shell insertion, wood furniture, and shaped muzzle flash

five-pellet horizontal shotgun spread with close-range stacking, multi-monster blasts, classic vertical auto-aim, and individual wall sparks and impact marks

a collectible multi-barrel chaingun with rotary animation and rapid held-fire cadence

separate shell and bullet ammunition pools with weapon-aware HUD display

persistent corpses, health vials, shell boxes, and hit confirmation

synthesized asynchronous shotgun and chaingun reports

original synthesized wake, pain, death, fireball, impact, door, secret, pickup, barrel, keycard, and Warden cues

event-prioritized audio dispatch authored in Lean, with the native shim limited to asynchronous WAV playback

health, ammo, damage vignette, crosshair, score state, victory, death, and restart

distinct full-screen red damage and warm pickup palette pulses

a procedural title screen, reusable pixel font, pause overlay, numeric HUD, and readable state messages

timed map-name cards for The Foundry and Black Circuit

selectable Easy/Hard/Nightmare modes scaling enemy health, aggression, ammunition, damage, and score

a full-screen intermission tracking real elapsed time, kills, secrets, shots, hits, accuracy, and score

a live automap showing geometry, doors, supplies, alerted enemies, corpses, and the exit

dynamic red/amber/green lock feedback in-world, on the HUD, and on the automap

a hidden wall-rune secret with health, ammunition, score rewards, and a pixel-art discovery banner

a second hidden, roofed maintenance chamber with a moving facade, trapped monster, supplies, and optional combat

clear-gated glowing exit pads, per-map intermissions, and a campaign-complete state

a real-time state/update/render loop with frame pacing

The game state, AI, combat, camera, meshes, material IDs, lighting changes, and HUD composition live in Lean. The native shim owns the Win32/OpenGL context, uploads Lean's triangle stream and HUD texture, and handles input and audio.

Checks

lake exe lean64 --smoke-test lake exe lean64 --window-smoke lake exe lean64 --gpu-benchmark lake exe lean64 --screenshot lake exe lean64 --promo-frames lake exe lean64 --level-screenshot lake exe lean64 --chaingun-frames lake exe lean64 --map-screenshot lake exe lean64 --secret-screenshot lake exe lean64 --barrel-frames lake exe lean64 --key-frames lake exe lean64 --cache-frames lake exe lean64 --boss-frames lake exe lean64 --impact-frames lake exe lean64 --title-screenshot lake exe lean64 --difficulty-frames lake exe lean64 --pause-screenshot lake exe lean64 --intermission-screenshot lake exe lean64 --map2-screenshot lake exe lean64 --map2-automap lake exe lean64 --campaign-frames lake exe lean64 --rush-frames lake exe lean64 --audio-demo

The next large milestone toward source-port territory would be a legally supplied WAD reader, BSP traversal, texture atlases, sprite animation, and a larger authored campaign. Lean 64 deliberately ships only original procedural art and synthesized audio.

About

doom64 but lean

Resources

Readme

License

MIT license

Uh oh!

There was an error while loading. Please reload this page.

Activity

Stars

0 stars

Watchers

0 watching

Forks

0 forks

Report repository

Releases

No releases published

Packages 0

Uh oh!

There was an error while loading. Please reload this page.

Contributors

Uh oh!

There was an error while loading. Please reload this page.

Languages

Lean 85.3%

C 14.7%