Add more debug messages and ask for logging in tests

runtimeverification · May 16, 2024 · cc230ba · cc230ba
1 parent 4afc267
commit cc230ba
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -270,7 +270,7 @@ jobs:
           k-deb-path: kframework.deb
       - name: 'Run integration tests'
         run: |
-          docker exec -u user k-pyk-integration-${{ github.sha }} make test-integration TEST_ARGS='-k "test_prove_claim " -n4 --timeout 300 -vv'
+          docker exec -u user k-pyk-integration-${{ github.sha }} make test-integration TEST_ARGS='-k "test_prove_claim" -n4 --timeout 300 -vv --log-level INFO -rP'
       - name: 'Tear down Docker'
         if: always()
         run: |

diff --git a/pyk/src/pyk/ktool/kprove.py b/pyk/src/pyk/ktool/kprove.py
@@ -217,9 +217,12 @@ def prove(
         env = os.environ.copy()
         existing_opts = os.getenv('KORE_EXEC_OPTS')
         kore_exec_opts = ' '.join(list(haskell_args) + haskell_log_args + ([existing_opts] if existing_opts else []))
-        _LOGGER.debug(f'export KORE_EXEC_OPTS={kore_exec_opts!r}')
+        _LOGGER.info(f'export KORE_EXEC_OPTS={kore_exec_opts!r}')
         env['KORE_EXEC_OPTS'] = kore_exec_opts
 
+        r = run_process(['kore-exec', '--version'], logger=_LOGGER)
+        _LOGGER.info(r)
+
         proc_result = _kprove(
             spec_file=spec_file,
             command=self.prover,
@@ -238,6 +241,7 @@ def prove(
         if proc_result.returncode not in (0, 1):
             raise RuntimeError('kprove failed!')
 
+        _LOGGER.info(log_file.read_text())
         debug_log = _get_rule_log(log_file)
         final_state = KInner.from_dict(kast_term(json.loads(proc_result.stdout)))
         if is_top(final_state) and len(debug_log) == 0: