From 311a022c793360b4b73181926633f2cefc0a4d61 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 5 Sep 2026 15:27:47 +0000 Subject: [PATCH] lean: put elan's bin on PATH, so a fresh checkout finds lake `make test` in the lean port failed with "lake: not found" on a machine whose Lean came from elan. elan installs to ~/.elan/bin and a stock install does not put that on a non-login shell's PATH, so make's own shell could not see it. CI never hit this: it unpacks a pinned lean release to /opt/lean/bin and puts that on GITHUB_PATH itself, so only a local checkout was affected. Prepending a directory that does not exist is a no-op, which is why CI stays as it was. This is the line sekreto's lean port already carries, for the same reason. Verified by running `make test` with a PATH that has no elan on it: 18 modules compile, 572 corpus entries pass. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01SD5pZ6WjP8nMiUcAkRZjNN --- lean/Makefile | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/lean/Makefile b/lean/Makefile index d74e00a..ffe459b 100644 --- a/lean/Makefile +++ b/lean/Makefile @@ -16,6 +16,17 @@ # (voxgig/struct) and Lean has no port of it, so src/Plugin/Value.lean # parses the corpus. +# elan installs to ~/.elan/bin, which a stock install does not put on a +# non-login shell's PATH, so `make test` in a fresh checkout found no +# lake. CI does not go through elan at all — it unpacks a pinned release +# to /opt/lean/bin — so only a local checkout was affected, and this is +# the same line sekreto's lean port carries. Prepending a directory that +# does not exist is a no-op, so CI is unchanged. `make` runs each recipe +# in its own shell; exporting PATH here is the only place all of them +# see it. +ELANBIN := $(HOME)/.elan/bin +export PATH := $(ELANBIN):$(PATH) + LAKE ?= lake BIN = .lake/build/bin/run