lean4-htt/src/lake/examples
Mac Malone 7a076d0bd4
fix: lake: package duplication in workspace (#3957)
Fixes a bug where packages that appeared multiple times in the
dependency tree would be duplicated in the workspace (and in manifests).
Added a regression test for this to prevent this from happening again in
the future.

This was first reported in
l[eanprover/mathlib4#12250](https://github.com/leanprover-community/mathlib4/pull/12258#discussion_r1571834509).
2024-04-23 09:50:10 +00:00
..
bootstrap feat: lake: alternative TOML config (#3298) 2024-03-28 02:35:02 +00:00
deps fix: lake: package duplication in workspace (#3957) 2024-04-23 09:50:10 +00:00
ffi chore: update tests to account for .lake 2023-11-13 20:31:24 -05:00
hello feat: lake: alternative TOML config (#3298) 2024-03-28 02:35:02 +00:00
precompile feat: lake: alternative TOML config (#3298) 2024-03-28 02:35:02 +00:00
reverse-ffi fix: split libInit_shared out of libleanshared (#3421) 2024-02-22 19:16:32 +00:00
scripts fix: lake: leave run options for script (#3064) 2023-12-13 17:45:30 +00:00
targets fix: do not dllexport symbols in core static libraries (#3601) 2024-03-15 11:58:34 +00:00