fix(frontend): Process intercalating elements in refactoring #252

Merged

aniva merged 6 commits from frontend/refactor into dev

2025-07-28 16:05:08 -07:00

aniva commented

2025-07-25 16:01:09 -07:00

Owner

This is from PutnamBench's putnam_1997_b1, where we have declarations:

def mystery : Nat -> Nat := sorry
def auxiliary : Nat -> Nat := id
theorem property : ...

where property refers to both mystery and auxiliary.

This is from PutnamBench's `putnam_1997_b1`, where we have declarations: ```lean def mystery : Nat -> Nat := sorry def auxiliary : Nat -> Nat := id theorem property : ... ``` where `property` refers to both `mystery` and `auxiliary`.

aniva added this to the v0.3.5 milestone

2025-07-25 16:01:09 -07:00

aniva added the

part/Frontend

category

feature

labels

2025-07-25 16:01:09 -07:00

aniva self-assigned this

2025-07-25 16:01:09 -07:00

aniva added

and removed

labels

2025-07-25 16:01:14 -07:00

aniva added 1 commit

2025-07-25 16:05:08 -07:00

test(frontend): Add intercalating test case 59a83b85cb

aniva commented

2025-07-25 16:06:37 -07:00

Author

Owner

The current solution is to condense the search target in the head decl's environment. This clearly does not work. Therefore, we need to condense the search target in the last decl's environment.

However, in the future we may need to preserve the decl names instead of just squashing them into a new _composite decl. In this case, I think we should run two concurrent FrontendMs, one is for the input file, and one is for the output file.

The current solution is to condense the search target in the head decl's environment. This clearly does not work. Therefore, we need to condense the search target in the last decl's environment. However, in the future we may need to preserve the decl names instead of just squashing them into a new `_composite` decl. In this case, I think we should run two concurrent `FrontendM`s, one is for the input file, and one is for the output file.

aniva added 1 commit

2025-07-28 14:32:55 -07:00

refactor(frontend): Use dual-monad in RefactorM 5d8d63ec0f

aniva added 1 commit

2025-07-28 14:49:40 -07:00

fix(frontend): Pre-process intercalating commands 2776e881ea

aniva added 1 commit

2025-07-28 14:52:16 -07:00

feat(frontend): Add refactor config (unused) afc00e8c39

aniva added 1 commit

2025-07-28 14:55:39 -07:00

doc(frontend): Doc comments about auxiliaries 157f77f739