-
Notifications
You must be signed in to change notification settings - Fork 58
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Segfault when displaying a hole #114
Comments
BTW, commenting out the rewrite before the |
Debugging idris2 gives me the following stack frame when it segfaults:
|
Segfaults in Idris generally mean stack overflow so it seems that something caused an infinite loop in the TTC deserialiser of names. Do you have outdated |
Thanks! |
The only plausible explanation I can come up with for a deeply nested name on reading (it turns out to be (NS [] (NS [] (NS [] ...))) is that there is some corruption in the .ttc file. Maybe something is being written incorrectly... |
OK, so what's the best way to proceed? |
Not calculating the needed space correctly, so sometimes not expanding the buffer enough! This cause buffer data to be corrupted, leading to issues like #114.
I believe I've found the cause of this. I encountered the same problem, but in an easier to reproduce way! There was an allocation error when writing out ttc files. I won't close this until someone (maybe me later) has tested this specific case though. |
Sorry this is a large program. I'm happy to try to cut it down to a minimal example, but I really have no clue where to start. If you have a suggestion, let me know.
Steps to Reproduce
Download segfaulting-frex.zip
Expected Behavior
To display the context and expected type of the hole.
Observed Behavior
The offending hole
zero_preservation
is part of this definition (CMonoids.idr:133
):The text was updated successfully, but these errors were encountered: