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

Adapt to changes from GaloisInc/cryptol#1751, GaloisInc/cryptol#1526, and friends #2174

Merged
merged 3 commits into from
Jan 24, 2025

Conversation

RyanGlScott
Copy link
Contributor

@RyanGlScott RyanGlScott commented Jan 9, 2025

GaloisInc/cryptol#1751 removed the width field from word values, which requires mechanical changes on the cryptol-saw-core side to make it build. This bumps the cryptol submodule and makes the corresponding code changes.

GaloisInc/cryptol#1526 requires updating the freeze files used in the CI files to make them able to download simple-smt-0.9.8.

@RyanGlScott
Copy link
Contributor Author

I've confirmed that things break once the cryptol submodule is bumped to include GaloisInc/cryptol#1526. @glguy, do you have any ideas on what might be causing panics like this one?

  test_unint_extcore:                  [12:56:43.119] Loading file "/home/runner/work/saw-script/saw-script/intTests/test_unint_extcore/test_unint.saw"
[12:56:43.148] You have encountered a bug in Cryptol's implementation.
*** Please create an issue at https://github.com/GaloisInc/cryptol/issues

%< --------------------------------------------------- 
  Revision:  09853251186d4590f3b093dbdf2b324c9a7e6ca0
  Branch:    HEAD
  Location:  modNameChunksText
  Message:   Cannot get chunks of main module name
CallStack (from HasCallStack):
  panic, called at src/Cryptol/Utils/Panic.hs:21:9 in cryptol-3.2.0.99-inplace:Cryptol.Utils.Panic
  panic, called at src/Cryptol/Utils/Ident.hs:229:33 in cryptol-3.2.0.99-inplace:Cryptol.Utils.Ident
%< ---------------------------------------------------

@glguy
Copy link
Member

glguy commented Jan 21, 2025

@glguy, do you have any ideas on what might be causing panics like this one?

The projects code I inherited had some logic in its to give nicer names to Main modules. I don't know why it was written to assume it wouldn't be called on Main. I'll have to read through the code to work out what it's doing.

GaloisInc/cryptol#1751 removed the width field from word values, which requires
mechanical changes on the `cryptol-saw-core` side to make it build. This bumps
the `cryptol` submodule and makes the corresponding code changes.
…Inc/cryptol#1783, and GaloisInc/cryptol#1791

This is a collection of `cryptol` submodule bumps that is squashed together in
order to ensure that the SAW CI continues to pass with this commit:

* GaloisInc/cryptol#1783 bumps Cryptol's lower version bounds on `simple-smt`
  to `>=0.9.8`, which requires updating SAW's `cabal.GHC-*.config` files
  accordingly.
* GaloisInc/cryptol#1526 is brought along for the ride as part of this bump,
  but this will not pass SAW's integration tests without also including the
  bugfix from GaloisInc/cryptol#1791. As a result, I've also included
  GaloisInc/cryptol#1791.

GaloisInc/cryptol#1791 is latest of the three patchsets, so I have bumped the
`cryptol` submodule to point to the merge commit from that PR.
@RyanGlScott RyanGlScott changed the title Adapt cryptol-saw-core to changes from GaloisInc/cryptol#1751 Adapt cryptol-saw-core to changes from GaloisInc/cryptol#1751, GaloisInc/cryptol#1526, and friends Jan 23, 2025
@RyanGlScott
Copy link
Contributor Author

Thanks to @glguy's heroism, I was able to make the CI pass by including the changes from GaloisInc/cryptol#1791. I've included this and cleaned up the commit history.

This should now be ready for review. Once this lands, I'll base #2173 (which also requires bumping the Cryptol submodule) on top of it.

@RyanGlScott RyanGlScott marked this pull request as ready for review January 23, 2025 22:00
@RyanGlScott RyanGlScott changed the title Adapt cryptol-saw-core to changes from GaloisInc/cryptol#1751, GaloisInc/cryptol#1526, and friends Adapt to changes from GaloisInc/cryptol#1751, GaloisInc/cryptol#1526, and friends Jan 23, 2025
Copy link
Contributor

@sauclovian-g sauclovian-g left a comment

Choose a reason for hiding this comment

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

Surprisingly simple for how hard it blew up before...

(actually n/m, missed that it had to get fixed upstream first)

@RyanGlScott RyanGlScott merged commit fe668de into master Jan 24, 2025
32 of 34 checks passed
@RyanGlScott RyanGlScott deleted the bump-cryptol-1751 branch January 24, 2025 12:45
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.

3 participants