Skip to content

Initial portion of GHC 9.10 and 9.12 support - #3252

Merged
sauclovian-g merged 8 commits into
masterfrom
ghc-updates-preview
May 28, 2026
Merged

Initial portion of GHC 9.10 and 9.12 support#3252
sauclovian-g merged 8 commits into
masterfrom
ghc-updates-preview

Conversation

@sauclovian-g

Copy link
Copy Markdown
Contributor

It looks like 9.12 support in Crucible is going to take a while, and these bits are mergeable, so let's merge them to reduce the maintenance overhead on the branch with the full support.

This part:

  • fixes a regression of Migrate imports of foldl' for ghc 9.10+ #3146
  • bumps a bunch of submodules whose updates have now been merged
  • bumps SAW's own constraints to allow 9.10 and 9.12
  • fixes a couple warnings that appeared with 9.10
  • updates the CI to a newer cabal to fix a bunch of weird solver errors (same as we saw on the Cryptol branch)

@sauclovian-g

Copy link
Copy Markdown
Contributor Author

something broke and it doesn't make any sense, will investigate

@sauclovian-g

Copy link
Copy Markdown
Contributor Author

ok, it was broken by updating Cryptol, bisecting reveals that it was broken by GaloisInc/cryptol#2040 (expose parameters from functor instantiations).

I rather fear that the real problem is #3000 and the Cryptol changes have made it easier to trigger.

@sauclovian-g

Copy link
Copy Markdown
Contributor Author

Further analysis is going in #3254.

@sauclovian-g
sauclovian-g force-pushed the ghc-updates-preview branch 2 times, most recently from 2f1405f to a655dfc Compare May 21, 2026 00:42
@sauclovian-g

Copy link
Copy Markdown
Contributor Author

Not sure what's going on here, might just be cache corruption

@sauclovian-g
sauclovian-g force-pushed the ghc-updates-preview branch from a655dfc to e641fa9 Compare May 21, 2026 02:16
@sauclovian-g

Copy link
Copy Markdown
Contributor Author

Note that this can't be merged for the moment because it's pointing at an unmerged Cryptol commit.

@sauclovian-g
sauclovian-g force-pushed the ghc-updates-preview branch from e641fa9 to 9059eab Compare May 21, 2026 22:55
@sauclovian-g

sauclovian-g commented May 21, 2026

Copy link
Copy Markdown
Contributor Author

It is no longer pointing at an unmerged Cryptol commit. However, I have no idea what's going on with the coverage generation. Bumping the cache version did not help, so it probably isn't cache corruption, and it's the same GHC version that we were doing it with before. Best bet is that something about the new Cabal version broke it...

@sauclovian-g
sauclovian-g force-pushed the ghc-updates-preview branch from 9059eab to 09ab90e Compare May 22, 2026 19:55
@sauclovian-g

Copy link
Copy Markdown
Contributor Author

Meanwhile for some reason the change I pushed to improve the logging behavior of compute-coverage.sh contained an extra unwanted change that reverted the Cryptol version and broke everything.

@sauclovian-g sauclovian-g linked an issue May 22, 2026 that may be closed by this pull request
@sauclovian-g
sauclovian-g force-pushed the ghc-updates-preview branch from 09ab90e to 2d76b62 Compare May 23, 2026 01:28
@sauclovian-g

Copy link
Copy Markdown
Contributor Author

ok, the speculative change worked. I'm quite confused, but we can run with it...

@sauclovian-g

Copy link
Copy Markdown
Contributor Author

I'm about to force-push this repeatedly to try to (a) figure out what's going on and (b) make sure all the commits in the eventual branch are buildable. I would recommend not trying to follow these and instead just looking at the final diffs.

This should probably be reviewed again anyway as I've made material changes since it was last approved.

@sauclovian-g
sauclovian-g force-pushed the ghc-updates-preview branch from 2d76b62 to 9e986c8 Compare May 26, 2026 18:33
@sauclovian-g

Copy link
Copy Markdown
Contributor Author

I do not understand what's going on with Paths_saw; however, it's probably moot.

It seems the cabal update and the compute-coverage.sh search changes need to get committed together. Which I guess isn't too surprising

This pulls in GHC 9.10 and/or 9.12 support, and also the naming
simplifications in cryptol #2059 that close #3254.

This changes the output of one of the Rocq export tests; update the
reference output.
With current Cryptol we should never see a nonempty "ogFromParam"
field in any module we can actually import, so if we do, fail instead
of adding the parameter name to the module path.
This bumps language-sally and macaw, and also pulls in a new flexdis86
to go with the new macaw.
As requested by a warning in GHC 9.10.
Use explicit progress messages instead of set -x, and explicit error
checks instead of set -e.

The set -x output spews vast amounts of illegible crud because the
paths we're dealing with are in excess of 200 characters each (between
the GH runner's work dir being five layers deep, the top level of
cabal's output being another five under that, and the top of each
hpc tree under that being another six layers...).

Meanwhile, it makes sense to print some of this stuff only on error,
and that requires handling the failure explicitly rather than using
set -e.

It's still going to be an ugly mess, but it seems like that can't be
helped.
@sauclovian-g
sauclovian-g force-pushed the ghc-updates-preview branch from 0a22528 to cb17dea Compare May 26, 2026 22:09
This fixes weird solve errors seen with GHC 9.10 and/or 9.12 test

Also it seems we need to rearrange the mix file search in
compute-coverage.sh again, because something about the Cabal version
change changed hpc's search behavior even though the file layout seems
to be the same as before.
@sauclovian-g

Copy link
Copy Markdown
Contributor Author

ok, this is now actually working and can be re-reviewed

@sauclovian-g
sauclovian-g merged commit 70e2aeb into master May 28, 2026
37 checks passed
@sauclovian-g
sauclovian-g deleted the ghc-updates-preview branch May 28, 2026 18:33
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.

GaloisInc/cryptol#2040 breaks test1892

3 participants