diff --git a/.github/workflows/master.yml b/.github/workflows/master.yml index 5731a2521d..dd38ae48c4 100644 --- a/.github/workflows/master.yml +++ b/.github/workflows/master.yml @@ -8,7 +8,7 @@ concurrency: cancel-in-progress: true env: - ghc_version: "9.6.5" + ghc_version: "9.8.4" stack_version: "2.15.1" hpack_version: '0.36' diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 36c2a31176..5ff73056c7 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -5,7 +5,7 @@ on: - release env: - ghc_version: "9.6.5" + ghc_version: "9.8.4" stack_version: "2.15.1" hpack_version: '0.36' diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 6214395bc1..e97446de43 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -10,7 +10,7 @@ concurrency: cancel-in-progress: true env: - ghc_version: "9.6.5" + ghc_version: "9.8.4" stack_version: "2.15.1" hpack_version: '0.36' @@ -118,6 +118,16 @@ jobs: - 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" + - name: 'DEBUG MacOS build error' + if: ${{ contains(matrix.os, 'macos') }} + run: | + ls result/bin + for file in result/bin/*; do + echo $file; + strings $file | grep -e "/nix/store" + done + + nix-integration: name: 'Nix / Integration' needs: formatting diff --git a/.hlint.yaml b/.hlint.yaml index 0fec3816f8..dba5c20e29 100644 --- a/.hlint.yaml +++ b/.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,6 +101,10 @@ name: "Redundant bracket" within: - Kore.Internal.TermLike.TermLike +# decreases readability +- ignore: {name: "Functor law"} +- ignore: {name: "Move filter"} +- ignore: {name: "Move mapMaybe"} # Haskell names match K names diff --git a/booster/library/Booster/Builtin/LIST.hs b/booster/library/Booster/Builtin/LIST.hs index 2f67395e95..b4176f0e18 100644 --- a/booster/library/Booster/Builtin/LIST.hs +++ b/booster/library/Booster/Builtin/LIST.hs @@ -44,12 +44,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 diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 0b1a2102f4..0690ffef17 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -27,7 +27,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 @@ -469,9 +469,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 = @@ -667,10 +667,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 diff --git a/booster/library/Booster/LLVM/TH.hs b/booster/library/Booster/LLVM/TH.hs index 3aaa9c5302..5591655bc2 100644 --- a/booster/library/Booster/LLVM/TH.hs +++ b/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" diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 6bb043ce73..7d9eb6ae82 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -229,12 +229,13 @@ pushRecursion t = eqState $ do popRecursion :: LoggerMIO io => EquationT io () popRecursion = do s <- getState - if null s.recursionStack - then do + case s.recursionStack of + [] -> do withContext CtxAbort $ logMessage ("Trying to pop an empty recursion stack" :: Text) throw $ InternalError "Trying to pop an empty recursion stack" - else eqState $ put s{recursionStack = tail s.recursionStack} + _hd : rest -> + eqState $ put s{recursionStack = rest} toCache :: LoggerMIO io => CacheTag -> Term -> Term -> EquationT io () toCache LLVM orig result = eqState . modify $ diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs index 5b884377b4..955fce7540 100644 --- a/booster/library/Booster/Pattern/Implies.hs +++ b/booster/library/Booster/Pattern/Implies.hs @@ -130,7 +130,6 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = then -- we are being conservative here for now and returning an error. -- since we have already simplified the LHS, we may want to eventually return implise, but the condition -- will contain the remainder as an equality contraint, predicating the implication on that equality being true. - pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $ "match remainder: " <> renderDefault @@ -155,7 +154,6 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = (externaliseExistTerm existsR patR.term) subst else -- FIXME This is incomplete because patL.constraints are not assumed in the check. - ApplyEquations.evaluateConstraints def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case (Right newPreds, _) -> if all (== Predicate TrueBool) newPreds diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index b85985f7eb..8ee0035d6e 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -399,7 +399,8 @@ matchSymbolAplications then failWith (DifferentSymbols (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2)) - else addIndeterminate (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2) + else + addIndeterminate (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2) | length args1 /= length args2 = failWith $ ArgLengthsDiffer (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2) diff --git a/booster/library/Booster/SMT/Translate.hs b/booster/library/Booster/SMT/Translate.hs index dd721d8357..6083e9a7d7 100644 --- a/booster/library/Booster/SMT/Translate.hs +++ b/booster/library/Booster/SMT/Translate.hs @@ -27,7 +27,7 @@ import Data.Char (isDigit) import Data.Coerce (coerce) import Data.Map (Map) import Data.Map qualified as Map -import Data.Maybe (catMaybes, fromMaybe, mapMaybe) +import Data.Maybe (catMaybes, fromMaybe, listToMaybe, mapMaybe) import Data.Set qualified as Set import Data.Text (Text, pack) import Prettyprinter (pretty) @@ -205,11 +205,10 @@ equationToSMTLemma equation | (t, v) <- Map.toList m ] lemmaId = - head $ + fromMaybe "Unknown location" . listToMaybe $ catMaybes [ fmap Pretty.pretty equation.attributes.ruleLabel , fmap Pretty.pretty equation.attributes.location - , Just "Unknown location" ] -- free variables (not created by abstraction during -- translation) are all-quantified on the outside diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index 56400defaa..4a25c492ce 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -488,7 +488,7 @@ mkSubstitution initialSubst = Map.fromListWith (<>) [(v, [t]) | SubstitutionPred v t <- initialSubst] equations = [Internal.mkEq v t | (v, ts) <- Map.assocs duplicates, t <- ts] - in execState breakCycles (Map.map head substMap, equations) + in execState breakCycles (Map.map (!! 0) substMap, equations) where breakCycles :: State (Map Internal.Variable Internal.Term, [Internal.Predicate]) () breakCycles = do @@ -734,8 +734,10 @@ isTermM pat = case pat of Syntax.KJNot{} -> pure False Syntax.KJAnd{patterns} -> do terms <- mapM isTermM patterns - when (length (nub terms) /= 1) $ throwE (InconsistentPattern pat) - pure $ head terms + case nub terms of + [] -> throwE (InconsistentPattern pat) -- empty and not allowed + [x] -> pure x + _more -> throwE (InconsistentPattern pat) Syntax.KJOr{} -> pure False Syntax.KJImplies{} -> pure False Syntax.KJIff{} -> pure False diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs index 4031315d62..f737c2814a 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -339,9 +339,11 @@ addModule things `mappedBy` getKey = let sorted :: [[a]] sorted = groupBy ((==) `on` getKey) $ sortOn getKey things - (good, dups) = partition (null . tail) sorted + isGood [_] = True + isGood _ = False + (good, dups) = partition isGood sorted in ( Map.fromAscList [(getKey a, a) | [a] <- good] - , [(getKey $ head d, d) | d <- dups] + , [(getKey d', d) | d@(d' : _) <- dups] ) -- if two symbols have the same smtlib attribute, they get renamed @@ -786,9 +788,9 @@ internaliseRulePattern partialDefinition ref maybeVars f t = do unless (null ceilConditions) $ throwE $ DefinitionPatternError ref CeilNotAllowed - unless (null unsupported) $ - throwE $ - DefinitionPatternError ref (NotSupported (head unsupported)) + case unsupported of + [] -> pure () + x : _ -> throwE $ DefinitionPatternError ref (NotSupported x) pure ( Util.modifyVariablesInT f term , map (Util.modifyVariablesInP f) (preds <> Substitution.asEquations substitution) @@ -975,10 +977,9 @@ internaliseCeil partialDef left right sortVars attrs = do -- turn substitution-like predicates back into equations constraints = internalPs.boolPredicates <> Substitution.asEquations internalPs.substitution unsupported = internalPs.unsupported - unless (null unsupported) $ - throwE $ - DefinitionPatternError (sourceRef attrs) $ - NotSupported (head unsupported) + case unsupported of + [] -> pure () + x : _ -> throwE $ DefinitionPatternError (sourceRef attrs) $ NotSupported x pure $ map (Util.modifyVariablesInT (Util.modifyVarName ("Eq#" <>)) . coerce) constraints @@ -1013,9 +1014,11 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att unless (null ceils) $ throwE $ DefinitionPatternError (sourceRef attrs) CeilNotAllowed - unless (null unsupported) $ - throwE $ - DefinitionPatternError (sourceRef attrs) (NotSupported (head unsupported)) + case unsupported of + [] -> pure () + x : _ -> + throwE $ + DefinitionPatternError (sourceRef attrs) (NotSupported x) -- extract argument binders from predicates and inline in to LHS term argPairs <- mapM internaliseArg args let lhs = diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs index 25155aee02..e9a0cafff9 100644 --- a/booster/tools/booster/Proxy.hs +++ b/booster/tools/booster/Proxy.hs @@ -601,12 +601,11 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of , nextStates = Nothing , logs = combineLogs $ res.logs : simplifiedStateLogs : logsOnly } - | length filteredNexts == 1 -> do + | [onlyNext] <- filteredNexts -> do -- all but one next states are bottom, execution should proceed -- Note that we've effectively made a rewrite step here, so we need to -- extract the rule-id information from the result we proceed with - let onlyNext = head filteredNexts - rewriteRuleId = fromMaybe "UNKNOWN" onlyNext.ruleId + let rewriteRuleId = fromMaybe "UNKNOWN" onlyNext.ruleId proxyRewriteStepLogs | Just True <- logSettings.logSuccessfulRewrites = Just . (: []) $ diff --git a/booster/unit-tests/Test/Booster/Syntax/Json.hs b/booster/unit-tests/Test/Booster/Syntax/Json.hs index d056bdc3ed..564edabcd7 100644 --- a/booster/unit-tests/Test/Booster/Syntax/Json.hs +++ b/booster/unit-tests/Test/Booster/Syntax/Json.hs @@ -1,3 +1,6 @@ +-- no head/tail warnings +{-# OPTIONS_GHC -Wno-x-partial #-} + module Test.Booster.Syntax.Json ( -- Tasty wrappers test_prettyPattern, diff --git a/cabal.project b/cabal.project index 5be4459aad..1b6987ccc6 100644 --- a/cabal.project +++ b/cabal.project @@ -8,17 +8,10 @@ package * ghc-options: -fhide-source-paths -haddock package kore - ghc-options: -Wall -Werror + ghc-options: -Wall -Werror -Wno-x-partial profiling-detail: exported-functions source-repository-package type: git - location: https://github.com/goodlyrottenapple/tasty-test-reporter.git - tag: b704130545aa3925a8487bd3e92f1dd5ce0512e2 - -source-repository-package - type: git - location: https://github.com/goodlyrottenapple/profiteur.git - tag: 7b30bbe6b2a6b72a5b4896f3a0eed5587a5bf465 - -constraints: profiteur +embed-data-files \ No newline at end of file + location: https://github.com/jberthold/tasty-test-reporter.git + tag: 3abbfa942553f0986393af44eda0cb69bcaba6ad diff --git a/cabal.project.freeze b/cabal.project.freeze index 2c1bf4233f..c6e5123e3b 100644 --- a/cabal.project.freeze +++ b/cabal.project.freeze @@ -6,175 +6,221 @@ constraints: any.Cabal ==3.10.3.0, any.OneTuple ==0.4.2, any.Only ==0.1, any.QuickCheck ==2.14.3, + QuickCheck -old-random +templatehaskell, any.StateVar ==1.2.2, any.adjunctions ==4.4.2, - any.aeson ==2.1.2.1, + any.aeson ==2.2.3.0, + aeson +ordered-keymap, any.aeson-pretty ==0.8.10, - any.ansi-terminal ==1.0.2, - any.ansi-terminal-types ==0.11.5, - any.array ==0.5.6.0, + aeson-pretty -lib-only, + any.ansi-terminal ==1.1.2, + ansi-terminal -example, + any.ansi-terminal-types ==1.1, + any.array ==0.5.8.0, any.assoc ==1.1.1, + assoc -tagged, any.async ==2.2.5, + async -bench, any.attoparsec ==0.14.4, - any.auto-update ==0.1.6, - any.barbies ==2.0.5.0, - any.base ==4.18.2.1, + attoparsec -developer, + any.attoparsec-aeson ==2.2.2.0, + any.auto-update ==0.2.6, + any.barbies ==2.1.1.0, + any.base ==4.19.2.0, any.base-compat ==0.13.1, - any.base-compat-batteries ==0.13.1, - any.base-orphans ==0.9.2, + any.base-orphans ==0.9.3, any.base16 ==1.0, any.basement ==0.0.16, any.bifunctors ==5.6.2, + bifunctors +tagged, any.binary ==0.8.9.1, any.bitvec ==1.1.5.0, + bitvec +simd, any.blaze-builder ==0.4.2.3, any.blaze-html ==0.9.2.0, any.blaze-markup ==0.8.3.0, any.blaze-textual ==0.2.3.1, + blaze-textual -developer -integer-simple +native, any.boring ==0.2.2, - any.bytebuild ==0.3.16.2, - any.byteslice ==0.2.13.2, + boring +tagged, + any.bytebuild ==0.3.16.3, + bytebuild -checked, + any.byteslice ==0.2.14.0, + byteslice +avoid-rawmemchr, any.bytesmith ==0.3.11.1, - any.bytestring ==0.11.5.3, + any.bytestring ==0.12.1.0, any.bz2 ==1.0.1.2, - any.cabal-doctest ==1.0.10, + bz2 -cross +with-bzlib, + any.c2hs ==0.28.8, + c2hs +base3 -regression, + any.cabal-doctest ==1.0.11, any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, any.casing ==0.1.4.1, any.cereal ==0.5.8.3, + cereal -bytestring-builder, any.cereal-conduit ==0.8.0, - any.chronos ==1.1.6.1, + any.character-ps ==0.1, + any.chronos ==1.1.6.2, any.clock ==0.8.4, - any.co-log ==0.6.1.0, - any.co-log-core ==0.3.2.2, + clock -llvm, + any.cmdargs ==0.10.22, + cmdargs +quotation -testprog, + any.co-log ==0.6.1.1, + co-log -tutorial, + any.co-log-core ==0.3.2.4, any.colour ==2.3.6, - any.comonad ==5.0.8, + any.comonad ==5.0.9, + comonad +containers +distributive +indexed-traversable, any.concurrent-output ==1.10.21, - any.conduit ==1.3.5, - any.conduit-extra ==1.3.6, + any.conduit ==1.3.6, + any.conduit-extra ==1.3.7, any.constraints ==0.14.2, - any.constraints-extras ==0.4.0.0, - any.containers ==0.6.7, + any.constraints-extras ==0.4.0.2, + constraints-extras +build-readme, + any.containers ==0.6.8, any.contiguous ==0.6.4.2, any.contravariant ==1.5.5, + contravariant +semigroups +statevar +tagged, any.cryptonite ==0.30, - any.data-default ==0.7.1.1, - any.data-default-class ==0.1.2.0, - any.data-default-instances-containers ==0.0.1, - any.data-default-instances-dlist ==0.0.1, - any.data-default-instances-old-locale ==0.0.1, - any.data-fix ==0.3.3, + cryptonite -check_alignment +integer-gmp -old_toolchain_inliner +support_aesni +support_deepseq -support_pclmuldq +support_rdrand -support_sse +use_target_attributes, + any.data-default ==0.7.1.3, + any.data-default-class ==0.1.2.2, + any.data-default-instances-containers ==0.1.0.3, + any.data-default-instances-dlist ==0.0.1.2, + any.data-default-instances-old-locale ==0.0.1.2, + any.data-fix ==0.3.4, any.decision-diagrams ==0.2.0.0, - any.deepseq ==1.4.8.1, + any.deepseq ==1.5.1.0, any.dependent-map ==0.4.0.0, any.dependent-sum ==0.7.2.0, - any.deriving-aeson ==0.2.9, + any.deriving-aeson ==0.2.10, any.direct-sqlite ==2.3.29, - any.directory ==1.3.8.4, + direct-sqlite +dbstat +fulltextsearch +haveusleep +json1 -mathfunctions -systemlib +urifilenames, + any.directory ==1.3.8.5, any.distributive ==0.6.2.1, + distributive +semigroups +tagged, any.dlist ==1.0, + dlist -werror, any.easy-file ==0.2.5, - any.entropy ==0.4.1.10, + any.entropy ==0.4.1.11, + entropy -donotgetentropy, any.erf ==2.0.0.0, any.errors ==2.3.0, any.exceptions ==0.10.7, any.extra ==1.7.16, - any.fast-logger ==3.2.3, - any.fgl ==5.8.2.0, - any.file-embed ==0.0.11.2, - any.filepath ==1.4.300.1, + any.fast-logger ==3.2.5, + any.fgl ==5.8.3.0, + fgl +containers042, + any.filepath ==1.4.301.0, any.free ==5.2, any.generic-lens ==2.2.2.0, any.generic-lens-core ==2.2.1.0, any.generically ==0.1.1, - any.generics-sop ==0.5.1.3, - any.ghc-boot-th ==9.6.5, + any.generics-sop ==0.5.1.4, + any.ghc-boot-th ==9.8.4, any.ghc-compact ==0.1.0.0, - any.ghc-events ==0.19.0.1, - any.ghc-prim ==0.10.0, - any.ghc-prof ==1.4.1.12, + any.ghc-events ==0.20.0.0, + any.ghc-prim ==0.11.0, any.ghc-trace-events ==0.1.2.9, any.gitrev ==1.3.1, any.graphviz ==2999.20.2.0, - any.hashable ==1.4.2.0, + graphviz -test-parsing, + any.hashable ==1.4.7.0, + hashable -arch-native +integer-gmp -random-initial-seed, any.hashtables ==1.3.1, + hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, any.haskeline ==0.8.2.1, - any.haskell-lexer ==1.1.1, + any.haskell-lexer ==1.1.2, any.haskell-src-exts ==1.23.1, - any.haskell-src-meta ==0.8.14, - any.hedgehog ==1.4, + any.haskell-src-meta ==0.8.15, + any.hedgehog ==1.5, any.hpp ==0.6.5, any.hsc2hs ==0.68.10, hsc2hs -in-ghc-tree, - any.hspec ==2.11.8, - any.hspec-api ==2.11.8, - any.hspec-core ==2.11.8, - any.hspec-discover ==2.11.8, + any.hspec ==2.11.10, + any.hspec-api ==2.11.10, + any.hspec-core ==2.11.10, + any.hspec-discover ==2.11.10, any.hspec-expectations ==0.8.4, - any.hspec-hedgehog ==0.1.1.0, + any.hspec-hedgehog ==0.3.0.0, any.indexed-profunctors ==0.1.1.1, any.indexed-traversable ==0.1.4, any.indexed-traversable-instances ==0.1.2, + any.integer-conversion ==0.1.1, any.integer-gmp ==1.1, - any.integer-logarithms ==1.0.3.1, - any.intern ==0.9.5, - any.invariant ==0.6.3, - any.js-jquery ==3.3.1, - any.json-rpc ==1.0.4, - any.junit-xml ==0.1.0.3, + any.integer-logarithms ==1.0.4, + integer-logarithms -check-bounds +integer-gmp, + any.intern ==0.9.6, + any.invariant ==0.6.4, + any.json-rpc ==1.1.1, + any.junit-xml ==0.1.0.4, any.kan-extensions ==5.2.6, kore +threaded, - any.language-c ==0.9.3, - any.lens ==5.2.3, + any.language-c ==0.10.0, + language-c +iecfpextension +usebytestrings, + any.lens ==5.3.3, + lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, any.libyaml ==0.1.4, + libyaml -no-unicode -system-libyaml, any.libyaml-clib ==0.2.5, - any.lifted-async ==0.10.2.5, + any.lifted-async ==0.10.2.7, any.lifted-base ==0.2.3.12, - any.logict ==0.8.1.0, + any.logict ==0.8.2.0, any.loop ==0.3.0, any.math-functions ==0.3.4.4, + math-functions +system-erf +system-expm1, any.matrix ==0.3.6.3, - any.megaparsec ==9.5.0, + any.megaparsec ==9.6.1, + megaparsec -dev, any.memory ==0.18.0, + memory +support_bytestring +support_deepseq, any.mmorph ==1.2.0, any.monad-control ==1.0.3.1, - any.monad-logger ==0.3.40, + any.monad-logger ==0.3.41, + monad-logger +template_haskell, any.monad-loops ==0.4.3, + monad-loops +base4, any.monad-validate ==1.3.0.0, - any.mono-traversable ==1.0.17.0, + any.mono-traversable ==1.0.21.0, any.mtl ==2.3.1, any.multiset ==0.3.4.3, - any.mwc-random ==0.15.0.2, - any.natural-arithmetic ==0.1.4.0, - any.network ==3.1.4.0, - any.network-run ==0.2.8, + any.mwc-random ==0.15.2.0, + mwc-random -benchpapi, + any.natural-arithmetic ==0.2.1.0, + any.network ==3.2.7.0, + network -devel, + any.network-run ==0.4.3, + any.network-uri ==2.6.4.2, any.old-locale ==1.0.0.7, any.old-time ==1.1.0.4, any.optparse-applicative ==0.18.1.0, - any.os-string ==2.0.2.2, + optparse-applicative +process, + any.os-string ==2.0.7, any.parallel ==3.2.2.0, - any.parsec ==3.1.16.1, + any.parsec ==3.1.17.0, any.parser-combinators ==1.3.0, + parser-combinators -dev, any.polyparse ==1.13, any.pqueue ==1.5.0.0, any.pretty ==1.1.3.6, any.pretty-show ==1.10, any.prettyprinter ==1.7.1, + prettyprinter -buildreadme +text, any.prettyprinter-ansi-terminal ==1.1.3, - any.primitive ==0.8.0.0, + any.primitive ==0.9.0.0, any.primitive-addr ==0.1.0.3, any.primitive-offset ==0.2.0.1, any.primitive-unlifted ==2.1.0.0, - any.process ==1.6.19.0, - any.profiteur ==0.4.7.0, - profiteur +embed-data-files, + any.process ==1.6.25.0, any.profunctors ==5.6.2, - any.quickcheck-instances ==0.3.30, - quickcheck-instances -bytestring-builder, + any.quickcheck-instances ==0.3.32, any.quickcheck-io ==0.2.0, - any.random ==1.2.1.2, - any.recursion-schemes ==5.2.2.5, - any.reflection ==2.1.8, + any.random ==1.2.1.3, + any.recursion-schemes ==5.2.3, + recursion-schemes +template-haskell, + any.reflection ==2.1.9, + reflection -slow +template-haskell, any.regex-base ==0.94.0.2, any.regex-pcre-builtin ==0.95.2.3.8.44, any.resourcet ==1.3.0, @@ -182,82 +228,102 @@ constraints: any.Cabal ==3.10.3.0, any.run-st ==0.1.3.3, any.safe ==0.3.21, any.safe-exceptions ==0.1.7.4, - any.scientific ==0.3.7.0, - any.secp256k1-haskell ==1.1.0, + any.scientific ==0.3.8.0, + scientific -integer-simple, + any.secp256k1-haskell ==1.4.2, any.semialign ==1.3.1, + semialign +semigroupoids, any.semigroupoids ==6.0.1, + semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, any.semigroups ==0.20, + semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, any.smallcheck ==1.2.1.1, any.smtlib-backends ==0.3, any.smtlib-backends-process ==0.3, any.some ==1.0.6, + some +newtype-unsafe, any.sop-core ==0.5.0.2, any.split ==0.2.5, - any.splitmix ==0.1.0.5, + any.splitmix ==0.1.1, + splitmix -optimised-mixer, any.sqlite-simple ==0.4.19.0, - any.stm ==2.5.1.0, + any.stm ==2.5.3.1, any.stm-chans ==3.0.0.9, any.stm-conduit ==4.0.1, - any.streaming-commons ==0.2.2.6, - any.streams ==3.3.2, - any.strict ==0.5, + any.streaming-commons ==0.2.3.0, + streaming-commons -use-bytestring-builder, + any.streams ==3.3.3, + any.strict ==0.5.1, any.string-conversions ==0.4.0.1, any.syb ==0.7.2.4, any.tagged ==0.8.8, + tagged +deepseq +transformers, any.tar ==0.6.3.0, - any.tasty ==1.4.3, + any.tasty ==1.5.3, tasty +unix, - any.tasty-discover ==5.0.0, + any.tasty-discover ==5.0.1, + tasty-discover -dev, any.tasty-golden ==2.3.5, tasty-golden -build-example, any.tasty-hedgehog ==1.4.0.2, any.tasty-hspec ==1.2.0.4, - any.tasty-hunit ==0.10.1, - any.tasty-quickcheck ==0.10.2, + any.tasty-hunit ==0.10.2, + any.tasty-quickcheck ==0.11, any.tasty-smallcheck ==0.8.2, any.tasty-test-reporter ==0.1.1.4, - any.template-haskell ==2.20.0.0, + any.template-haskell ==2.21.0.0, any.temporary ==1.3, any.terminal-size ==0.3.4, any.terminfo ==0.4.1.6, - any.text ==2.0.2, + any.text ==2.1.1, + any.text-iso8601 ==0.1.1, any.text-short ==0.1.6, + text-short -asserts, any.tf-random ==0.5, - any.th-abstraction ==0.5.0.0, - any.th-compat ==0.1.5, - any.th-expand-syns ==0.4.11.0, - any.th-lift ==0.8.4, - any.th-orphans ==0.13.14, + any.th-abstraction ==0.7.1.0, + any.th-compat ==0.1.6, + any.th-expand-syns ==0.4.12.0, + any.th-lift ==0.8.6, + any.th-orphans ==0.13.16, any.th-reify-many ==0.1.10, any.these ==1.2.1, any.time ==1.12.2, - any.time-compat ==1.9.6.1, - any.time-manager ==0.0.1, + any.time-compat ==1.9.7, + any.time-manager ==0.2.2, any.torsor ==0.1.0.1, any.transformers ==0.6.1.0, any.transformers-base ==0.4.6, + transformers-base +orphaninstances, any.transformers-compat ==0.7.2, + transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, any.tuples ==0.1.0.0, - any.typed-process ==0.2.11.1, - any.unix ==2.8.4.0, - any.unix-compat ==0.7.1, - any.unix-time ==0.4.12, + any.typed-process ==0.2.12.0, + any.unix ==2.8.6.0, + any.unix-compat ==0.7.3, + any.unix-time ==0.4.16, + any.unlifted ==0.2.2.0, any.unliftio ==0.2.25.0, any.unliftio-core ==0.2.1.0, any.unordered-containers ==0.2.20, + unordered-containers -debug, any.utf8-string ==1.0.2, - any.uuid-types ==1.0.5.1, - any.vector ==0.13.1.0, - any.vector-algorithms ==0.9.0.2, + any.uuid-types ==1.0.6, + any.vector ==0.13.2.0, + vector +boundschecks -internalchecks -unsafechecks -wall, + any.vector-algorithms ==0.9.1.0, + vector-algorithms +bench +boundschecks -internalchecks -llvm -unsafechecks, any.vector-stream ==0.1.0.1, any.void ==0.7.3, + void -safe, any.wide-word ==0.1.6.0, - any.witherable ==0.4.2, + any.witherable ==0.5, any.wl-pprint-annotated ==0.1.0.1, any.wl-pprint-text ==1.2.0.2, - any.xml-conduit ==1.9.1.3, + any.xml-conduit ==1.9.1.4, any.xml-types ==0.3.8, any.yaml ==0.11.11.2, - any.zigzag ==0.0.1.0, - any.zlib ==0.6.3.0 -index-state: hackage.haskell.org 2024-07-22T06:21:59Z + yaml +no-examples +no-exe, + any.zigzag ==0.1.0.0, + any.zlib ==0.7.1.0, + zlib -bundled-c-zlib +non-blocking-ffi +pkg-config +index-state: hackage.haskell.org 2025-02-23T22:52:03Z diff --git a/dev-tools/package.yaml b/dev-tools/package.yaml index cf002942bd..6c2a5579fe 100644 --- a/dev-tools/package.yaml +++ b/dev-tools/package.yaml @@ -121,23 +121,6 @@ executables: - time ghc-options: - -rtsopts - time-profile: - source-dirs: time-profile - main: Main.hs - dependencies: - - aeson - - base - - bytestring - - containers - - directory - - filepath - - kore-rpc-types - - profiteur - - text - - unordered-containers - - vector - ghc-options: - - -rtsopts parsetest-binary: source-dirs: parsetest-binary main: ParsetestBinary.hs diff --git a/dev-tools/process-logs/Main.hs b/dev-tools/process-logs/Main.hs index c20151a0ff..fe7dc53c87 100644 --- a/dev-tools/process-logs/Main.hs +++ b/dev-tools/process-logs/Main.hs @@ -271,11 +271,12 @@ ruleStats = Map.fromListWith (<>) . collect interesting (CLWithId c') = isRuleCtx c' fromCtxSpan :: Seq CLContext -> [LogLine] -> (RuleStats, [LogLine]) - fromCtxSpan prefix ls - | null prefixLines = - error "Should have at least one line with the prefix" -- see above - | otherwise = - (mkOutcome (head prefixLines) (last prefixLines), rest) + fromCtxSpan prefix ls = + case prefixLines of + [] -> + error "Should have at least one line with the prefix" -- see above + hd : _ -> + (mkOutcome hd (last prefixLines), rest) where len = Seq.length prefix diff --git a/flake.lock b/flake.lock index e670a1a22a..1a595de0ef 100644 --- a/flake.lock +++ b/flake.lock @@ -1,6 +1,22 @@ { "nodes": { "nixpkgs": { + "locked": { + "lastModified": 1740383968, + "narHash": "sha256-45S3DqgiWLmKKXloubh4QKvZJUPIpWCcOc3QxRJFUDw=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "410fedb0b2521255efe3ab79010add3580410ee0", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "410fedb0b2521255efe3ab79010add3580410ee0", + "type": "github" + } + }, + "nixpkgs_2": { "locked": { "lastModified": 1716457947, "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", @@ -18,10 +34,7 @@ }, "root": { "inputs": { - "nixpkgs": [ - "rv-utils", - "nixpkgs" - ], + "nixpkgs": "nixpkgs", "rv-utils": "rv-utils", "stacklock2nix": "stacklock2nix", "z3": "z3" @@ -29,14 +42,14 @@ }, "rv-utils": { "inputs": { - "nixpkgs": "nixpkgs" + "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1716459074, - "narHash": "sha256-IpahO+EkWdGl9QP7B2YXfJWpSfghjxgpz4ab47nRJY4=", + "lastModified": 1726497185, + "narHash": "sha256-iN+5eLmDm/rLuIZezS5ZqiW1BtBpwrrM9CPPP7Z5Tog=", "owner": "runtimeverification", "repo": "rv-nix-tools", - "rev": "a65058865cda201de504f5546271b8e997a0be9c", + "rev": "854d4f05ea78547d46e807b414faad64cea10ae4", "type": "github" }, "original": { @@ -47,11 +60,11 @@ }, "stacklock2nix": { "locked": { - "lastModified": 1705051190, - "narHash": "sha256-xgH0gaD3dNtOzZzX3A40hZTiHJP5cIGmifbmfcS2OGI=", + "lastModified": 1740119818, + "narHash": "sha256-j+lGzwLbwQ39l3hfnuconcHPmVjHN0utYT8KhPW1ltM=", "owner": "cdepillabout", "repo": "stacklock2nix", - "rev": "22676dfc45fa1c33899ba1da1a23665172a18ba7", + "rev": "bfef245fe33e62cdd8b1679235c1d0e7b7eed96b", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 2d032b53f2..ca1cc72a7c 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,8 @@ description = "K Kore Language Haskell Backend"; inputs = { rv-utils.url = "github:runtimeverification/rv-nix-tools"; - nixpkgs.follows = "rv-utils/nixpkgs"; + # nixpkgs.follows = "rv-utils/nixpkgs"; + nixpkgs.url = "github:NixOS/nixpkgs/410fedb0b2521255efe3ab79010add3580410ee0"; # FIXME! stacklock2nix.url = "github:cdepillabout/stacklock2nix"; z3 = { url = "github:Z3Prover/z3/z3-4.13.4"; @@ -28,13 +29,12 @@ makeWrapper ${pkg}/bin/${exe} $out/bin/${exe} --prefix PATH : ${pkgs.z3}/bin ''; }; - # This should based on the compiler version from the resolver in stack.yaml. - ghcVersion = pkgs: pkgs.haskell.packages.ghc965; + # This should match the compiler version from the resolver in stack.yaml. + ghcVersion = pkgs: pkgs.haskell.packages.ghc984; in { overlay = final: prev: { haskell-backend = final.stacklock2nix { stackYaml = ./stack.yaml; - # This should based on the compiler version from the resolver in stack.yaml. baseHaskellPkgSet = ghcVersion final; cabal2nixArgsOverrides = args: args // { @@ -46,8 +46,9 @@ }; additionalHaskellPkgSetOverrides = hfinal: hprev: with final.haskell.lib; { + bytebuild = dontCheck hprev.bytebuild; + cborg = dontCheck hprev.cborg; crypton-x509 = dontCheck hprev.crypton-x509; - data-fix = doJailbreak hprev.data-fix; decision-diagrams = dontCheck hprev.decision-diagrams; fgl = dontCheck hprev.fgl; fgl-arbitrary = dontCheck hprev.fgl-arbitrary; @@ -55,12 +56,9 @@ json-rpc = dontCheck hprev.json-rpc; lifted-base = dontCheck hprev.lifted-base; prettyprinter = dontCheck hprev.prettyprinter; - semialign = doJailbreak hprev.semialign; + primitive-unlifted = dontCheck hprev.primitive-unlifted; + serialise = dontCheck hprev.serialise; smtlib-backends-process = dontCheck hprev.smtlib-backends-process; - tar = dontCheck hprev.tar; - text-short = doJailbreak hprev.text-short; - these = doJailbreak hprev.these; - ghc-prof = doJailbreak hprev.ghc-prof; hs-backend-booster = overrideCabal hprev.hs-backend-booster (drv: { doCheck = false; @@ -104,8 +102,8 @@ # this need to be bumped if changing the stack resolver all-cabal-hashes = final.fetchurl { url = - "https://github.com/commercialhaskell/all-cabal-hashes/archive/ce857734d7d4c0fad3f6dda3a4db052836ed4619.tar.gz"; - sha256 = "sha256-Q7Zg32v5ubjVJMQXGiyyMmeFg08jTzVRKC18laiHCPE="; + "https://github.com/commercialhaskell/all-cabal-hashes/archive/7a0542e6f0122602fcc0bdba41dea0febfd2df6d.tar.gz"; + sha256 = "sha256-TIwCyv9+COsTA9YYTnwj2M7jZb5PdisJfWoLjpi7UY0="; }; }; }; @@ -118,7 +116,10 @@ kore = with pkgs; haskell.lib.justStaticExecutables haskell-backend.pkgSet.kore; hs-backend-booster = with pkgs; - haskell.lib.justStaticExecutables haskell-backend.pkgSet.hs-backend-booster; + # FIXME remove after MacOS debugging on CI + haskell.lib.overrideCabal + (haskell.lib.justStaticExecutables haskell-backend.pkgSet.hs-backend-booster) + (drv: { disallowGhcReference = false; }); hs-backend-booster-dev-tools = with pkgs; haskell.lib.justStaticExecutables haskell-backend.pkgSet.hs-backend-booster-dev-tools; in { @@ -158,6 +159,7 @@ pkgs.nix pkgs.z3 pkgs.lsof + pkgs.git ]; shellHook = '' hpack booster && hpack dev-tools diff --git a/kore/kore.cabal b/kore/kore.cabal index 95d877eee4..f81bd5caa5 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -92,7 +92,7 @@ common exe common library -- Dependencies of the library, shared in common with the tests build-depends: adjunctions >=4.4 - build-depends: aeson >=1.4 && <2.2 + build-depends: aeson >=2.2 && <3 build-depends: aeson-pretty == 0.8.10 build-depends: array build-depends: async >=2.2 @@ -123,9 +123,9 @@ common library build-depends: ghc-trace-events >=0.1 build-depends: gitrev >=1.3 build-depends: graphviz >=2999.20 - -- Pin hashable to make sure cabal build uses the one Nix & Stack builds do + -- TODO Pin hashable to make sure cabal build uses the one Nix & Stack builds do -- Also note that hashable-1.4.3.0 DOES NOT WORK! (see #3730) - build-depends: hashable ==1.4.2.0 + build-depends: hashable >1.4.4 build-depends: haskeline ==0.8.* build-depends: ghc-bignum >=1.2 build-depends: json-rpc >=1.0 @@ -167,7 +167,7 @@ common library build-depends: transformers-base build-depends: unordered-containers >=0.2 build-depends: vector >=0.12 - build-depends: witherable ==0.4.* + build-depends: witherable >=0.4 build-depends: yaml >=0.11.5.0 build-depends: zlib >=0.6 build-tool-depends: happy:happy diff --git a/kore/src/Debug.hs b/kore/src/Debug.hs index a52baceb75..4626f851e9 100644 --- a/kore/src/Debug.hs +++ b/kore/src/Debug.hs @@ -223,7 +223,7 @@ debugConstr (SOP.Constructor name) args = where name' = parens needsParens (Pretty.pretty name) where - initial = head name + initial = name !! 0 needsParens = (not . Char.isLetter) initial && initial /= '(' args' = map ($ precConstr) (SOP.hcollapse args) debugConstr (SOP.Infix name _ precInfix) (K x :* K y :* Nil) = diff --git a/kore/src/Kore/BugReport.hs b/kore/src/Kore/BugReport.hs index 596cebf14c..8432de3271 100644 --- a/kore/src/Kore/BugReport.hs +++ b/kore/src/Kore/BugReport.hs @@ -111,7 +111,7 @@ writeBugReportArchive base tar = do Monad.whenM (doesFileExist sessionCommands) $ do - copyFile sessionCommands (base tail sessionCommands) + copyFile sessionCommands (base "sessionCommands") removeFile sessionCommands contents <- listDirectory base let filename = tar <.> "tar" <.> "gz" diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index feb6a84427..a41cbbaed3 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/kore/src/Kore/JsonRpc.hs @@ -541,7 +541,6 @@ respond reqId serverState moduleName runSMT = MVar.putMVar serverState $ if nameAsId then -- the module already exists, but re-adding with name because name-as-id is true - ServerState { serializedModules = Map.insert (coerce name) foundSerModule serializedModules diff --git a/kore/src/Kore/Log/InfoJsonRpcProcessRequest.hs b/kore/src/Kore/Log/InfoJsonRpcProcessRequest.hs index c1c66e29cf..16d4a6bb8d 100644 --- a/kore/src/Kore/Log/InfoJsonRpcProcessRequest.hs +++ b/kore/src/Kore/Log/InfoJsonRpcProcessRequest.hs @@ -19,7 +19,8 @@ import Pretty ( ) import Pretty qualified -data InfoJsonRpcProcessRequest = forall a. +data InfoJsonRpcProcessRequest + = forall a. (Show a, Pretty a, Typeable a) => InfoJsonRpcProcessRequest { requestId :: Id diff --git a/kore/src/Kore/Repl/Interpreter.hs b/kore/src/Kore/Repl/Interpreter.hs index 19ec7fd235..8eea8db6e6 100644 --- a/kore/src/Kore/Repl/Interpreter.hs +++ b/kore/src/Kore/Repl/Interpreter.hs @@ -881,11 +881,14 @@ showPrecBranch maybeNode = do -- "Left n" means continue looping with value being n -- "Right n" means "stop and return n" loopCond gph n - | isNotBranch gph n && isNotRoot gph n = Left $ head (Graph.pre gph n) + | isNotBranch gph n + , (hd : _) <- Graph.pre gph n {- isNotRoot gph n -} = + Left hd | otherwise = Right n isNotBranch gph n = Graph.outdeg gph n <= 1 - isNotRoot gph n = not . null . Graph.pre gph $ n + +-- isNotRoot gph n = not . null . Graph.pre gph $ n -- | Shows the next node(s) for the selected node. showChildren :: diff --git a/kore/src/Kore/Rewrite/Strategy.hs b/kore/src/Kore/Rewrite/Strategy.hs index 147274a16d..cee7ba0da2 100644 --- a/kore/src/Kore/Rewrite/Strategy.hs +++ b/kore/src/Kore/Rewrite/Strategy.hs @@ -432,7 +432,7 @@ history ExecutionGraph{root, graph} = See also: 'runStrategy' -} pickLongest :: ExecutionGraph config rule -> config -pickLongest exeGraph = head $ last $ history exeGraph +pickLongest exeGraph = (last $ history exeGraph) !! 0 -- | Return all 'stuck' configurations, i.e. all leaves of the 'Tree'. pickFinal :: ExecutionGraph config rule -> [config] diff --git a/kore/src/Kore/Simplify/Simplify.hs b/kore/src/Kore/Simplify/Simplify.hs index 45d7445e92..7b0422d629 100644 --- a/kore/src/Kore/Simplify/Simplify.hs +++ b/kore/src/Kore/Simplify/Simplify.hs @@ -456,8 +456,8 @@ It returns the result of simplifying the pattern with builtins and axioms, together with a proof certifying that it was simplified correctly (which is only a placeholder right now). -} -newtype BuiltinAndAxiomSimplifier = - -- TODO (thomas.tuegel): Rename me! +newtype BuiltinAndAxiomSimplifier + = -- TODO (thomas.tuegel): Rename me! BuiltinAndAxiomSimplifier { runBuiltinAndAxiomSimplifier :: TermLike RewritingVariableName -> diff --git a/kore/src/Kore/Syntax/Pattern.hs b/kore/src/Kore/Syntax/Pattern.hs index fd52112d85..d1a10ec14a 100644 --- a/kore/src/Kore/Syntax/Pattern.hs +++ b/kore/src/Kore/Syntax/Pattern.hs @@ -96,7 +96,8 @@ annotations. newtype Pattern (variable :: Type) - (annotation :: Type) = Pattern + (annotation :: Type) + = Pattern {getPattern :: Cofree (PatternF variable) annotation} deriving stock (Show) deriving stock (GHC.Generic) diff --git a/kore/src/Kore/Unification/NewUnifier.hs b/kore/src/Kore/Unification/NewUnifier.hs index be427538f3..4cf48387bb 100644 --- a/kore/src/Kore/Unification/NewUnifier.hs +++ b/kore/src/Kore/Unification/NewUnifier.hs @@ -1186,8 +1186,10 @@ remakeMapTerms _ AcTerm{acElements = [var]} = mkElemVar $ fromJust $ retract var remakeMapTerms tools AcTerm{acElements, acSort} = if fromJust $ isMapSort tools acSort - then Ac.asInternal tools acSort $ NormalizedMap{getNormalizedMap = normalizedAc $ map mkVar acElements} - else Ac.asInternal tools acSort $ NormalizedSet{getNormalizedSet = normalizedAc $ map mkVar acElements} + then + Ac.asInternal tools acSort $ NormalizedMap{getNormalizedMap = normalizedAc $ map mkVar acElements} + else + Ac.asInternal tools acSort $ NormalizedSet{getNormalizedSet = normalizedAc $ map mkVar acElements} where normalizedAc opaque = NormalizedAc{elementsWithVariables = [], concreteElements = HashMap.empty, opaque} diff --git a/kore/src/Kore/Validate/PatternVerifier.hs b/kore/src/Kore/Validate/PatternVerifier.hs index ef532f33ba..8b8c8d00b2 100644 --- a/kore/src/Kore/Validate/PatternVerifier.hs +++ b/kore/src/Kore/Validate/PatternVerifier.hs @@ -238,9 +238,11 @@ internalizeAnd :: internalizeAnd And{andSort, andChildren = [andFirst, andSecond]} = BinaryAnd{andSort, andFirst, andSecond} internalizeAnd And{andSort, andChildren} = - let first = head andChildren - in let second = internalizeAnd And{andSort, andChildren = tail andChildren} - in BinaryAnd{andSort, andFirst = first, andSecond = synthesize (Internal.AndF second)} + case andChildren of + [] -> error "Empty And-node in verified pattern" + first : rest -> + let second = internalizeAnd And{andSort, andChildren = rest} + in BinaryAnd{andSort, andFirst = first, andSecond = synthesize (Internal.AndF second)} internalizeOr :: Or Sort Verified.Pattern -> @@ -248,9 +250,11 @@ internalizeOr :: internalizeOr Or{orSort, orChildren = [orFirst, orSecond]} = BinaryOr{orSort, orFirst, orSecond} internalizeOr Or{orSort, orChildren} = - let first = head orChildren - in let second = internalizeOr Or{orSort, orChildren = tail orChildren} - in BinaryOr{orSort, orFirst = first, orSecond = synthesize (Internal.OrF second)} + case orChildren of + [] -> error "Empty Or-node in verified pattern" + first : rest -> + let second = internalizeOr Or{orSort, orChildren = rest} + in BinaryOr{orSort, orFirst = first, orSecond = synthesize (Internal.OrF second)} verifyAnd :: And Sort (PatternVerifier Verified.Pattern) -> diff --git a/kore/test/Test/Kore/Builtin/Map.hs b/kore/test/Test/Kore/Builtin/Map.hs index 2cfacab9dc..6d14c6c261 100644 --- a/kore/test/Test/Kore/Builtin/Map.hs +++ b/kore/test/Test/Kore/Builtin/Map.hs @@ -328,7 +328,7 @@ test_removeAll = map' <- forAll genMapPattern set <- forAll Test.Set.genSetConcreteIntegerPattern when (set == HashSet.empty) discard - let key = head (HashSet.toList set) + let key = (HashSet.toList set) !! 0 -- not empty, see above diffSet = HashSet.delete key set patSet = mkSet_ set & fromConcrete patDiffSet = mkSet_ diffSet & fromConcrete diff --git a/kore/test/Test/Kore/Repl/Interpreter.hs b/kore/test/Test/Kore/Repl/Interpreter.hs index b85e94fe1b..f39726ffc4 100644 --- a/kore/test/Test/Kore/Repl/Interpreter.hs +++ b/kore/test/Test/Kore/Repl/Interpreter.hs @@ -1,3 +1,6 @@ +-- no head/tail warnings +{-# OPTIONS_GHC -Wno-x-partial #-} + module Test.Kore.Repl.Interpreter ( test_replInterpreter, ) where diff --git a/kore/test/Test/Kore/Syntax/Json.hs b/kore/test/Test/Kore/Syntax/Json.hs index 9dd2c7ea2f..5d4087dacd 100644 --- a/kore/test/Test/Kore/Syntax/Json.hs +++ b/kore/test/Test/Kore/Syntax/Json.hs @@ -1,4 +1,6 @@ {-# LANGUAGE OverloadedStrings #-} +-- no head/tail warnings +{-# OPTIONS_GHC -Wno-x-partial #-} module Test.Kore.Syntax.Json ( -- Tasty wrappers diff --git a/kore/test/Test/Kore/Validate/DefinitionVerifier/PatternVerifier.hs b/kore/test/Test/Kore/Validate/DefinitionVerifier/PatternVerifier.hs index 7f606ded7e..15bfff3249 100644 --- a/kore/test/Test/Kore/Validate/DefinitionVerifier/PatternVerifier.hs +++ b/kore/test/Test/Kore/Validate/DefinitionVerifier/PatternVerifier.hs @@ -1,3 +1,6 @@ +-- no head/tail warnings +{-# OPTIONS_GHC -Wno-x-partial #-} + module Test.Kore.Validate.DefinitionVerifier.PatternVerifier ( test_patternVerifier, test_verifyBinder, diff --git a/scripts/fourmolu.sh b/scripts/fourmolu.sh index 604186aa58..6c1d4fa6a5 100755 --- a/scripts/fourmolu.sh +++ b/scripts/fourmolu.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash set -euxo pipefail -expected_fourmolu_version="0.14.0.0" +expected_fourmolu_version="0.15.0.0" fourmolu=${FOURMOLU:-$(which fourmolu)} || { echo 'No fourmolu!' ; exit 1 ; } fourmolu_version=$(${fourmolu} --version | head -n1) # drop the prefix 'fourmolu ' which is 9 letters long diff --git a/scripts/hlint.sh b/scripts/hlint.sh index fe77694306..0899b4f30e 100755 --- a/scripts/hlint.sh +++ b/scripts/hlint.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash set -euxo pipefail -expected_hlint_version=v3.6.1 +expected_hlint_version=v3.8 hlint=${HLINT:-$(which hlint)} || { echo 'No hlint!' ; exit 1 ; } hlint_version=$(${hlint} --version | head -n1 | cut --field=1 --delimiter=',' | cut --field=2 --delimiter=' ') [[ ${hlint_version} == ${expected_hlint_version} ]] || { echo "Unexpected hlint version, got ${hlint_version}, expected ${expected_hlint_version}" ; exit 1 ; } diff --git a/stack.yaml b/stack.yaml index b42775a83b..e3f295ac98 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,4 +1,4 @@ -resolver: lts-22.23 +resolver: lts-23.9 nix: packages: @@ -14,27 +14,13 @@ packages: # Dependency packages to be pulled from upstream that are not in the resolver extra-deps: - - tar-0.6.3.0 - - hashable-1.4.2.0 - decision-diagrams-0.2.0.0 - smtlib-backends-0.3 - smtlib-backends-process-0.3 - typerep-map-0.6.0.0 - monad-validate-1.3.0.0 - - github: goodlyrottenapple/tasty-test-reporter - commit: b704130545aa3925a8487bd3e92f1dd5ce0512e2 - - github: goodlyrottenapple/profiteur - commit: 7b30bbe6b2a6b72a5b4896f3a0eed5587a5bf465 - - ghc-prof-1.4.1.12@sha256:0146d3324470db81f6ed1d84b445f1d1aadaeb2e4e045876f5cd231a0946b713,2117 - -allow-newer: true - -allow-newer-deps: - - data-fix - - semialign - - text-short - - these - - ghc-prof + - github: jberthold/tasty-test-reporter + commit: 3abbfa942553f0986393af44eda0cb69bcaba6ad ghc-options: "$everything": -haddock diff --git a/stack.yaml.lock b/stack.yaml.lock index 098f216431..80510dd00a 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -1,27 +1,13 @@ # This file was autogenerated by Stack. # You should not edit this file by hand. # For more information, please see the documentation at: -# https://docs.haskellstack.org/en/stable/lock_files +# https://docs.haskellstack.org/en/stable/topics/lock_files packages: - completed: - hackage: tar-0.6.3.0@sha256:e9f151d9999be8953443e730524b2792e9c0a4fb5b1463097fa1a8230870fd8a,4634 + hackage: decision-diagrams-0.2.0.0@sha256:a973d0e448cb4cb409f93b210bf7f968c893a2152c1e2f81b2e9c922f83f9b76,3423 pantry-tree: - sha256: e59e0d0224352033c32356d517f90d4c6a41cee4fa0d386885df146302d1ba3b - size: 2241 - original: - hackage: tar-0.6.3.0 -- completed: - hackage: hashable-1.4.2.0@sha256:585792335d5541dba78fa8dfcb291a89cd5812a281825ff7a44afa296ab5d58a,4520 - pantry-tree: - sha256: 792a6cab3f15c5db29d759c8ca735d0be5f4c94f363329652f8b9780009d0829 - size: 1248 - original: - hackage: hashable-1.4.2.0 -- completed: - hackage: decision-diagrams-0.2.0.0@sha256:9f82d39f7331f6836784fa89354986e436a4d62d810b8fb2b44dd10c6a0beb85,3415 - pantry-tree: - sha256: 36696cfd2af10c44fc0b7d8746c57d94c476eef4ba16f6ac98c2d6dae04f4b36 + sha256: 26973e8414beb08901551df63b078fa543aa80ddf46ee2f42e411b246dd79066 size: 866 original: hackage: decision-diagrams-0.2.0.0 @@ -33,9 +19,9 @@ packages: original: hackage: smtlib-backends-0.3 - completed: - hackage: smtlib-backends-process-0.3@sha256:caf131d3d6f6825e3a3182713130a8e14d0bd6530eeda643e8a511b546ff1a26,1676 + hackage: smtlib-backends-process-0.3@sha256:1cdd2ae8ebf3786f08cafe2f6b47001f7647779ad87cba3f05250f68d70e3f07,1676 pantry-tree: - sha256: 7147fef29b4270275168a285fc0c68784329d1276ab9e44e9a45f8d79b526220 + sha256: 05326db88add261e687f039a81b8573a4192b42e47e994230e516b3c604af3e8 size: 461 original: hackage: smtlib-backends-process-0.3 @@ -56,35 +42,17 @@ packages: - completed: name: tasty-test-reporter pantry-tree: - sha256: 474bc3fcf7719257c5a6c3b6b883a41c1fc2e7eb61b42f9ecb93ffe1ad36a592 + sha256: 5a9857eb1fa7fd9dcf6753219623a6ea2c4219b69e192f66c1b709b0b25ce3a2 size: 861 - sha256: 52f8ee5c20aa71ab40f612d617e5d2871ce42c1092de7f500cfc0088671cebab - size: 235629 - url: https://github.com/goodlyrottenapple/tasty-test-reporter/archive/b704130545aa3925a8487bd3e92f1dd5ce0512e2.tar.gz + sha256: d5df376edf759ecd93624ee10900edf0dfa7df5c97589220a6ace96941962d0c + size: 235624 + url: https://github.com/jberthold/tasty-test-reporter/archive/3abbfa942553f0986393af44eda0cb69bcaba6ad.tar.gz version: 0.1.1.4 original: - url: https://github.com/goodlyrottenapple/tasty-test-reporter/archive/b704130545aa3925a8487bd3e92f1dd5ce0512e2.tar.gz -- completed: - name: profiteur - pantry-tree: - sha256: 0aeb13dd17b44a10f92040844224e27bf9d436f48d9436060f6e5e745576ca7e - size: 1806 - sha256: 674623e6590230f69b0841c2b430e7c58fe7d9ea4bc875c2c1c6a98ee80d105e - size: 71475 - url: https://github.com/goodlyrottenapple/profiteur/archive/7b30bbe6b2a6b72a5b4896f3a0eed5587a5bf465.tar.gz - version: 0.4.7.0 - original: - url: https://github.com/goodlyrottenapple/profiteur/archive/7b30bbe6b2a6b72a5b4896f3a0eed5587a5bf465.tar.gz -- completed: - hackage: ghc-prof-1.4.1.12@sha256:0146d3324470db81f6ed1d84b445f1d1aadaeb2e4e045876f5cd231a0946b713,2117 - pantry-tree: - sha256: 37a45db4d22b7b20bd06343cfc9517cadf84536da9cb694a822f6c857d385675 - size: 687 - original: - hackage: ghc-prof-1.4.1.12@sha256:0146d3324470db81f6ed1d84b445f1d1aadaeb2e4e045876f5cd231a0946b713,2117 + url: https://github.com/jberthold/tasty-test-reporter/archive/3abbfa942553f0986393af44eda0cb69bcaba6ad.tar.gz snapshots: - completed: - sha256: 73ad581de7c5306278aec7706cafaf3b1c2eb7abf4ab586e4d9dc675c6106c4e - size: 718708 - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/22/23.yaml - original: lts-22.23 + sha256: 04c9d37f2a00c2bd51bf6b25eb98872059bc58f225d50b5f306ac58f760a178c + size: 680567 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/23/9.yaml + original: lts-23.9