lean4-htt/tests/lake
Mac Malone 326f43aa3a
fix: lake: meta import transitive import artifacts (#13600)
This PR fixes a Lake issue where the IR for a `meta import`'s transitive
imports was not included in the import artifacts Lake provided to Lean
(e.g., via `--setup`). When using the Lake artifact cache, this could
produce "missing data file" errors due to absent IR.

Closes #13419

---------

Co-authored-by: Claude Code <noreply@anthropic.com>
2026-05-03 17:44:46 +00:00
..
examples feat: lake: fixedToolchain package configuration (#12935) 2026-03-17 02:37:55 +00:00
tests fix: lake: meta import transitive import artifacts (#13600) 2026-05-03 17:44:46 +00:00
.gitattributes
.gitignore
lakefile.toml feat: lake: cached compressed module artifacts (#12914) 2026-03-16 04:36:19 +00:00
run_clean.sh test: tests/lake/run_test.sh (#13501) 2026-04-25 04:36:08 +00:00
run_test.sh test: tests/lake/run_test.sh (#13501) 2026-04-25 04:36:08 +00:00