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

Update submodules. #1317

Merged
merged 2 commits into from
Jun 7, 2021
Merged

Update submodules. #1317

merged 2 commits into from
Jun 7, 2021

Conversation

brianhuffman
Copy link
Contributor

No description provided.

@brianhuffman brianhuffman requested a review from atomb June 4, 2021 00:41
@RyanGlScott
Copy link
Contributor

The next cryptol commits involve GaloisInc/cryptol#1207, which will require some changes to saw-remote-api to accommodate. When you get to that point, I have a branch here which makes the necessary changes.

@RyanGlScott
Copy link
Contributor

Is the test failure in cryptol-saw-core-tc-test expected?

Type error when checking "sort"
Inferred type
  sort 1
Not a subtype of expected type
  sort 0
For term
  (a' : sort 0)
-> (n' : Cryptol.Num)
-> (a'
    -> a'
    -> Prelude.Bool)
-> Cryptol.seq n' a'
-> Cryptol.seq n' a'

@brianhuffman
Copy link
Contributor Author

No, that test failure was not expected. I suspect cryptol-saw-core might have an issue with universe levels when translating cryptol functions that use polymorphic recursion. I'll look into it.

@brianhuffman
Copy link
Contributor Author

Well, it actually has nothing to do with polymorphic recursion, but rather with class dictionary types. For some reason Eq and Cmp class dictionaries are declared to be in sort 1 rather than sort 0, and this is the root of the problem. I might need to open a separate ticket for this.

@brianhuffman
Copy link
Contributor Author

Actually, it looks like it's not the dictionary types either. I'll put further discussion on a new ticket thread.

@brianhuffman brianhuffman added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Jun 5, 2021
Copy link
Contributor

@atomb atomb left a comment

Choose a reason for hiding this comment

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

Now that #1318 is fixed, I see no reason not to merge this.

@mergify mergify bot merged commit e5ed6d0 into master Jun 7, 2021
@mergify mergify bot deleted the update-deps branch June 7, 2021 17:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants