Add kompile file and run with booster-dev

geo2a · geo2a · commit d070611ea020 · 2024-05-29T11:51:17.000+02:00
diff --git a/booster/test/rpc-integration/resources/non-linear-int-requires.k b/booster/test/rpc-integration/resources/non-linear-int-requires.k
@@ -1,4 +1,4 @@
-module TEST
+module NON-LINEAR-INT-REQUIRES
   imports INT
   imports BOOL
 
diff --git a/booster/test/rpc-integration/resources/non-linear-int-requires.kompile b/booster/test/rpc-integration/resources/non-linear-int-requires.kompile
@@ -0,0 +1,3 @@
+kompile --backend haskell non-linear-int-requires.k --syntax-module NON-LINEAR-INT-REQUIRES
+cp non-linear-int-requires-kompiled/definition.kore ./non-linear-int-requires.kore
+rm -r non-linear-int-requires-kompiled
diff --git a/scripts/booster-integration-tests.sh b/scripts/booster-integration-tests.sh
@@ -49,7 +49,7 @@ for dir in $(ls -d test-*); do
             SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@
             SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@
             ;;
-        "compute-ceil" | "no-evaluator")
+        "compute-ceil" | "no-evaluator" | "non-linear-int-requires")
             SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@
             ;;
         "simplify")

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-module TEST`
	`1`	`+module NON-LINEAR-INT-REQUIRES`
`2`	`2`	`imports INT`
`3`	`3`	`imports BOOL`
`4`	`4`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+kompile --backend haskell non-linear-int-requires.k --syntax-module NON-LINEAR-INT-REQUIRES`
	`2`	`+cp non-linear-int-requires-kompiled/definition.kore ./non-linear-int-requires.kore`
	`3`	`+rm -r non-linear-int-requires-kompiled`