Hs dependency upgrade ghc 9.10.3

.github/workflows/master.yml

@@ -8,14 +8,14 @@ concurrency:
   cancel-in-progress: true
 
 env:
-  ghc_version: "9.6.5"
-  stack_version: "2.15.1"
+  ghc_version: "9.10.3"
+  stack_version: "3.7.1"
   hpack_version: '0.36'
 
 jobs:
   cache-stack:
     name: 'Cache Stack'
-    runs-on: ubuntu-22.04
+    runs-on: ubuntu-24.04
     steps:
       - name: Install prerequisites
         run: |

.github/workflows/release.yml

@@ -5,8 +5,8 @@ on:
       - release
 
 env:
-  ghc_version: "9.6.5"
-  stack_version: "2.15.1"
+  ghc_version: "9.10.3"
+  stack_version: "3.7.1"
   hpack_version: '0.36'
 
 jobs:
@@ -35,7 +35,7 @@ jobs:
   release:
     name: 'Release'
     needs: draft-release
-    runs-on: ubuntu-22.04
+    runs-on: ubuntu-24.04
     steps:
       - name: Check out code
         uses: actions/checkout@v6
@@ -49,7 +49,7 @@ jobs:
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
             substituters = http://cache.nixos.org https://cache.iog.io
-            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= 
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
 
       - name: Install Cachix
         uses: cachix/cachix-action@v17
@@ -73,7 +73,7 @@ jobs:
   ubuntu-package:
     name: 'Build Ubuntu package'
     needs: draft-release
-    runs-on: ubuntu-22.04
+    runs-on: ubuntu-24.04
     steps:
       - name: Check out code
         uses: actions/checkout@v6

.github/workflows/test.yml

@@ -10,14 +10,15 @@ concurrency:
   cancel-in-progress: true
 
 env:
-  ghc_version: "9.6.5"
-  stack_version: "2.15.1"
+  ghc_version: "9.10.3"
+  stack_version: "3.7.1"
   hpack_version: '0.36'
 
 jobs:
   formatting:
     name: 'Formatting and Style'
-    runs-on: ubuntu-22.04
+    needs: nix-integration-early
+    runs-on: ubuntu-24.04
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v6
@@ -33,7 +34,7 @@ jobs:
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
             substituters = http://cache.nixos.org https://cache.iog.io
-            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= 
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
 
       # - name: 'Install Cachix'
       #   uses: cachix/cachix-action@v17
@@ -61,8 +62,8 @@ jobs:
       fail-fast: false
       matrix:
         include:
-          - runner: ubuntu-22.04
-            os: ubuntu-22.04
+          - runner: ubuntu-24.04
+            os: ubuntu-24.04
             nix: x86_64-linux
           - runner: self-macos-latest
             os: self-macos-latest
@@ -89,7 +90,7 @@ jobs:
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
             substituters = http://cache.nixos.org https://cache.iog.io
-            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= 
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
 
       # - name: 'Install Cachix'
       #   if: ${{ !startsWith(matrix.os, 'self') }}
@@ -99,14 +100,15 @@ jobs:
 
       - name: Build
         run: GC_DONT_GC=1 nix build .#kore-exec .#kore-rpc-booster
-        
+
       - name: Test
         run: GC_DONT_GC=1 nix develop .#cabal --command bash -c "hpack ./booster && hpack dev-tools && cabal update && cabal build all && cabal test --enable-tests --test-show-details=direct kore-test unit-tests"
 
   nix-integration:
     name: 'Nix / Integration'
     needs: formatting
     runs-on: [self-hosted, linux, normal]
+    timeout-minutes: 120
     steps:
       - name: Check out code
         uses: actions/checkout@v6
@@ -122,7 +124,7 @@ jobs:
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
             substituters = http://cache.nixos.org https://cache.iog.io
-            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= 
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
 
       # - name: Install Cachix
       #   uses: cachix/cachix-action@v17
@@ -166,17 +168,84 @@ jobs:
         if: ${{ (steps.changes.outputs.kore == 'true' || steps.changes.outputs.kore_rpc_types == 'true' || steps.changes.outputs.kore_tests == 'true' || steps.changes.outputs.project == 'true') }}
         run: |
           GC_DONT_GC=1 nix develop github:runtimeverification/k/v$(cat deps/k_release)#kore-integration-tests \
-                --override-input haskell-backend . --update-input haskell-backend \
+                --override-input haskell-backend . \
+                --override-input haskell-backend/nixpkgs \
+                "github:NixOS/nixpkgs/$(nix eval --raw --impure --expr '(builtins.getFlake ("git+file://" + toString ./. + "?shallow=1")).inputs.nixpkgs.rev')" \
+                --command bash -c "cd test && make -j2 --output-sync test"
+
+nix-integration-early:
+    name: 'Nix / Integration (early)'
+    runs-on: [self-hosted, linux, normal]
+    timeout-minutes: 120
+    steps:
+      - name: Check out code
+        uses: actions/checkout@v6
+        with:
+          # Check out pull request HEAD instead of merge commit.
+          ref: ${{ github.event.pull_request.head.sha }}
+          submodules: recursive
+
+      - name: Install Nix
+        uses: cachix/install-nix-action@v26
+        with:
+          install_url: https://releases.nixos.org/nix/nix-2.30.1/install
+          extra_nix_config: |
+            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
+            substituters = http://cache.nixos.org https://cache.iog.io
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
+
+      # - name: Install Cachix
+      #   uses: cachix/cachix-action@v17
+      #   with:
+      #     name: k-framework
+      #     skipPush: true
+
+      - uses: dorny/paths-filter@v4
+        id: changes
+        with:
+          filters: |
+            kore:
+              - 'kore/**'
+            kore_rpc_types:
+              - 'kore-rpc-types/**'
+            booster:
+              - 'booster/**'
+            dev_tools:
+              - 'dev-tools/**'
+            project:
+              - 'stack.yaml*'
+              - 'cabal.project*'
+              - 'Makefile'
+              - '*.mk'
+              - 'flake.nix'
+              - 'deps/*'
+              - scripts/booster-integration-tests.sh
+            kore_tests:
+              - 'test/**'
+
+      - name: Run kore integration tests
+        # do not run this unless anything has changed in a relevant directory
+        if: ${{ (steps.changes.outputs.kore == 'true' || steps.changes.outputs.kore_rpc_types == 'true' || steps.changes.outputs.kore_tests == 'true' || steps.changes.outputs.project == 'true') }}
+        run: |
+          echo nix develop github:runtimeverification/k/v$(cat deps/k_release)#kore-integration-tests \
+                --override-input haskell-backend . \
+                --override-input haskell-backend/nixpkgs \
+                "github:NixOS/nixpkgs/$(nix eval --raw --impure --expr '(builtins.getFlake ("git+file://" + toString ./. + "?shallow=1")).inputs.nixpkgs.rev')" \
+                --command bash -c "cd test && make -j2 --output-sync test"
+          GC_DONT_GC=1 nix develop github:runtimeverification/k/v$(cat deps/k_release)#kore-integration-tests \
+                --override-input haskell-backend . \
+                --override-input haskell-backend/nixpkgs \
+                "github:NixOS/nixpkgs/$(nix eval --raw --impure --expr '(builtins.getFlake ("git+file://" + toString ./. + "?shallow=1")).inputs.nixpkgs.rev')" \
                 --command bash -c "cd test && make -j2 --output-sync test"
 
   stack:
     name: 'Stack / Unit Tests'
     needs: formatting
-    runs-on: ubuntu-22.04
+    runs-on: ubuntu-24.04
     steps:
       - name: Install prerequisites
         run: |
-          sudo apt install --yes debhelper z3 libsecp256k1-dev
+          sudo apt install --yes build-essential debhelper z3 libsecp256k1-dev
 
       - uses: actions/checkout@v6
         with:
@@ -216,12 +285,12 @@ jobs:
         run: stack test kore:kore-test hs-backend-booster:unit-tests
 
       - name: Build Ubuntu package
-        run: ./package/debian/build-package jammy k-haskell-backend.deb
+        run: ./package/debian/build-package noble k-haskell-backend.deb
 
   hlint:
     name: 'HLint'
     needs: formatting
-    runs-on: ubuntu-22.04
+    runs-on: ubuntu-24.04
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v6
@@ -237,7 +306,7 @@ jobs:
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
             substituters = http://cache.nixos.org https://cache.iog.io
-            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= 
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
 
       # - name: 'Install Cachix'
       #   uses: cachix/cachix-action@v17

.hlint.yaml

@@ -16,6 +16,13 @@
 # applied to Kore.Rewrite.SMT.Evaluator.evaluate.
 - ignore: {name: "Redundant evaluate"}
 
+# This warning should apply to Data.NonEmpty.unzip but is mistakenly
+# applied to Data.List.unzip
+- ignore: {name: "Avoid NonEmpty.unzip", within: [Booster.Pattern.Rewrite]}
+
+# This suggestion is invalid since ghc-9.8.4 decided to emit a warning about partial functions
+- ignore: {name: "Use head"}
+
 # Corporate style
 - ignore: {name: "Move brackets to avoid $" }
 - ignore: {name: "Use tuple-section"}
@@ -94,7 +101,11 @@
     name: "Redundant bracket"
     within:
       - Kore.Internal.TermLike.TermLike
-
+# decreases readability
+- ignore: {name: "Functor law"}
+- ignore: {name: "Move filter"}
+- ignore: {name: "Move mapMaybe"}
+- ignore: {name: "Move reverse out"}
 
 # Haskell names match K names
 - ignore:

CLAUDE.md

@@ -113,7 +113,7 @@ cd booster/test/rpc-integration && ./runDirectoryTest.sh test-<name>
 # First, enter the integration nix shell:
 nix develop \
   github:runtimeverification/k/v$(cat deps/k_release)#kore-integration-tests \
-  --override-input haskell-backend . --update-input haskell-backend
+  --override-input haskell-backend .
 
 # Then:
 make test-k          # all integration tests

README.md

@@ -191,7 +191,7 @@ To use this nix shell, execute
 ``` sh
 me@somewhere:haskell-backend$ nix develop \
     github:runtimeverification/k/v$(cat deps/k_release)#kore-integration-tests \
-    --override-input haskell-backend . --update-input haskell-backend
+    --override-input haskell-backend .
 ...
 ...(nix output)
 integration-shell:me@somewhere:haskell-backend$

booster/library/Booster/Builtin/LIST.hs

@@ -85,12 +85,12 @@ listGetHook [KList _ heads mbRest, intArg] =
                     if i < headLen
                         then pure $ Just $ heads !! i -- positive index in range
                         else -- headLen <= i
-                        case mbRest of
-                            Nothing ->
-                                -- index too large
-                                pure Nothing -- actually #Bottom
-                            Just _ ->
-                                pure Nothing
+                            case mbRest of
+                                Nothing ->
+                                    -- index too large
+                                    pure Nothing -- actually #Bottom
+                                Just _ ->
+                                    pure Nothing
                 | otherwise -> -- i < 0, negative index, consider rest
                     case mbRest of
                         Nothing

booster/library/Booster/CLOptions.hs

@@ -387,8 +387,7 @@ parseSMTOptions =
                         ( metavar "SMT_ARG"
                             <> long "smt-arg"
                             <> help
-                                ( "Arguments to be passed to the SMT solver process"
-                                )
+                                ("Arguments to be passed to the SMT solver process")
                         )
                     )
             )

booster/library/Booster/Definition/Ceil.hs

@@ -171,7 +171,9 @@ computeCeil (KMap _ keyVals rest) = do
     symbols <- mkInKeysMap . (.definition.symbols) <$> getConfig
     pure $
         [Left $ Predicate $ mkNeq a b | a <- map fst keyVals, b <- map fst keyVals, a /= b]
-            <> [ Left $ Predicate $ NotBool (mkInKeys symbols a rest') | a <- map fst keyVals, rest' <- maybeToList rest
+            <> [ Left $ Predicate $ NotBool (mkInKeys symbols a rest')
+               | a <- map fst keyVals
+               , rest' <- maybeToList rest
                ]
             <> recArgs
 computeCeil (KList _ heads rest) = concatMapM computeCeil $ heads <> maybe [] (uncurry (:)) rest

booster/library/Booster/GlobalState.hs

@@ -14,10 +14,11 @@ data EquationOptions = EquationOptions
     { maxIterations :: Bound "Iterations"
     , maxRecursion :: Bound "Recursion"
     , maxLocalSteps :: Bound "LocalSteps"
-    -- ^ how many equations may be applied in place at a rewritten
-    -- subterm (per chain of in-place rewrites) before falling back
-    -- to restarting the traversal from the top (0, the default, is
-    -- restart-only evaluation)
+    {- ^ how many equations may be applied in place at a rewritten
+    subterm (per chain of in-place rewrites) before falling back
+    to restarting the traversal from the top (0, the default, is
+    restart-only evaluation)
+    -}
     }
     deriving stock (Show, Eq)
 

booster/library/Booster/JsonRpc.hs

@@ -28,7 +28,7 @@ import Data.Foldable
 import Data.List (singleton)
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
-import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe)
+import Data.Maybe (catMaybes, fromMaybe, isJust, listToMaybe, mapMaybe)
 import Data.Proxy qualified
 import Data.Sequence (Seq)
 import Data.Set qualified as Set
@@ -481,9 +481,9 @@ execStateToKoreJson RpcTypes.ExecuteState{term = t, substitution, predicate} =
         innerSorts = mapMaybe sortOfJson $ KoreJson.term t : subAndPred
         topLevelSort = case innerSorts of
             [] -> KoreJson.SortApp (KoreJson.Id "SortGeneratedTopCell") []
-            xs ->
-                if all (== head xs) (tail xs) -- we know xs is non-empty, hence `head` is safe here
-                    then KoreJson.SortApp (head xs).name []
+            x : xs ->
+                if all (== x) xs
+                    then KoreJson.SortApp x.name []
                     else KoreJson.SortApp (KoreJson.Id "SortGeneratedTopCell") []
      in t
             { KoreJson.term =
@@ -507,8 +507,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
                     , nextStates =
                         Just
                             $ map
-                                ( \(rewritten, ruleMetadata) -> toExecState rewritten (Just ruleMetadata) unsupported
-                                )
+                                (\(rewritten, ruleMetadata) -> toExecState rewritten (Just ruleMetadata) unsupported)
                             $ toList nexts
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -686,10 +685,10 @@ mkLogRewriteTrace
                                             { reason = "Uncertain about a condition in rule"
                                             , _ruleId = Just $ getUniqueId (uniqueId $ Definition.attributes r)
                                             }
-                                    RewriteRemainderPredicate rs _ _ ->
+                                    RewriteRemainderPredicate rules _ _ ->
                                         Failure
                                             { reason = "Uncertain about the remainder after applying a rule"
-                                            , _ruleId = Just $ getUniqueId (uniqueId $ Definition.attributes (head rs))
+                                            , _ruleId = fmap (getUniqueId . uniqueId . Definition.attributes) $ listToMaybe rules
                                             }
                                     DefinednessUnclear r _ undefReasons ->
                                         Failure

booster/library/Booster/LLVM/TH.hs

@@ -169,6 +169,7 @@ cTypeToHs = \case
             C.TyDouble -> ''Foreign.C.CDouble
             C.TyLDouble -> error "TyLDouble unsupported"
             C.TyFloatN _ _ -> error "TyFloatN unsupported"
+            C.TyBFloat16{} -> error "TyBFloat16 unsupported"
         C.TyComplex _floatType -> error "TyComplex unsupported"
         C.TyComp _compTypeRef -> error "TyComp unsupported"
         C.TyEnum _enumTypeRef -> error "TyEnum unsupported"