HOTFIX Better version information (#3983)

* Adds the version as a tag to master whenever the release branch is
updated with a new version
* Always recompiles the files that use template Haskell to read `git`
information to output as a version
* Outputs only the version number if it is a proper `release` version,
not the dummy version `0.1.0` from master
```
$ kore-rpc-client  --version
0.1.40
$ kore-rpc-booster  --version
0.1.40
$ kore-rpc  --version
0.1.40
```
* Otherwise outputs the `git` information as before:
```
$ .build/kore/bin/kore-rpc-client  --version
hs-backend-booster custom build:
  revision:	723eaa2 (dirty)
  branch:	HOTFIX-better-version-information
  last commit:	Wed Jul 17 14:59:15 2024 +1000

$ .build/kore/bin/kore-rpc-booster  --version
hs-backend-booster custom build:
  revision:	723eaa2 (dirty)
  branch:	HOTFIX-better-version-information
  last commit:	Wed Jul 17 14:59:15 2024 +1000

$ .build/kore/bin/kore-rpc  --version
kore custom build:
  revision:	723eaa2 (dirty)
  branch:	HOTFIX-better-version-information
  last commit:	Wed Jul 17 14:59:15 2024 +1000
```

---------

Co-authored-by: github-actions <github-actions@github.com>

.github/workflows/master.yml

@@ -78,4 +78,6 @@ jobs:
           ./package/version.sh sub
           if git add --update && git commit --no-edit --allow-empty --message "Set Version: $(cat package/version)"; then
             git push origin release
+            git tag "v$(cat package/version)" origin/master
+            git push "v$(cat package/version)"
           fi

booster/library/Booster/CLOptions.hs

@@ -1,6 +1,8 @@
 {-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE TemplateHaskell #-}
 
+{-# OPTIONS -fforce-recomp #-}
+
 module Booster.CLOptions (
     CLOptions (..),
     EquationOptions (..),
@@ -22,6 +24,7 @@ import Data.Map qualified as Map
 import Data.Maybe (fromMaybe)
 import Data.Text (Text, pack)
 import Data.Text.Encoding (decodeASCII)
+import Data.Version (Version (..), showVersion)
 import Options.Applicative
 import Text.Casing (fromHumps, fromKebab, toKebab, toPascal)
 import Text.Read (readMaybe)
@@ -34,6 +37,7 @@ import Booster.SMT.LowLevelCodec qualified as SMT (parseSExpr)
 import Booster.Trace (CustomUserEventType)
 import Booster.Util (Bound (..), encodeLabel)
 import Booster.VersionInfo (VersionInfo (..), versionInfo)
+import Paths_hs_backend_booster (version)
 
 data CLOptions = CLOptions
     { definitionFile :: FilePath
@@ -436,12 +440,15 @@ versionInfoParser =
         )
 
 versionInfoStr :: String
-versionInfoStr =
-    unlines
-        [ "hs-backend-booster version:"
-        , "  revision:\t" <> gitHash <> if gitDirty then " (dirty)" else ""
-        , "  branch:\t" <> fromMaybe "<unknown>" gitBranch
-        , "  last commit:\t" <> gitCommitDate
-        ]
+versionInfoStr
+    | version == dummyVersion =
+        unlines
+            [ "hs-backend-booster custom build:"
+            , "  revision:\t" <> gitHash <> if gitDirty then " (dirty)" else ""
+            , "  branch:\t" <> fromMaybe "<unknown>" gitBranch
+            , "  last commit:\t" <> gitCommitDate
+            ]
+    | otherwise = showVersion version
   where
     VersionInfo{gitHash, gitDirty, gitBranch, gitCommitDate} = $versionInfo
+    dummyVersion = Version [0, 1, 0] []

booster/tools/rpc-client/RpcClient.hs

@@ -51,6 +51,7 @@ import System.Time.Extra (Seconds, sleep)
 import Text.Casing (fromKebab, toPascal)
 import Text.Read (readMaybe)
 
+import Booster.CLOptions (versionInfoParser)
 import Booster.JsonRpc (rpcJsonConfig)
 import Booster.JsonRpc.Utils (
     DiffResult (DifferentType),
@@ -336,7 +337,7 @@ parseCommonOptions =
 parseOptions :: ParserInfo Options
 parseOptions =
     info
-        (parseOptions' <**> helper)
+        (parseOptions' <**> versionInfoParser <**> helper)
         ( fullDesc
             <> progDesc "Simple RPC test client"
         )

kore/app/share/GlobalMain.hs

@@ -1,5 +1,7 @@
 {-# LANGUAGE TemplateHaskell #-}
 
+{-# OPTIONS -fforce-recomp #-}
+
 {- |
 Copyright   : (c) Runtime Verification, 2020-2022
 License     : BSD-3-Clause
@@ -70,6 +72,7 @@ import Data.Text (
     pack,
  )
 import Data.Text.IO qualified as Text
+import Data.Version (Version (..), showVersion)
 import GHC.Compact (getCompact)
 import GHC.Generics qualified as GHC
 import GHC.Stack (
@@ -178,6 +181,7 @@ import Options.SMT (
     KoreSolverOptions (..),
     Solver (..),
  )
+import Paths_kore (version)
 import Prelude.Kore
 import Pretty qualified as KorePretty
 import SMT (
@@ -358,14 +362,17 @@ mainGlobal exeName maybeEnv localOptionsParser modifiers = do
 
 -- | main function to print version information
 mainVersion :: IO ()
-mainVersion =
-    mapM_
-        putStrLn
-        [ "Git:"
-        , "  revision:\t" ++ gitHash ++ if gitDirty then " (dirty)" else ""
-        , "  branch:\t" ++ fromMaybe "<unknown>" gitBranch
-        , "  last commit:\t" ++ gitCommitDate
-        ]
+mainVersion
+    | version == Version [0, 1, 0] [] =
+        mapM_
+            putStrLn
+            [ "kore custom build:"
+            , "  revision:\t" ++ gitHash ++ if gitDirty then " (dirty)" else ""
+            , "  branch:\t" ++ fromMaybe "<unknown>" gitBranch
+            , "  last commit:\t" ++ gitCommitDate
+            ]
+    | otherwise =
+        putStrLn $ showVersion version
   where
     VersionInfo{gitHash, gitDirty, gitBranch, gitCommitDate} = $versionInfo
 

kore/kore.cabal

@@ -560,6 +560,7 @@ library
     Log.Entry
     Logic
     Options.SMT
+    Paths_kore
     Pair
     Partial
     Prelude.Kore