Merge master into branch

Author: nwatson22

.github/workflows/test-pr.yml

@@ -59,6 +59,7 @@ jobs:
     needs: code-quality-checks
     name: 'Unit Tests'
     runs-on: ubuntu-latest
+    timeout-minutes: 5
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
@@ -71,6 +72,7 @@ jobs:
     needs: code-quality-checks
     name: 'Profiling'
     runs-on: [self-hosted, linux, normal-ephemeral]
+    timeout-minutes: 10
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
@@ -97,6 +99,7 @@ jobs:
     needs: code-quality-checks
     name: 'Integration Tests'
     runs-on: [self-hosted, linux, normal-ephemeral]
+    timeout-minutes: 30
     strategy:
       matrix:
         python-version: ['3.10', '3.11']
@@ -118,7 +121,7 @@ jobs:
           sudo apt-get -y install graphviz ./${DEB_PACKAGE_NAME}
           kompile --version
       - name: 'Run integration tests'
-        run: make cov-integration COV_ARGS='-n8'
+        run: make cov-integration COV_ARGS='-n8 --timeout 300'
 
   build-on-nix:
     needs: code-quality-checks

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.624'
-release = '0.1.624'
+version = '0.1.627'
+release = '0.1.627'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.624
+0.1.627

poetry.lock

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.624"
+version = "0.1.627"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -36,6 +36,7 @@ pep8-naming = "*"
 pytest = "*"
 pytest-cov = "*"
 pytest-mock = "*"
+pytest-timeout = "*"
 pytest-xdist = "*"
 pyupgrade = "*"
 sphinx = "*"

pyproject.toml

@@ -37,12 +37,12 @@ def mlEquals(  # noqa: N802
     return KLabel('#Equals', arg_sort, sort)(term1, term2)
 
 
-def mlEqualsTrue(term: KInner) -> KApply:  # noqa: N802
-    return mlEquals(TRUE, term, BOOL)
+def mlEqualsTrue(term: KInner, sort: str | KSort = GENERATED_TOP_CELL) -> KApply:  # noqa: N802
+    return mlEquals(TRUE, term, arg_sort=BOOL, sort=sort)
 
 
-def mlEqualsFalse(term: KInner) -> KApply:  # noqa: N802
-    return mlEquals(FALSE, term, BOOL)
+def mlEqualsFalse(term: KInner, sort: str | KSort = GENERATED_TOP_CELL) -> KApply:  # noqa: N802
+    return mlEquals(FALSE, term, arg_sort=BOOL, sort=sort)
 
 
 def mlTop(sort: str | KSort = GENERATED_TOP_CELL) -> KApply:  # noqa: N802

src/pyk/prelude/ml.py

@@ -1,3 +1,3 @@
-from .equality import EqualityProof, EqualityProver
+from .equality import EqualityProof, ImpliesProver, RefutationProof
 from .proof import ProofStatus
 from .reachability import APRProof, APRProver