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

Import both public and private Cryptol symbols #1020

Merged
merged 4 commits into from
Jan 21, 2021
Merged

Import both public and private Cryptol symbols #1020

merged 4 commits into from
Jan 21, 2021

Conversation

atomb
Copy link
Contributor

@atomb atomb commented Jan 19, 2021

It doesn't make sense to merge this until after #1018 is merged.

@brianhuffman
Copy link
Contributor

@atomb It looks like you need to bump the saw-core submodule to include GaloisInc/saw-core#120.

@atomb
Copy link
Contributor Author

atomb commented Jan 20, 2021

Oops. Yep, I do.

@atomb
Copy link
Contributor Author

atomb commented Jan 20, 2021

Ah, and I need to update the servers, too.

@brianhuffman
Copy link
Contributor

brianhuffman commented Jan 21, 2021

It looks like your submodule bump includes not only GaloisInc/saw-core#120, but also the unrelated PR GaloisInc/saw-core#118. It turns out that 118 causes a performance regression in the saw-core typechecker, which is fixed by the yet-to-be-merged PR GaloisInc/saw-core#127.

To avoid the performance regression in saw-script master, I'd recommend bumping the saw-core submodule again to include GaloisInc/saw-core#127 (once it's merged, of course) before merging this PR. (Alternatively, you could un-bump saw-core to include only 120.)

@atomb
Copy link
Contributor Author

atomb commented Jan 21, 2021

Thanks for the heads-up @brianhuffman. In the interest of keeping saw-script aligned with the latest submodules whenever possible, I'll wait until GaloisInc/saw-core#127 is merged.

@brianhuffman
Copy link
Contributor

It's already merged, so go ahead and do the further submodule bump.

@brianhuffman
Copy link
Contributor

I just marked this as "next-to-merge" because I have some other changes that are blocked on this PR. Let's get this one done.

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.

2 participants