lean4-htt/tests/lake/examples
Mac Malone 41ecccec6d
feat: lake: hoist compiled configurations (#13683)
This PR moves the compiled Lake configurations (e.g., `lakefile.olean`)
from the package's `.lake/config` directory to the workspace's
`.lake/config`. This removes a potential source contention between
workspaces sharing a dependency.
2026-05-08 18:00:37 +00:00
..
bootstrap
deps feat: lake: hoist compiled configurations (#13683) 2026-05-08 18:00:37 +00:00
ffi fix: lake: moreLinkObjs|Libs on a lean_exe (#11117) 2025-11-08 04:20:42 +00:00
hello
precompile
reverse-ffi fix: symbol clashes between packages (#11082) 2025-11-19 02:24:44 +00:00
scripts