Misc dev fixes (#411)

This PR contains a number of small misc dev tools/fixes:

* Add `pretty`, a KORE JSON pretty printer util, useful when looking at
bug reports without the original k definition (If we have the K
definition, It's better to call pyk's pretty printer). The README has
been updated with a sample use-case invocation.
* Fix performance scripts, `kevm-dist` -> `kdist`
* Modify the nix shell to automatically call `hpack` when the shell is
re-loaded, useful to keep the local cabal files in sync with
`package.yaml`
* Cleanup the README, removing references to stale nix stuff related to
the dev shell.

---------

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

README.md

@@ -47,37 +47,15 @@ There are several things you can do, to make the development via nix as seamless
 
 #### Nix shell
 
-To open the nix shell you will need nix version 2.4 or newer. Then use either `nix develop` (if you have flakes enabled) or use the old style `nix-shell` command.
+To open the nix shell, run `nix develop`. You will need nix version 2.4 or newer with nix flakes enabled.
 
-If you want to open a shell for a different version of ghc (currently supporting `ghc927`), use
-
-```bash
-nix develop .#ghc927
-```
-or
-
-```bash
-nix-shell --argstr ghc ghc927
-```
-
-You can open a dev shell which contains cabal with all the required libraries compiled with profiling via:
-
-```
-nix develop .#ghc925-prof
-```
 
 #### Nix-direnv
 
 Using a version of direnv that works with nix (https://github.com/nix-community/nix-direnv) allows seamless loading and unloading of the nix shell, which adds all the required packages such as `cabal`, `hpack`, `fourmolu`, etc. Use the above link to install `nix-direnv`, making sure to hook direnv into whichever shell you are using (https://direnv.net/docs/hook.html). You can use the default nix shell (currently GHC version 9.2.7) by running
 
 ```bash
-echo "use nix" > .envrc
-```
-
-If you want to use a different version of GHC for your shell, e.g. `ghc927`, use
-
-```bash
-echo "use flake .#ghc927" > .envrc
+echo "use flake ." > .envrc
 ```
 
 Finally, run `direnv allow` inside the repo folder to load up the nix shell.
@@ -101,11 +79,7 @@ To get HLS working in VSCode, install these two extensions:
 https://marketplace.visualstudio.com/items?itemName=arrterian.nix-env-selector
 https://marketplace.visualstudio.com/items?itemName=haskell.haskell
 
-The `nix-env-selector` extension may prompt for the workspace to be re-loaded. Once re-loaded, HLS should start working. In case you need to use a specific version of ghc for this extension, modify the `.vscode/settings.json` file here:
-
-```json
-  "nixEnvSelector.args": "--argstr ghc ghc927"
-```
+The `nix-env-selector` extension may prompt for the workspace to be re-loaded. Once re-loaded, HLS should start working. 
 
 ## Eventlog tracing
 
@@ -130,4 +104,12 @@ Besides compiling the backend with profiling mode, we can also enable a targeted
 1) Rename `bug-report.tar.gz` to something more descriptive like `issue-123.tar.gz`
 2) Copy the tar file into `test/rpc-integration/`
 3) Run `./generateDirectoryTest.sh issue-123.tar.gz`. This will copy the definition files into `resources/` and rpc commands into `test-issue-123/`
-4) Run the test via `./runDirectoryTest test-issue-123`
+4) Run the test via `./runDirectoryTest test-issue-123`
+
+## Pretty printing KORE JSON
+
+There is a simple utility called pretty which can be used to pretty print a KORE JSON term from a bug report, which does not contain the original K definition:
+
+```
+cabal run pretty -- ../definition.kore <(jq '.result.state' XXX_response.json)
+```

dev-tools/package.yaml

@@ -96,6 +96,19 @@ executables:
       - text
     ghc-options:
     - -rtsopts
+  pretty:
+    source-dirs: pretty
+    main: Pretty.hs
+    dependencies:
+      - base
+      - aeson
+      - bytestring
+      - hs-backend-booster
+      - prettyprinter
+      - text
+      - transformers
+    ghc-options:
+    - -rtsopts
   eventlog-parser:
     source-dirs: eventlog-parser
     main: EventlogParser.hs

dev-tools/pretty/Pretty.hs

@@ -0,0 +1,42 @@
+{-# LANGUAGE PatternSynonyms #-}
+
+{- | Pretty printer for JSON KORE terms
+
+Copyright   : (c) Runtime Verification, 2022
+License     : BSD-3-Clause
+-}
+module Main (
+    main,
+) where
+
+import Booster.Prettyprinter (renderDefault)
+import Booster.Syntax.Json (KoreJson (..))
+import Booster.Syntax.Json.Internalise (
+    internalisePattern,
+    pattern CheckSubsorts,
+    pattern DisallowAlias,
+ )
+import Booster.Syntax.ParsedKore (internalise, parseKoreDefinition)
+import Control.Monad.Trans.Except
+import Data.Aeson (eitherDecode)
+import Data.ByteString.Lazy qualified as BS
+import Data.Text.IO qualified as Text
+import Prettyprinter
+import System.Environment (getArgs)
+
+main :: IO ()
+main = do
+    [def, json] <- getArgs
+    parsedDef <-
+        either (error . renderDefault . pretty) id . parseKoreDefinition def <$> Text.readFile def
+    let internalDef = either (error . renderDefault . pretty) id $ internalise Nothing parsedDef
+
+    fileContent <- BS.readFile json
+    case eitherDecode fileContent of
+        Left err -> putStrLn $ "Error: " ++ err
+        Right KoreJson{term} -> do
+            let (trm, _subst) =
+                    either (error . show) id $
+                        runExcept $
+                            internalisePattern DisallowAlias CheckSubsorts Nothing internalDef term
+            putStrLn $ renderDefault $ pretty trm

flake.nix

@@ -119,7 +119,12 @@
         };
       });
 
-      devShell =
-        perSystem (system: (nixpkgsFor system).booster-backend.devShell);
+      devShell = perSystem (system:
+        (nixpkgsFor system).booster-backend.devShell.overrideAttrs (old: {
+          shellHook = ''
+            ${old.shellHook}
+            hpack && cd dev-tools && hpack
+          '';
+        }));
     };
 }

scripts/performance-tests-kevm.sh

@@ -55,7 +55,7 @@ fi
 git submodule update --init --recursive --depth 1 kevm-pyk/src/kevm_pyk/kproj/plugin
 
 
-feature_shell "make poetry && poetry run -C kevm-pyk -- kevm-dist --verbose build evm-semantics.plugin evm-semantics.haskell --jobs 4"
+feature_shell "make poetry && poetry run -C kevm-pyk -- kdist --verbose build evm-semantics.plugin evm-semantics.haskell --jobs 4"
 
 mkdir -p $SCRIPT_DIR/logs
 

scripts/performance-tests-kontrol.sh

@@ -68,7 +68,7 @@ master_shell() {
   GC_DONT_GC=1 nix develop . --extra-experimental-features 'nix-command flakes' --override-input kevm/k-framework/booster-backend github:runtimeverification/hs-backend-booster/$MASTER_COMMIT --command bash -c "$1"
 }
 
-feature_shell "poetry install && poetry run kevm-dist --verbose build evm-semantics.plugin evm-semantics.haskell kontrol.foundry --jobs 4"
+feature_shell "poetry install && poetry run kdist --verbose build evm-semantics.plugin evm-semantics.haskell kontrol.foundry --jobs 4"
 
 mkdir -p $SCRIPT_DIR/logs