CLI and test improvements (#270)

* Specification file does not require `--spec-file` * `pretty` is default output for `parse` and `run` * Changed `prove` command in `nix-tests.sh` * Changed `make test-integration` to call all tests in single session * Added summary for `SKIPPED` and `FAILING` * Set Version: 0.2.9 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Dec 11, 2023 · b6242d4 · b6242d4
1 parent 11980a5
commit b6242d4
Show file tree

Hide file tree

Showing 7 changed files with 20 additions and 15 deletions.
diff --git a/kmir/Makefile b/kmir/Makefile
@@ -35,7 +35,12 @@ test: test-unit test-integration
 test-unit: poetry-install
 	$(POETRY_RUN) pytest src/tests/unit --maxfail=1 --verbose $(TEST_ARGS)
 
-test-integration: test-integration-parse test-integration-run test-integration-prove
+test-integration: poetry-install
+	$(POETRY_RUN) pytest -ra                                              \
+        src/tests/integration/test_parse.py                               \
+        src/tests/integration/test_run.py                                 \
+        src/tests/integration/test_prove.py                               \
+        --numprocesses=4 --durations=0 --maxfail=1 --verbose $(TEST_ARGS) \
 
 test-integration-parse: poetry-install
 	$(POETRY_RUN) pytest src/tests/integration/test_parse.py --numprocesses=4 --durations=0 --maxfail=1 --verbose $(TEST_ARGS)
@@ -48,7 +53,7 @@ test-integration-prove: poetry-install
 
 ## Produce *-fail.tsv files by running the tests with --no-skip and no parallelism
 compiletest-parse-fail:
-	-$(POETRY_RUN) pytest src/tests/integration/test_parse.py                    \
+	-$(POETRY_RUN) pytest src/tests/integration/test_parse.py                        \
             --tb=line                                                                \
             --no-skip                                                                \
             -k test_compiletest                                                      \
@@ -58,7 +63,7 @@ compiletest-parse-fail:
 .PHONY: compiletest-parse-fail
 
 compiletest-run-fail:
-	-$(POETRY_RUN) pytest src/tests/integration/test_run.py                     \
+	-$(POETRY_RUN) pytest src/tests/integration/test_run.py                         \
             --timeout=30                                                            \
             --tb=line                                                               \
             --no-skip                                                               \
@@ -69,7 +74,7 @@ compiletest-run-fail:
 .PHONY: compiletest-run-fail
 
 handwritten-parse-fail:
-	-$(POETRY_RUN) pytest src/tests/integration/test_parse.py                     \
+	-$(POETRY_RUN) pytest src/tests/integration/test_parse.py                         \
             --tb=line                                                                 \
             --no-skip                                                                 \
             -k test_handwritten_syntax                                                \
@@ -79,7 +84,7 @@ handwritten-parse-fail:
 .PHONY: handwritten-test-parse
 
 handwritten-run-fail:
-	$(POETRY_RUN) pytest src/tests/integration/test_run.py                      \
+	$(POETRY_RUN) pytest src/tests/integration/test_run.py                          \
             --tb=line                                                               \
             --no-skip                                                               \
             -k test_handwritten                                                     \

diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.2.8"
+version = "0.2.9"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py
@@ -2,4 +2,4 @@
 
 from .kmir import KMIR
 
-VERSION: Final = '0.2.8'
+VERSION: Final = '0.2.9'
diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py
@@ -60,9 +60,9 @@ def exec_init(llvm_dir: str, **kwargs: Any) -> KMIR:
 
 def exec_parse(
     input_file: str,
+    input: str,
+    output: str,
     definition_dir: str | None = None,
-    input: str = 'program',
-    output: str = 'kore',
     **kwargs: Any,
 ) -> None:
     kast_input = KAstInput[input.upper()]
@@ -77,8 +77,8 @@ def exec_parse(
 
 def exec_run(
     input_file: str,
+    output: str,
     definition_dir: str | None = None,
-    output: str = 'none',
     depth: int | None = None,
     bug_report: bool = False,
     ignore_return_code: bool = False,

diff --git a/kmir/src/kmir/cli.py b/kmir/src/kmir/cli.py
@@ -54,7 +54,7 @@ def create_argument_parser() -> ArgumentParser:
     parse_subparser.add_argument(
         '--output',
         type=str,
-        default='kore',
+        default='pretty',
         help='Output mode',
         choices=['pretty', 'program', 'json', 'kore', 'kast', 'none'],
         required=False,
@@ -76,7 +76,7 @@ def create_argument_parser() -> ArgumentParser:
     run_subparser.add_argument(
         '--output',
         type=str,
-        default='kast',
+        default='pretty',
         help='Output mode',
         choices=['pretty', 'program', 'json', 'kore', 'kast', 'none'],
         required=False,
@@ -115,7 +115,7 @@ def create_argument_parser() -> ArgumentParser:
         help='Path to Haskell definition to use.',
     )
     prove_subparser.add_argument(
-        '--spec-file',
+        'spec_file',
         type=file_path,
         help='Path to specification file',
     )

diff --git a/kmir/src/tests/nix/nix-tests.sh b/kmir/src/tests/nix/nix-tests.sh
@@ -15,4 +15,4 @@ kmir run   --output pretty sum-to-n.mir > nix-sum-to-n.run.out
 # Uncomment and run `nix build --extra-experimental-features 'nix-command flakes' --print-build-logs .#kmir-test`
 git --no-pager diff nix-sum-to-n.run.out   sum-to-n.run.out
 
-kmir prove --spec-file simple-spec.k
+kmir prove simple-spec.k
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.2.8
+0.2.9