Reorganize pyk distribution (#2513)

* Replace hand-written kpyk script by setup.cfg entry point

* Move pyk to root

* Organize requirements

* Add src folder

* Move pyk integration tests to pyk folder

* Perform linting on integration_tests

* Add test-integration make target

* Add CI test steps for pyk

* Organize venv make targets

* Install pyk in Focal image

* Add README.md

Jenkinsfile

@@ -72,6 +72,9 @@ pipeline {
                   export K_OPTS='-Xmx12G'
                   echo 'Building K...'
                   mvn --batch-mode verify -U
+                  echo 'Testing pyk...'
+                  make -C pyk
+                  make -C pyk integration-test
                   echo 'Starting kserver...'
                   k-distribution/target/release/k/bin/spawn-kserver kserver.log
                   cd k-exercises/tutorial

k-distribution/Makefile

@@ -1,3 +1,3 @@
-SUBDIRS=pl-tutorial tests/equiv tests/regression-new tests/builtins/collections tests/pyk src/main/scripts/lib/pyk
+SUBDIRS=pl-tutorial tests/equiv tests/regression-new tests/builtins/collections
 
 include include/kframework/ktest-group.mak

package/docker/Dockerfile.ubuntu-focal

@@ -8,7 +8,8 @@ RUN    apt-get update                   \
     && apt-get install --yes            \
                         build-essential \
                         git             \
-                        python
+                        python          \
+                        python3-pip
 
 RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.11 \
     && cd z3                                                         \
@@ -25,3 +26,7 @@ RUN    apt-get update                                     \
     && apt-get install --yes /kframework_amd64_focal.deb
 
 RUN rm -rf /kframework_amd64_focal.deb
+
+COPY pyk/ /pyk
+RUN    pip3 install /pyk \
+    && rm -rf /pyk

pyk/Makefile

@@ -0,0 +1,68 @@
+.PHONY: all clean test integration-test                            \
+        $(VENV_DEV_DIR) $(VENV_PROD_DIR)                           \
+        check-code-style isort check-isort check-flake8 check-mypy
+
+
+all: check-code-style test
+
+
+# virtualenv
+
+VENV_DEV_DIR := venv-dev
+VENV_DEV     := $(VENV_DEV_DIR)/pyvenv.cfg
+ACTIVATE_DEV := . $(VENV_DEV_DIR)/bin/activate
+
+$(VENV_DEV):
+	   virtualenv -p python3.8 $(VENV_DEV_DIR) \
+	&& $(ACTIVATE_DEV)                         \
+	&& pip install -r requirements/dev.txt
+
+$(VENV_DEV_DIR): $(VENV_DEV)
+	@echo $(ACTIVATE_DEV)
+
+
+VENV_PROD_DIR := venv-prod
+VENV_PROD     := $(VENV_PROD_DIR)/pyvenv.cfg
+ACTIVATE_PROD := . $(VENV_PROD_DIR)/bin/activate
+
+$(VENV_PROD):
+	   virtualenv -p python3.8 $(VENV_PROD_DIR) \
+	&& $(ACTIVATE_PROD)                         \
+	&& pip install .
+
+$(VENV_PROD_DIR): $(VENV_PROD)
+	@echo $(ACTIVATE_PROD)
+
+
+# Checks
+
+check-code-style: check-isort check-flake8 check-mypy
+
+isort: $(VENV_DEV)
+	$(ACTIVATE_DEV) && isort src integration_tests
+
+check-isort: $(VENV_DEV)
+	$(ACTIVATE_DEV) && isort --check src integration_tests
+
+check-flake8: $(VENV_DEV)
+	$(ACTIVATE_DEV) && flake8 src integration_tests
+
+check-mypy: $(VENV_DEV)
+	$(ACTIVATE_DEV) && mypy src integration_tests
+
+
+# Tests
+
+test: $(VENV_DEV)
+	$(ACTIVATE_DEV) && python3 -m unittest discover --start-directory src
+
+integration-test: $(VENV_PROD)
+	$(ACTIVATE_PROD) && $(MAKE) -C integration_tests
+	rm -rf $(VENV_PROD_DIR) build src/pyk.egg-info
+
+# Clean
+
+clean:
+	rm -rf $(VENV_DEV_DIR) $(VENV_PROD_DIR) build src/pyk.egg-info .myp_cache
+	find -type d -name __pycache__ -prune -exec rm -rf {} \;
+	$(MAKE) -C integration_tests clean

pyk/README.md

@@ -0,0 +1,19 @@
+# pyk
+
+
+## Installation
+
+Prerequsites: `python 3.8.*`, `pip >= 20.0.2`.
+
+```bash
+pip install git+https://github.com/runtimeverification/k.git[@<ref>]#subdirectory=pyk
+```
+
+## For Developers
+
+Prerequsite: `virtualenv >= 20.13.4`.
+
+Use `make` to run tests in virtual environments.
+
+* `make`: check code style and run tests in `src/pyk/tests/`.
+* `make test-integration`: run tests in `integration_tests/`.

k-distribution/tests/pyk/Makefile → pyk/integration_tests/Makefile

@@ -1,13 +1,12 @@
-K_RELEASE := $(abspath ../../target/release/k)
-K_BIN     := $(K_RELEASE)/bin
-K_LIB     := $(K_RELEASE)/lib/kframework
+K_ROOT := $(abspath ../..)
+K_BIN  := $(K_ROOT)/k-distribution/target/release/k/bin
 
 KOMPILE = $(K_BIN)/kompile
 KAST    = $(K_BIN)/kast
 KRUN    = $(K_BIN)/krun
 KPROVE  = $(K_BIN)/kprove
 KPROVEX = $(K_BIN)/kprovex
-KPYK    = $(K_BIN)/kpyk
+PYK     = pyk
 
 export PATH := $(K_BIN):$(PATH)
 
@@ -24,21 +23,12 @@ all: test
 
 clean:
 	rm -rf definitions specs
-	rm -rf venv
 
 update-results: CHECK=cp
 update-results: test
 kompile: $(llvm_imp_kompiled) $(haskell_imp_kompiled)
 
 
-# Virtualenv
-
-VENV     := venv/pyvenv.cfg
-ACTIVATE := . venv/bin/activate
-
-$(VENV):
-	virtualenv -p python3.8 venv && $(ACTIVATE) && pip install -e $(K_LIB)/pyk
-
 # Tests
 
 test: test-kpyk test-pytest
@@ -47,14 +37,14 @@ test: test-kpyk test-pytest
 
 test-kpyk: test-kpyk-graphviz test-kpyk-minimize-term
 
-test-kpyk-graphviz: imp-verification/haskell.kompiled $(VENV)
-	$(ACTIVATE) && $(KPYK) definitions/imp-verification/haskell/imp-verification-kompiled graph-imports
+test-kpyk-graphviz: imp-verification/haskell.kompiled
+	$(PYK) definitions/imp-verification/haskell/imp-verification-kompiled graph-imports
 	cat definitions/imp-verification/haskell/imp-verification-kompiled/import-graph | tr -cd '[:alnum:]\n' | grep . | tr '[:lower:]' '[:upper:]' | sort > import-graph.sorted
 	$(CHECK) import-graph.sorted imp-import-graph.expected
 
-test-kpyk-minimize-term: imp-verification/haskell.kompiled $(VENV)
-	$(ACTIVATE) && $(KPYK) definitions/imp-verification/haskell/imp-verification-kompiled prove k-files/imp-verification.k k-files/imp-unproveable-spec.k IMP-UNPROVEABLE-SPEC \
-	    | $(KPYK) definitions/imp-verification/haskell/imp-verification-kompiled print /dev/stdin > imp-unproveable-spec.k.out
+test-kpyk-minimize-term: imp-verification/haskell.kompiled
+	$(PYK) definitions/imp-verification/haskell/imp-verification-kompiled prove k-files/imp-verification.k k-files/imp-unproveable-spec.k IMP-UNPROVEABLE-SPEC \
+	    | $(PYK) definitions/imp-verification/haskell/imp-verification-kompiled print /dev/stdin > imp-unproveable-spec.k.out
 	$(CHECK) imp-unproveable-spec.k.out imp-unproveable-spec.k.expected
 
 ## pytests
@@ -73,8 +63,8 @@ simple_proofs_test.py.pytest:  FILE_DEPS = simple-proofs/haskell.kompiled
 test-pytest: $(pytests:=.pytest)
 
 .SECONDEXPANSION:
-%.pytest: % $$(FILE_DEPS) $(VENV)
-	$(ACTIVATE) && python3 -m unittest $<
+%.pytest: % $$(FILE_DEPS)
+	python3 -m unittest $<
 
 ## proofs to turn to json ahead of time
 

k-distribution/tests/pyk/defn_test.py → pyk/integration_tests/defn_test.py

@@ -1,28 +1,22 @@
-import json
-import os
-import shutil
-from pathlib import Path
-
 from kprove_test import KProveTest
+
 from pyk.kast import (
     KApply,
-    KAtt,
     KClaim,
-    KRequire,
     KRewrite,
-    KRule,
     KToken,
     KVariable,
     assocWithUnit,
     constLabel,
 )
-from pyk.kastManip import pushDownRewrites, rewriteAnywhereWith, simplifyBool
+from pyk.kastManip import pushDownRewrites, simplifyBool
 from pyk.prelude import boolToken, intToken
 
+
 class DefnTest(KProveTest):
     DEFN_DIR = 'definitions/imp-verification/haskell/imp-verification-kompiled'
     MAIN_FILE_NAME = 'imp-verification.k'
-    USE_DIR = f'.defn-test'
+    USE_DIR = '.defn-test'
     INCLUDE_DIRS = ['k-files']
 
     @staticmethod
@@ -33,15 +27,15 @@ def _update_symbol_table(symbol_table):
     def test_print_configuration(self):
         # Given
         config = KApply('<T>', [KApply('<k>', [KApply('int_;_', [KApply('_,_', [KToken('x', 'Id'), KApply('_,_', [KToken('y', 'Id'), KApply('.List{"_,_"}')])])])]), KApply('<state>', [KApply('.Map')])])
-        config_expected = '\n'.join([ '<T>'
-                                    , '  <k>'
-                                    , '    int x , y ;'
-                                    , '  </k>'
-                                    , '  <state>'
-                                    , '    .Map'
-                                    , '  </state>'
-                                    , '</T>'
-                                    ])
+        config_expected = '\n'.join([ '<T>'              # noqa
+                                    , '  <k>'            # noqa
+                                    , '    int x , y ;'  # noqa
+                                    , '  </k>'           # noqa
+                                    , '  <state>'        # noqa
+                                    , '    .Map'         # noqa
+                                    , '  </state>'       # noqa
+                                    , '</T>'             # noqa
+                                    ])                   # noqa
 
         # When
         config_actual = self.kprove.prettyPrint(config)
@@ -51,22 +45,23 @@ def test_print_configuration(self):
 
     def test_print_prove_rewrite(self):
         # Given
-        claim_rewrite = KRewrite( KApply('<T>', [ KApply('<k>', [KApply('_+_', [KVariable('X'), KVariable('Y')])])
-                                                , KApply('<state>', [KVariable('STATE')])
-                                                ])
-                                , KApply('<T>', [ KApply('<k>', [KApply('_+Int_', [KVariable('X'), KVariable('Y')])])
-                                                , KApply('<state>', [KVariable('STATE')])
-                                                ])
-                                )
-        minimized_claim_rewrite_expected = '\n'.join([ '<T>'
-                                                     , '  <k>'
-                                                     , '    ( X + Y => X +Int Y )'
-                                                     , '  </k>'
-                                                     , '  <state>'
-                                                     , '    STATE'
-                                                     , '  </state>'
-                                                     , '</T>'
-                                                     ])
+        claim_rewrite = KRewrite( KApply('<T>', [ KApply('<k>', [KApply('_+_', [KVariable('X'), KVariable('Y')])])     # noqa
+                                                , KApply('<state>', [KVariable('STATE')])                              # noqa
+                                                ])                                                                     # noqa
+                                , KApply('<T>', [ KApply('<k>', [KApply('_+Int_', [KVariable('X'), KVariable('Y')])])  # noqa
+                                                , KApply('<state>', [KVariable('STATE')])                              # noqa
+                                                ])                                                                     # noqa
+                                )                                                                                      # noqa
+
+        minimized_claim_rewrite_expected = '\n'.join([ '<T>'                        # noqa
+                                                     , '  <k>'                      # noqa
+                                                     , '    ( X + Y => X +Int Y )'  # noqa
+                                                     , '  </k>'                     # noqa
+                                                     , '  <state>'                  # noqa
+                                                     , '    STATE'                  # noqa
+                                                     , '  </state>'                 # noqa
+                                                     , '</T>'                       # noqa
+                                                     ])                             # noqa
 
         # When
         minimized_claim_rewrite = pushDownRewrites(claim_rewrite)

k-distribution/tests/pyk/emit_json_spec_test.py → pyk/integration_tests/emit_json_spec_test.py

@@ -2,10 +2,11 @@
 from pathlib import Path
 
 from kprove_test import KProveTest
+
 from pyk.kast import (
     EMPTY_ATT,
-    KAst,
     KApply,
+    KAst,
     KClaim,
     KDefinition,
     KRequire,

k-distribution/tests/pyk/kprove_test.py → pyk/integration_tests/kprove_test.py

@@ -3,7 +3,7 @@
 from abc import ABC, abstractmethod
 from itertools import chain
 from pathlib import Path
-from typing import List, final
+from typing import List
 from unittest import TestCase
 
 from pyk.ktool import KProve

k-distribution/tests/pyk/parse_kast_test.py → pyk/integration_tests/parse_kast_test.py

@@ -1,7 +1,7 @@
 from abc import ABC
 from unittest import TestCase
 
-from pyk.kast import KAs, KDefinition, KRule, KSort, KSortSynonym, readKastTerm
+from pyk.kast import KAs, KDefinition, KSort, KSortSynonym, readKastTerm
 
 
 class ParseKAstTest(TestCase, ABC):

k-distribution/tests/pyk/simple_proofs_test.py → pyk/integration_tests/simple_proofs_test.py

@@ -1,7 +1,5 @@
-import json
-from pathlib import Path
-
 from kprove_test import KProveTest
+
 from pyk.kast import KApply, KAtt, KClaim, KRule, KToken, KVariable
 from pyk.kastManip import rewriteAnywhereWith
 
@@ -20,7 +18,7 @@ def test_prove_claim_with_lemmas(self):
         # Given
         new_lemma = KRule(KToken('pred1(3) => true', 'Bool'), requires=KToken('pred1(4)', 'Bool'), att=KAtt(atts={'simplification': ''}))
         new_claim = KClaim(KToken('<k> foo => bar ... </k> <state> 3 |-> 3 </state>', 'TCellFragment'), requires=KToken('pred1(4)', 'Bool'))
-        
+
         # When
         result1 = self.kprove.proveClaim(new_claim, 'claim-without-lemma')
         result2 = self.kprove.proveClaim(new_claim, 'claim-with-lemma', lemmas=[new_lemma])