[ test ] add regression test for codata unification infinite loop #3706
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…inite loop Adds test idris2/reg/reg060 which reproduces the infinite loop when unifying eta-equivalent functions in codata context. The test includes a 5-second timeout to detect the hang.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
description
adds a regression test
idris2/reg/reg060that reproduces the infinite loop from #3705 when unifying codata with eta-equivalent functions.note: this test currently fails/times out. it documents the issue and will pass once #3705 is fixed.
test details
idris2/reg/reg060reproduces the exact issue from infinite loop when unifying codata with eta-equivalent functions #3705run the test:
make test only=idris2/reg/reg060Self-check
CONTRIBUTING.mdand I've updated
CONTRIBUTORS.mdwith my name.