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

Bump rustc version #655

Merged
merged 8 commits into from
May 13, 2024
Merged

Bump rustc version #655

merged 8 commits into from
May 13, 2024

Conversation

Nadrieril
Copy link
Collaborator

Some interesting clause-related changes.

Regarding Clause hashing, I think we should either never hash the binder or prevent hashing without a binder; the current middle-ground is error-prone. Consistently ignoring the binder seems fine.

This will make it possible to reuse `Binder::hash()` instead of this
manual hashing.
This doesn't change the hashes, only makes the hashing process easier to
follow.
@W95Psp
Copy link
Collaborator

W95Psp commented May 7, 2024

Cool, thanks, will review on Monday!
There is a to_predicate that happens in the hashing, which calls Binder::dummy, that checks if there are any unbound variable, and this can cause panics :(
So that's why I think we should always hash with binders, but I agree that the current situation is pretty bad! But that's not directly related to that PR :)

@Nadrieril
Copy link
Collaborator Author

With this PR we no longer call to_predicate before hashing Clauses

@W95Psp
Copy link
Collaborator

W95Psp commented May 7, 2024

Ah, I had no time to look at the code, that's great then! That's simplifies things
Might help with #495 then

@Nadrieril
Copy link
Collaborator Author

There are a few other places where we take shortcuts with binders, we'll have to go through these too

Copy link
Collaborator

@W95Psp W95Psp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you! 😀

Seems OK to me, one thing we should settle on is a vocabulary between clauses and predicates: those things now contain exactly the same pieces of information (if I understand correctly)
We should probably map both Predicate and Clause (from rustc) to Clause (from hax), wdyt?

frontend/exporter/src/types/copied.rs Show resolved Hide resolved
frontend/exporter/src/types/copied.rs Show resolved Hide resolved
@W95Psp
Copy link
Collaborator

W95Psp commented May 13, 2024

Let's merge whenever you want @Nadrieril (do you have permissions to press merge though?)

@Nadrieril
Copy link
Collaborator Author

I don't have permissions to merge, you can go ahead

@W95Psp W95Psp added this pull request to the merge queue May 13, 2024
Merged via the queue into hacspec:main with commit 765285c May 13, 2024
12 of 13 checks passed
@Nadrieril Nadrieril deleted the update-rustc branch May 13, 2024 22:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
No open projects
Status: Done
Development

Successfully merging this pull request may close these issues.

2 participants