Skip to content

Commit ce85346

Browse files
authored
perf: work around non-linearity in ElimDead (#14245)
This PR aims to improve performance of the compiler for large do blocks, such as observed in `Grind.Arith.Linear.StructId`. It changes a hash set that is used non-linearly into a tree set.
1 parent 1391dbb commit ce85346

1 file changed

Lines changed: 2 additions & 1 deletion

File tree

src/Lean/Compiler/LCNF/ElimDead.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,8 @@ so we opt for a safe subset.
1616

1717
namespace Lean.Compiler.LCNF
1818

19-
public abbrev UsedLocalDecls := FVarIdHashSet
19+
-- This is sometimes used non-linearly, so use a tree set instead of a hash set.
20+
public abbrev UsedLocalDecls := FVarIdSet
2021

2122
/--
2223
Collect set of (let) free variables in a LCNF value.

0 commit comments

Comments
 (0)