Merge branch 'develop' into _update-deps/runtimeverification/llvm-bac…

…kend

deps/haskell-backend_release

@@ -1 +1 @@
-v0.1.14
+v0.1.19

flake.nix

@@ -1,7 +1,7 @@
 {
   description = "K Framework";
   inputs = {
-    haskell-backend.url = "github:runtimeverification/haskell-backend/v0.1.14";
+    haskell-backend.url = "github:runtimeverification/haskell-backend/v0.1.19";
     nixpkgs.follows = "llvm-backend/nixpkgs";
     flake-utils.url = "github:numtide/flake-utils";
     llvm-backend = {

pyk/Makefile

@@ -67,7 +67,7 @@ profile: poetry-install
 # Checks and formatting
 
 format: autoflake isort black
-check: check-flake8 check-mypy check-autoflake check-isort check-black
+check: check-flake8 check-mypy check-autoflake check-isort check-pydocstyle check-black
 
 check-flake8: poetry-install
 	$(POETRY_RUN) flake8 src
@@ -87,6 +87,9 @@ isort: poetry-install
 check-isort: poetry-install
 	$(POETRY_RUN) isort --check src
 
+check-pydocstyle:
+	$(POETRY_RUN) pydocstyle src
+
 black: poetry-install
 	$(POETRY_RUN) black src
 

pyk/docs/conf.py

@@ -19,6 +19,7 @@
     'sphinx.ext.autodoc',
     'sphinx.ext.napoleon',
     'sphinx.ext.viewcode',
+    'sphinx_rtd_theme',
 ]
 templates_path = ['_templates']
 exclude_patterns = []
@@ -34,5 +35,5 @@
 # -- Options for HTML output -------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#options-for-html-output
 
-html_theme = 'alabaster'
+html_theme = 'sphinx_rtd_theme'
 html_static_path = ['_static']

pyk/docs/generate.sh

@@ -21,7 +21,7 @@ source $VENV_DIR/bin/activate
 
 pip install --upgrade pip
 pip install --editable $PYK_DIR
-pip install sphinx==$SPHINX_VERSION
+pip install sphinx==$SPHINX_VERSION sphinx_rtd_theme
 
 # Generate and install _kllvm
 PYTHON_LIB=$(find $VENV_DIR -name 'site-packages' -type d)

pyk/flake.nix

@@ -2,7 +2,8 @@
   description = "Application packaged using poetry2nix";
 
   inputs = {
-    nixpkgs.url = "github:NixOS/nixpkgs";
+    rv-utils.url = "github:runtimeverification/rv-nix-tools";
+    nixpkgs.follows = "rv-utils/nixpkgs";
     poetry2nix = {
       url =
         "github:nix-community/poetry2nix/626111646fe236cb1ddc8191a48c75e072a82b7c";
@@ -11,7 +12,7 @@
     flake-utils.follows = "poetry2nix/flake-utils";
   };
 
-  outputs = { self, nixpkgs, flake-utils, poetry2nix }:
+  outputs = { self, nixpkgs, flake-utils, rv-utils, poetry2nix }:
     {
       # Nixpkgs overlay providing the application
       overlay = final: prev:

pyk/pyproject.toml

@@ -39,6 +39,7 @@ flake8-type-checking = "*"
 isort = "*"
 mypy = "*"
 pep8-naming = "*"
+pydocstyle = "*"
 pytest = "*"
 pytest-cov = "*"
 pytest-mock = "*"
@@ -58,6 +59,11 @@ kore-exec-covr = "pyk.kore_exec_covr.__main__:main"
 [tool.poetry.plugins.pytest11]
 pytest-pyk = "pyk.testing.plugin"
 
+[tool.pydocstyle]
+convention = "google"
+add-select = "D204,D401,D404"
+add-ignore = "D1"
+
 [tool.isort]
 profile = "black"
 line_length = 120

pyk/src/pyk/__main__.py

@@ -218,9 +218,9 @@ def pretty_print_execute_response(execute_result: ExecuteResult) -> list[str]:
 
 
 def exec_rpc_kast(options: RPCKastOptions) -> None:
-    """
-    Convert an 'execute' JSON RPC response to a new 'execute' or 'simplify' request,
-    copying parameters from a reference request.
+    """Convert an 'execute' JSON RPC response to a new 'execute' or 'simplify' request.
+
+    Copies parameters from a reference request.
     """
     reference_request = json.loads(options.reference_request_file.read())
     input_dict = json.loads(options.response_file.read())

pyk/src/pyk/coverage.py

@@ -16,14 +16,13 @@
 def get_rule_by_id(definition: KDefinition, rule_id: str) -> KRule:
     """Get a rule from the definition by coverage rule id.
 
-    Input:
+    Args:
+        definition: JSON-encoded definition.
+        rule_id: String of unique rule identifier generated by `kompile --coverage`.
 
-        -   definition: json encoded definition.
-        -   rule_id: string of unique rule identifier generated by `kompile --coverage`.
-
-    Output: json encoded rule which has identifier rule_id.
+    Returns:
+        JSON encoded rule which has identifier `rule_id`.
     """
-
     for module in definition.modules:
         for sentence in module.sentences:
             if type(sentence) is KRule:
@@ -52,16 +51,15 @@ def translate_coverage(
 ) -> list[str]:
     """Translate the coverage data from one kompiled definition to another.
 
-    Input:
-
-        -   src_all_rules: contents of allRules.txt for definition which coverage was generated for.
-        -   dst_all_rules: contents of allRules.txt for definition which you desire coverage for.
-        -   dst_definition: JSON encoded definition of dst kompiled definition.
-        -   src_rules_list: Actual coverage data produced.
+    Args:
+        src_all_rules: Contents of allRules.txt for definition which coverage was generated for.
+        dst_all_rules: Contents of allRules.txt for definition which you desire coverage for.
+        dst_definition: JSON encoded definition of dst kompiled definition.
+        src_rules_list: Actual coverage data produced.
 
-    Output: list of non-functional rules applied in dst definition translated from src definition.
+    Returns:
+        List of non-functional rules applied in dst definition translated from src definition.
     """
-
     # Load the src_rule_id -> src_source_location rule map from the src kompiled directory
     src_rule_map = {}
     for line in src_all_rules:
@@ -110,13 +108,13 @@ def translate_coverage(
 def translate_coverage_from_paths(src_kompiled_dir: str, dst_kompiled_dir: str, src_rules_file: PathLike) -> list[str]:
     """Translate coverage information given paths to needed files.
 
-    Input:
-
-        -   src_kompiled_dir: Path to kompiled directory of source.
-        -   dst_kompiled_dir: Path to kompiled directory of destination.
-        -   src_rules_file: Path to generated rules coverage file.
+    Args:
+        src_kompiled_dir: Path to kompiled directory of source.
+        dst_kompiled_dir: Path to kompiled directory of destination.
+        src_rules_file: Path to generated rules coverage file.
 
-    Output: Translated list of rules with non-semantic rules stripped out.
+    Returns:
+        Translated list of rules with non-semantic rules stripped out.
     """
     src_all_rules = []
     with open(src_kompiled_dir + '/allRules.txt') as src_all_rules_file: