Re-merge Pyk into K (#4164)

This PR merges the Pyk library back into K such that it becomes a
first-class citizen once again, rather than a separately-maintained
library. The changes here are a full import of Pyk's history (cleaned so
that file histories are preserved), and a series of small changes that
set up CI and clean up the resulting issues from performing the merge.

> [!IMPORTANT]  
> This is a major piece of infrastructural change for our code, and it
should be reviewed as carefully as is practical given the nature of the
changes.

There are nearly 800 commits in Pyk's history, and so reviewing the
whole history of this PR is not practical. The salient parts to review
are the commits I have authored (beginning at
[e5c3370](e5c3370),
and ending at
[5caa31c](5caa31c));
their histories are clean and should be easy to review.

Additionally, please take a look through the repository tree as it is on
this branch, and check that the `pyk/` subtree looks reasonable to you
(histories, etc. are all sensible). I would like @tothtamas28, @ehildenb
and @F-WRunTime in particular to check this all over before merging.

See
#4066 (comment)
for a blow-by-blow account of what I've done to produce this PR.

> [!CAUTION]
> We **must not** use the RV automerger for this PR; it will squash the
Pyk history into a single commit (which isn't what we want). Instead,
once this PR has been reviewed and approved, it should be merged using
the GitHub user interface by an admin. Optionally, we can squash the
non-pyk commits to keep the history outside the subdirectory smaller.

Once the PR has been reviewed and is ready to merge, I will take the
following steps:
- Squash my changes down into a single commit, leaving the Pyk history
separate
- Make sure that the branch is up to date and no other PRs are going to
automerge during the merge of this PR
- Make sure that the release job is stable
- Manually merge this PR without squashing

There will be more cleanup of issues, PRs, CI and other ancillary parts
once this PR merges, but these issues are off the critical path.

Closes: #4066

.github/actions/setup-pyk-env/action.yml

@@ -0,0 +1,40 @@
+name: 'Set Up Pyk Environment'
+description: 'Set up Pyk test environment'
+inputs:
+  python-version:
+    description: 'Python version'
+    required: true
+    type: string
+    default: '3.10'
+  install-k:
+    description: 'Install K'
+    required: true
+    type: boolean
+    default: false
+  k-deb-path:
+    description: 'Path to K .deb file'
+    required: true
+    type: string
+    default: kframework.deb
+runs:
+  using: "composite"
+  steps:
+    - name: 'Install Python'
+      uses: actions/setup-python@v5
+      with:
+        python-version: ${{ inputs.python-version }}
+    - name: 'Install Poetry'
+      uses: Gr1N/setup-poetry@v9
+    - name: 'Install K'
+      if: fromJSON(inputs.install-k)
+      shell: bash
+      env:
+        DEB_PACKAGE_NAME: ${{ inputs.k-deb-path }}
+      run: |
+        sudo apt-get update
+        sudo apt-get -y install graphviz ./${DEB_PACKAGE_NAME}
+        sudo update-alternatives --set java /usr/lib/jvm/java-17-openjdk-amd64/bin/java
+        kompile --version
+    - name: 'Install package'
+      shell: bash
+      run: poetry -C pyk install

.github/workflows/release.yml

@@ -126,6 +126,8 @@ jobs:
           docker exec -t k-package-docker-test-jammy-${GITHUB_SHA} bash -c 'cd ~ && echo "module TEST imports BOOL endmodule" > test.k'
           docker exec -t k-package-docker-test-jammy-${GITHUB_SHA} bash -c 'cd ~ && kompile test.k --backend llvm'
           docker exec -t k-package-docker-test-jammy-${GITHUB_SHA} bash -c 'cd ~ && kompile test.k --backend haskell'
+          docker exec -t k-package-docker-test-jammy-${GITHUB_SHA} bash -c 'cd ~ && pyk kompile test.k --backend llvm'
+          docker exec -t k-package-docker-test-jammy-${GITHUB_SHA} bash -c 'cd ~ && pyk kompile test.k --backend haskell'
           docker image push ${DOCKERHUB_REPO}:${version_tag}
       - name: 'Clean up Docker Container'
         if: always()

.github/workflows/test-pr.yml

@@ -102,6 +102,162 @@ jobs:
           if-no-files-found: error
           retention-days: 1
 
+  pyk-code-quality-checks:
+    name: 'Pyk Code Quality Checks'
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: ./pyk
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+      - name: 'Set up environment'
+        uses: ./.github/actions/setup-pyk-env
+      - name: 'Run code quality checks'
+        run: make check
+      - name: 'Run pyupgrade'
+        run: make pyupgrade
+
+  pyk-build-docs:
+    needs: pyk-code-quality-checks
+    name: 'Build Pyk Documentation'
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: ./pyk
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+      - name: 'Set up environment'
+        uses: ./.github/actions/setup-pyk-env
+      - name: 'Build documentation'
+        run: make docs
+
+  pyk-unit-tests:
+    needs: pyk-code-quality-checks
+    name: 'Pyk Unit Tests'
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    strategy:
+      fail-fast: false
+      matrix:
+        python-version: ['3.10', '3.11', '3.12']
+    defaults:
+      run:
+        working-directory: ./pyk
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+      - name: 'Set up environment'
+        uses: ./.github/actions/setup-pyk-env
+        with:
+          python-version: ${{ matrix.python-version }}
+      - name: 'Run unit tests'
+        run: make cov-unit
+
+  pyk-profile:
+    needs: [pyk-code-quality-checks, test-package-ubuntu-jammy]
+    name: 'Pyk Profiling'
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    defaults:
+      run:
+        working-directory: ./pyk
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+      - name: 'Download K package from the Summary Page'
+        uses: actions/download-artifact@v4
+        with:
+          name: kframework.deb
+      - name: 'Set up environment'
+        uses: ./.github/actions/setup-pyk-env
+        with:
+          install-k: true
+          k-deb-path: kframework.deb
+      - name: 'Run profiling'
+        run: |
+          make profile PROF_ARGS=-n2
+          find /tmp/pytest-of-${USER}/pytest-current/ -type f -name '*.prof' | sort | xargs tail -n +1
+  pyk-integration-tests:
+    needs: [pyk-code-quality-checks, test-package-ubuntu-jammy]
+    name: 'Pyk Integration Tests'
+    runs-on: ubuntu-latest
+    timeout-minutes: 40
+    defaults:
+      run:
+        working-directory: ./pyk
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+      - name: 'Download K package from the Summary Page'
+        uses: actions/download-artifact@v4
+        with:
+          name: kframework.deb
+      - name: 'Set up environment'
+        uses: ./.github/actions/setup-pyk-env
+        with:
+          install-k: true
+          k-deb-path: kframework.deb
+      - name: 'Run integration tests'
+        run: make test-integration TEST_ARGS='-n2 --timeout 300'
+
+  pyk-regression-tests:
+    needs: [pyk-code-quality-checks, test-package-ubuntu-jammy]
+    name: 'Pyk K Regression Tests'
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    defaults:
+      run:
+        working-directory: ./pyk
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+      - name: 'Download K package from the Summary Page'
+        uses: actions/download-artifact@v4
+        with:
+          name: kframework.deb
+      - name: 'Set up environment'
+        uses: ./.github/actions/setup-pyk-env
+        with:
+          install-k: true
+          k-deb-path: kframework.deb
+      - name: 'Run K regression tests'
+        run: make test-regression-new -j2
+
+  pyk-build-on-nix:
+    needs: pyk-code-quality-checks
+    name: 'Pyk Build on Nix'
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-13]
+    defaults:
+      run:
+        working-directory: ./pyk
+    runs-on: ${{ matrix.os }}
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+      - name: 'Install Nix'
+        if: ${{ !startsWith(matrix.os, 'self') }}
+        uses: cachix/install-nix-action@v22
+        with:
+          install_url: https://releases.nixos.org/nix/nix-2.13.3/install
+          extra_nix_config: |
+            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
+            substituters = http://cache.nixos.org https://hydra.iohk.io
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
+      - name: 'Install Cachix'
+        if: ${{ !startsWith(matrix.os, 'self') }}
+        uses: cachix/cachix-action@v14
+        with:
+          name: k-framework
+          authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
+          skipPush: true
+      - name: 'Build pyk'
+        run: GC_DONT_GC=1 nix build --print-build-logs .#pyk-python310
+
+
   performance-tests:
     name: 'Performance Tests'
     runs-on: [self-hosted, linux, performance]

CHANGELOG.md

@@ -2,6 +2,48 @@
 copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
+K Framework 7.0.0
+=================
+
+Major Changes
+-------------
+
+- **Important change for all K and Pyk users**. The Pyk library has been
+  reintegrated into K, and is no longer maintained as a standalone project. This
+  means that in K 7, first-class Python tooling is available wherever K is
+  installed. Existing projects using the standalone Pyk library can continue to
+  do so, but will not receive updates in the future.
+
+- The Haskell backend and booster components have been merged and are now
+  developed as a single project.
+
+- Add an explicit `overload(_)` attribute to specify sets of overloaded symbols;
+  this replaces the old `klabel(_)` syntax.
+
+- The outer parser no longer supports `priorities`, `require` and `import`.
+
+Minor Changes
+-------------
+
+- Tooling and version updates for our Java and Scala code.
+
+- Substantial cleanup and auditing of the K frontend's use of attributes when
+  generating KORE definitions.
+
+- Extended compiler warnings for the deprecated `symbol, klabel(_)` attribute
+  combination, as well as for overload sets.
+
+- Clarification and better compiler warnings for cell collection initializers.
+
+- Add `total` attribute to record projection functions that are verifiably
+  total.
+
+- Removed deprecated `--directory` flag.
+
+- Removed deprecated binary format for KAST.
+
+- Removed deprecated `STRATEGY` module.
+
 K Framework 6.3.0
 =================
 

install-k

@@ -1,6 +1,6 @@
 #!/bin/sh -e
 
-K_VERSION=6.3.0
+K_VERSION=7.0.0
 
 if [ `id -u` -ne 0 ]; then
   echo "$0: error: This script must be run as root."

package/arch/PKGBUILD

@@ -1,6 +1,6 @@
 # Maintainer: Dwight Guth <dwight.guth@runtimeverification.com>
 pkgname=kframework-git
-pkgver=6.3.0
+pkgver=7.0.0
 pkgrel=1
 epoch=
 pkgdesc="K framework toolchain. Includes K Framework compiler for K language definitions, and K interpreter and prover for programs written in languages defined in K."

package/debian/changelog

@@ -1,4 +1,4 @@
-kframework (6.3.0) unstable; urgency=medium
+kframework (7.0.0) unstable; urgency=medium
 
   * Initial Release.
 

package/docker/Dockerfile.ubuntu-jammy

@@ -16,4 +16,11 @@ RUN    apt-get update
     && apt-get upgrade --yes                                                            \
     && apt-get install --yes --no-install-recommends /kframework_amd64_ubuntu_jammy.deb
 
+COPY pyk /pyk
+RUN pip install poetry        \
+    && cd /pyk                \
+    && make build             \
+    && pip install dist/*.whl \
+    && rm -rf /pyk
+
 RUN rm -rf /kframework_amd64_ubuntu_jammy.deb

package/version

@@ -1 +1 @@
-6.3.0
+7.0.0

package/version.sh

@@ -24,6 +24,10 @@ version_sub() {
     version="$(cat $version_file)"
     sed --in-place 's/^K_VERSION=.*$/K_VERSION='${version}'/'                                                         install-k
     sed --in-place 's/^kframework (.*) unstable; urgency=medium$/kframework ('${version}') unstable; urgency=medium/' package/debian/changelog
+    sed --in-place 's/^version = ".*"$/version = "'${version}'"/'                                                     pyk/pyproject.toml
+    sed --in-place "s/^version = '.*'$/version = '${version}'/"                                                       pyk/docs/conf.py
+    sed --in-place "s/^release = '.*'$/release = '${version}'/"                                                       pyk/docs/conf.py
+    sed --in-place "s/^__version__: Final = '.*'/__version__: Final = '${version}'/"                                  pyk/src/pyk/__init__.py
 }
 
 version_command="$1" ; shift

pom.xml

@@ -82,7 +82,7 @@
     <googleJavaFormat.version>1.18.1</googleJavaFormat.version>
     <scalafmt.version>3.7.17</scalafmt.version>
     <nativeDirs>**/src/main/native/**</nativeDirs>
-    <spotless.excludes>${nativeDirs},.idea/**,**/com/davekoelle/**,**/target/**,LICENSE.md,web/toc.md,web/k-web-theme/**,**/*-kompiled/*.kore,k-distribution/include/kframework/kore/*,**/.kompile-*/**,**/.git/**,result/**</spotless.excludes>
+    <spotless.excludes>${nativeDirs},.idea/**,**/com/davekoelle/**,**/target/**,LICENSE.md,web/toc.md,web/k-web-theme/**,**/*-kompiled/*.kore,k-distribution/include/kframework/kore/*,**/.kompile-*/**,**/.git/**,result/**,pyk/**</spotless.excludes>
   </properties>
 
   <dependencies>

pyk/.cruft.json

@@ -0,0 +1,18 @@
+{
+  "template": "https://github.com/runtimeverification/python-project-template.git",
+  "commit": "601d5e2a0e8a98c87dcb1ae694d22d76d0114e01",
+  "checkout": null,
+  "context": {
+    "cookiecutter": {
+      "project_name": "pyk",
+      "project_slug": "pyk",
+      "package_name": "pyk",
+      "version": "0.1.0",
+      "description": "",
+      "author_name": "Runtime Verification, Inc.",
+      "author_email": "contact@runtimeverification.com",
+      "_template": "https://github.com/runtimeverification/python-project-template.git"
+    }
+  },
+  "directory": null
+}

pyk/.flake8

@@ -0,0 +1,7 @@
+[flake8]
+max-line-length = 120
+extend-select = B9, TC1
+extend-ignore = B907,B950,E,W1,W2,W3,W4,W5
+per-file-ignores =
+    */__init__.py: F401
+type-checking-strict = true

pyk/.gitignore

@@ -0,0 +1,12 @@
+# For modularity, un-ignore everything from the K parent .gitignore...
+!*
+
+# ...and reinstate the original Pyk .gitignore.
+/dist/
+/docs/api/
+/docs/build/
+__pycache__/
+.coverage
+
+.kprove*
+*.debug-log

pyk/Dockerfile

@@ -0,0 +1,21 @@
+ARG K_DISTRO=jammy
+ARG K_VERSION
+FROM runtimeverificationinc/kframework-k:ubuntu-${K_DISTRO}-${K_VERSION}
+
+ARG PYTHON_VERSION=3.10
+
+RUN    apt-get -y update             \
+    && apt-get -y install            \
+         curl                        \
+         graphviz                    \
+         python${PYTHON_VERSION}     \
+         python${PYTHON_VERSION}-dev \
+    && apt-get -y clean
+
+RUN    curl -sSL https://install.python-poetry.org | POETRY_HOME=/usr python3 - \
+    && poetry --version
+
+ARG USER_ID=9876
+ARG GROUP_ID=9876
+RUN    groupadd -g ${GROUP_ID} user                     \
+    && useradd -m -u ${USER_ID} -s /bin/sh -g user user