Skip to content
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

Tc errors #964

Merged
merged 6 commits into from
Nov 17, 2020
Merged

Tc errors #964

merged 6 commits into from
Nov 17, 2020

Conversation

yav
Copy link
Member

@yav yav commented Nov 13, 2020

This is work in progress toward fixing #905 and #782

#905 is fixed because we simply don't have TCErrorMessage anymore, it really wasn't adding any useful information
that we can't recover when pretty printing an unsolved constraint.

#782 is improved because unificaiton variables are printed in a normalized form, although internal unique identifiers are still
visible in the printing of quantified variables.

yav added 6 commits November 12, 2020 15:40
This should go some way toward solving #782, although there are still
funny numbers from quantified variables.

Note the tests do not yet work, as the error messages are all different
and I'll change them only when I finalize the new error messages
@yav yav merged commit 608ae96 into master Nov 17, 2020
brianhuffman pushed a commit to GaloisInc/saw-core that referenced this pull request Nov 19, 2020
brianhuffman pushed a commit to GaloisInc/saw-core that referenced this pull request Nov 20, 2020
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Nov 20, 2020
This includes GaloisInc/cryptol#964 as well as GaloisInc/saw-core#104,
which adapts cryptol-saw-core to the changes in cryptol.
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Nov 20, 2020
This includes GaloisInc/cryptol#964 as well as GaloisInc/saw-core#104,
which adapts cryptol-saw-core to the changes in cryptol.
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Nov 20, 2020
brianhuffman pushed a commit to GaloisInc/crucible that referenced this pull request Nov 22, 2020
brianhuffman pushed a commit to GaloisInc/crucible that referenced this pull request Nov 24, 2020
@RyanGlScott RyanGlScott deleted the tc-errors branch March 22, 2024 14:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant