hwh-core

A minimal height–width model with formal constraints (Lean 4).

A First Experiment (Any Computer)

This repository pins its Lean version in lean-toolchain, so your first run will fetch exactly the toolchain it expects.

Prerequisites

• Git
• A working shell (macOS Terminal, Linux shell, or Windows PowerShell/WSL)

Install Lean (via elan)

macOS / Linux / WSL:

curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y

Windows (PowerShell):

iwr -useb https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1 | iex

Then ensure elan is on your PATH (a new shell session is often enough). If you can run lean --version, you’re ready.

Build and Run

Clone the repo, build it, and run the tiny executable:

git clone https://github.com/harpertoken/hwh-core.git
cd hwh-core
lake build
lake exe hwh_core

You should see:

area = 200

What “HWH” means (here)

HWH is treated as a small core for reasoning about Height/Width and simple rectangle/layout invariants in Lean.

Notes

• CI runs lake build + lake exe hwh_core on every push and pull request.
• If a build fails on first run, it’s usually a missing elan/lake on PATH or a proxy blocking downloads; fix the environment and re-run.
• Repo hooks/policy are aligned with our dotfiles setup: https://github.com/dotfiles-mac (e.g., strict Conventional Commit messages enforced on push).

Pre-commit versions (pinned)

As of 2026-03-24, the latest versions are:

• pre-commit (the framework): 4.5.1 (released 2025-12-16): https://pypi.org/project/pre-commit/
• pre-commit-hooks (hook collection): 6.0.0 (released 2025-08-09): https://pypi.org/project/pre-commit-hooks/

Website (separate branch)

This repo has a minimal static webpage on the site branch (kept out of main on purpose).

• Content lives under site/ on that branch (including site/assets/cover.png).
• A GitHub Pages deploy workflow also lives on that branch at .github/workflows/pages.yml and runs only for pushes to site.