Start playing with Lean

Author: xaionaro@dx.center

.github/workflows/lean_action_ci.yml

@@ -0,0 +1,36 @@
+name: Lean Proofs & Differential Tests
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  proofs:
+    name: Lean 4 Proofs
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: leanprover/lean-action@v1
+        with:
+          build-args: ""
+          lake-package-directory: proofs
+
+  differential:
+    name: Differential Tests (Lean <-> Go)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: actions/setup-go@v5
+        with:
+          go-version: "1.24"
+
+      - uses: leanprover/lean-action@v1
+        with:
+          build-args: ""
+          lake-package-directory: proofs
+
+      - name: Run differential tests
+        run: make test-differential

.gitignore

@@ -29,3 +29,4 @@ capi/manifests/.gen_*.yaml
 cligen
 ndkcli
 build/
+/.lake

Main.lean

@@ -0,0 +1,4 @@
+import ProofsTmp
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"

Makefile

@@ -25,7 +25,8 @@ BUILD_DIR      := build
 
 .PHONY: all capi specs idiomatic clean regen fixtures test lint check-examples check-no-capi \
         e2e e2e-build e2e-examples e2e-examples-test e2e-audio \
-        ndkcli ndkcli-commands ndkcli-release install-ndk
+        ndkcli ndkcli-commands ndkcli-release install-ndk \
+        proofs test-differential
 
 all: specs capi idiomatic
 
@@ -97,6 +98,15 @@ regen: clean specs capi idiomatic
 test:
 	go test $$(go list ./... | grep -v -E '/(capi|cmd|tests|examples)/|/ndk/[a-z][a-z0-9]*$$') -count=1
 
+# Build Lean 4 proofs (requires elan/lake toolchain).
+proofs:
+	cd proofs && lake build
+
+# Run differential tests comparing Go implementations against Lean oracle.
+# Requires: elan/lake toolchain. Builds the oracle automatically.
+test-differential: proofs
+	go test ./tools/pkg/capigen/ ./tools/pkg/idiomgen/ -run TestDifferential -v
+
 # Verify cmd/ and examples/ do not import capi packages.
 check-no-capi:
 	@if grep -rl '"github.com/xaionaro-go/ndk/capi' cmd/ examples/ 2>/dev/null; then \

ProofsTmp.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `ProofsTmp` library.
+-- Import modules here that should be built as part of the library.
+import ProofsTmp.Basic

ProofsTmp/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

lakefile.toml

@@ -0,0 +1,10 @@
+name = "proofs_tmp"
+version = "0.1.0"
+defaultTargets = ["proofs_tmp"]
+
+[[lean_lib]]
+name = "ProofsTmp"
+
+[[lean_exe]]
+name = "proofs_tmp"
+root = "Main"

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.16.0

proofs/.github/workflows/lean_action_ci.yml

@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1

proofs/.gitignore

@@ -0,0 +1 @@
+/.lake