Clean-up the executables in package kore (#3811)

Part of #3800 - remove `kore-check-functions`, `kore-format` and `kore-simplify` - Move `kore-parser` and `kore-match-disjunction` to the `hs-backend-booster-dev-tools` package Before merging, we should run the integration tests of K to make sure nothing is broken. --------- Co-authored-by: github-actions <[email protected]>
runtimeverification · Apr 16, 2024 · 744faf7 · 744faf7
1 parent 9ec5ff6
commit 744faf7
Show file tree

Hide file tree

Showing 12 changed files with 41 additions and 553 deletions.
diff --git a/Makefile b/Makefile
@@ -2,26 +2,16 @@ include include.mk
 
 .PHONY: all kore clean clean-execution docs haddock \
 		test test-kore test-k test-k-simplifierx test-simplifierx \
-		kore-exec kore-repl kore-parser kore-check-functions \
-		kore-format kore-match-disjunction
+		kore-exec kore-repl
 
-all: kore-exec kore-repl kore-parser kore-check-functions kore-format \
-	kore-match-disjunction
+all: kore-exec kore-repl
 
 kore: all
 
 kore-exec: $(KORE_EXEC)
 
 kore-repl: $(KORE_REPL)
 
-kore-parser: $(KORE_PARSER)
-
-kore-check-functions: $(KORE_CHECK_FUNCTIONS)
-
-kore-format: $(KORE_FORMAT)
-
-kore-match-disjunction: $(KORE_MATCH_DISJUNCTION)
-
 docs: haddock
 
 haddock:

diff --git a/kore/app/match-disjunction/Main.hs → dev-tools/kore-match-disjunction/Main.hs b/kore/app/match-disjunction/Main.hs → dev-tools/kore-match-disjunction/Main.hs
@@ -1,3 +1,6 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
 module Main (main) where
 
 import GlobalMain

diff --git a/kore/app/parser/Main.hs → dev-tools/kore-parser/Main.hs b/kore/app/parser/Main.hs → dev-tools/kore-parser/Main.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
 module Main (main) where
 
 import Control.Monad.Catch (

diff --git a/dev-tools/package.yaml b/dev-tools/package.yaml
@@ -86,7 +86,7 @@ executables:
       - text
       - transformers
     ghc-options:
-    - -rtsopts
+      - -rtsopts
   parsetest-binary:
     source-dirs: parsetest-binary
     main: ParsetestBinary.hs
@@ -98,7 +98,7 @@ executables:
       - hs-backend-booster
       - text
     ghc-options:
-    - -rtsopts
+      - -rtsopts
   pretty:
     source-dirs: pretty
     main: Pretty.hs
@@ -111,7 +111,7 @@ executables:
       - text
       - transformers
     ghc-options:
-    - -rtsopts
+      - -rtsopts
   eventlog-parser:
     source-dirs: eventlog-parser
     main: EventlogParser.hs
@@ -132,7 +132,7 @@ executables:
       - unix
       - unordered-containers
     ghc-options:
-    - -rtsopts
+      - -rtsopts
   kore-json-differ:
     source-dirs: kore-json-differ
     main: Main.hs
@@ -141,6 +141,8 @@ executables:
       - bytestring
       - containers
       - hs-backend-booster
+    ghc-options:
+      - -rtsopts
   tarball-compare:
     source-dirs: tarball-compare
     main: Main
@@ -189,3 +191,25 @@ executables:
     - -rtsopts
     - -threaded
     - -with-rtsopts=-N
+  kore-match-disjunction:
+    source-dirs: kore-match-disjunction
+    main: Main.hs
+    dependencies:
+      - base
+      - clock
+      - kore
+      - optparse-applicative
+      - transformers
+    ghc-options:
+      - -rtsopts
+  kore-parser:
+    source-dirs: kore-parser
+    main: Main.hs
+    dependencies:
+      - base
+      - bytestring
+      - containers
+      - exceptions
+      - kore
+    ghc-options:
+      - -rtsopts
diff --git a/flake.nix b/flake.nix
@@ -73,8 +73,6 @@
                 '';
                 postInstall = ''
                   ${drv.postInstall or ""}
-                  rm $out/bin/kore-check-functions
-                  rm $out/bin/kore-format
                 '';
               })).override {
                 # bit pathological, but ghc-compact is already included with the ghc compiler
@@ -237,10 +235,12 @@
             haskell.lib.justStaticExecutables haskell-backend.pkgSet.kore;
           hs-backend-booster = with pkgs;
             haskell.lib.justStaticExecutables haskell-backend.pkgSet.hs-backend-booster;
+          hs-backend-booster-dev-tools = with pkgs;
+            haskell.lib.justStaticExecutables haskell-backend.pkgSet.hs-backend-booster-dev-tools;
         in {
           kore-exec = withZ3 pkgs kore "kore-exec";
-          kore-match-disjunction = withZ3 pkgs kore "kore-match-disjunction";
-          kore-parser = withZ3 pkgs kore "kore-parser";
+          kore-match-disjunction = withZ3 pkgs hs-backend-booster-dev-tools "kore-match-disjunction";
+          kore-parser = withZ3 pkgs hs-backend-booster-dev-tools "kore-parser";
           kore-repl = withZ3 pkgs kore "kore-repl";
           kore-rpc = withZ3 pkgs kore "kore-rpc";
           kore-rpc-booster = withZ3 pkgs hs-backend-booster "kore-rpc-booster";

diff --git a/include.mk b/include.mk
@@ -59,35 +59,13 @@ KORE_REPL_OPTS = --no-bug-report
 export KORE_REPL
 export KORE_REPL_OPTS
 
-KORE_CHECK_FUNCTIONS = $(BUILD_DIR)/kore/bin/kore-check-functions
-KORE_CHECK_FUNCTIONS_OPTS = --no-bug-report
-export KORE_CHECK_FUNCTIONS
-export KORE_CHECK_FUNCTIONS_OPTS
-
-KORE_FORMAT = $(BUILD_DIR)/kore/bin/kore-format
-KORE_FORMAT_OPTS = --no-bug-report
-export KORE_FORMAT
-export KORE_FORMAT_OPTS
-
-KORE_MATCH_DISJUNCTION = $(BUILD_DIR)/kore/bin/kore-match-disjunction
-KORE_MATCH_DISJUNCTION_OPTS = --no-bug-report
-export KORE_MATCH_DISJUNCTION
-export KORE_MATCH_DISJUNCTION_OPTS
+$(BUILD_DIR)/kore/bin/kore-parser:
+	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins hs-backend-booster-dev-tools:exe:kore-parser
 
 $(BUILD_DIR)/kore/bin/kore-exec:
 	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-exec
 
 $(BUILD_DIR)/kore/bin/kore-repl:
 	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-repl
 
-$(BUILD_DIR)/kore/bin/kore-parser:
-	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-parser
-
-$(BUILD_DIR)/kore/bin/kore-check-functions:
-	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-check-functions
-
-$(BUILD_DIR)/kore/bin/kore-format:
-	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-format
 
-$(BUILD_DIR)/kore/bin/kore-match-disjunction:
-	$(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-match-disjunction
diff --git a/kore/Makefile b/kore/Makefile
@@ -46,21 +46,6 @@ ghcid:
 ghcid-repl:
 	$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-repl --work-dir .stack-work-ghci"
 
-ghcid-match:
-	$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-match-disjunction --work-dir .stack-work-ghci"
-
-ghcid-check-func:
-	$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-check-functions --work-dir .stack-work-ghci"
-
-ghcid-parser:
-	$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-parser --work-dir .stack-work-ghci"
-
-ghcid-format:
-	$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-format --work-dir .stack-work-ghci"
-
-ghcid-simplify:
-	$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-simplify --work-dir .stack-work-ghci"
-
 dev-deps:
 	stack install ghcid
 

diff --git a/kore/README.md b/kore/README.md
diff --git a/kore/app/check-functions/Main.hs b/kore/app/check-functions/Main.hs