From cc230baebab7323c51a71488271490655ba83c93 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 16 May 2024 11:08:10 +0200 Subject: [PATCH] Add more debug messages and ask for logging in tests --- .github/workflows/test-pr.yml | 2 +- pyk/src/pyk/ktool/kprove.py | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index b81d5ff62e0..086c9558394 100644 --- 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 index db350daa009..8c8affca2eb 100644 --- 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: