Merge branch 'develop' into add-pyk-to-sidebar

.github/actions/with-k-docker/Dockerfile

@@ -5,9 +5,11 @@ FROM ubuntu:${BASE_DISTRO}
 ARG K_DEB_PATH
 ARG INSTALL_BACKEND_DEBS
 ARG LLVM_BACKEND_DEB_PATH
+ARG HASKELL_BACKEND_DEB_PATH
 
 COPY ${K_DEB_PATH} /kframework.deb
 COPY ${LLVM_BACKEND_DEB_PATH} /llvm-backend.deb
+COPY ${HASKELL_BACKEND_DEB_PATH} /haskell-backend.deb
 
 RUN    apt-get -y update    \
     && apt-get -y install   \
@@ -19,7 +21,7 @@ RUN    apt-get -y update    \
          /kframework.deb
 
 RUN if [ "${INSTALL_BACKEND_DEBS}" = "true" ]; then \
-      apt-get -y install /llvm-backend.deb; \
+      apt-get -y install /llvm-backend.deb /haskell-backend.deb; \
     fi
 
 RUN apt-get -y clean

.github/actions/with-k-docker/action.yml

@@ -42,20 +42,28 @@ runs:
       DOCKERFILE=${{ github.action_path }}/Dockerfile
       K_DEB_PATH=${{ inputs.k-deb-path }}
       LLVM_BACKEND_DEB_PATH=llvm-backend.deb
+      HASKELL_BACKEND_DEB_PATH=haskell-backend.deb
 
       gh release download                           \
         --repo runtimeverification/llvm-backend     \
         --pattern "*ubuntu_${BASE_DISTRO}.deb"      \
         --output "${LLVM_BACKEND_DEB_PATH}"         \
         v$(cat deps/llvm-backend_release)
 
+      gh release download                           \
+        --repo runtimeverification/haskell-backend  \
+        --pattern "*ubuntu_${BASE_DISTRO}.deb"      \
+        --output "${HASKELL_BACKEND_DEB_PATH}"      \
+        $(cat deps/haskell-backend_release)
+
       docker build . \
         --file ${DOCKERFILE}                                        \
         --tag ${TAG}                                                \
         --build-arg BASE_DISTRO=${BASE_DISTRO}                      \
         --build-arg K_DEB_PATH=${K_DEB_PATH}                        \
         --build-arg INSTALL_BACKEND_DEBS=${INSTALL_BACKEND_DEBS}    \
-        --build-arg LLVM_BACKEND_DEB_PATH=${LLVM_BACKEND_DEB_PATH}
+        --build-arg LLVM_BACKEND_DEB_PATH=${LLVM_BACKEND_DEB_PATH}  \
+        --build-arg HASKELL_BACKEND_DEB_PATH=${HASKELL_BACKEND_DEB_PATH}
 
   - name: 'Run Docker container'
     shell: bash {0}

package/debian/kframework-frontend/rules.jammy

@@ -23,7 +23,7 @@ export PREFIX
 	dh $@ 
 
 override_dh_auto_build:
-	mvn --batch-mode package -DskipTests -Dllvm.backend.skip
+	mvn --batch-mode package -DskipTests -Dllvm.backend.skip -Dhaskell.backend.skip
 
 override_dh_auto_install:
 	package/package --frontend

pyk/src/pyk/__main__.py

@@ -346,6 +346,7 @@ def exec_kompile(options: KompileCommandOptions) -> None:
             type_inference_mode=options.type_inference_mode,
             warnings=options.warnings,
             warnings_to_errors=options.warnings_to_errors,
+            ignore_warnings=options.ignore_warnings,
             no_exc_wrap=options.no_exc_wrap,
         )
     except RuntimeError as err:

pyk/src/pyk/cli/args.py

@@ -206,6 +206,7 @@ class KompileOptions(Options):
     bison_lists: bool
     no_exc_wrap: bool
     outer_parsed_json: bool
+    ignore_warnings: list[str]
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -230,6 +231,7 @@ def default() -> dict[str, Any]:
             'bison_lists': False,
             'no_exc_wrap': False,
             'outer_parsed_json': False,
+            'ignore_warnings': [],
         }
 
     @staticmethod
@@ -475,6 +477,9 @@ def kompile_args(self) -> ArgumentParser:
             action='store_true',
             help='Do not wrap the output on the CLI.',
         )
+        args.add_argument(
+            '--ignore-warnings', '-Wno', dest='ignore_warnings', action='append', help='Ignore provided warnings'
+        )
         return args
 
     @cached_property

pyk/src/pyk/ktool/kompile.py

@@ -58,6 +58,7 @@ def kompile(
     type_inference_mode: str | TypeInferenceMode | None = None,
     warnings: str | Warnings | None = None,
     warnings_to_errors: bool = False,
+    ignore_warnings: Iterable[str] = (),
     no_exc_wrap: bool = False,
     # ---
     debug: bool = False,
@@ -78,6 +79,7 @@ def kompile(
             type_inference_mode=type_inference_mode,
             warnings=warnings,
             warnings_to_errors=warnings_to_errors,
+            ignore_warnings=ignore_warnings,
             no_exc_wrap=no_exc_wrap,
             debug=debug,
             verbose=verbose,
@@ -96,6 +98,7 @@ def kompile(
         type_inference_mode=type_inference_mode,
         warnings=warnings,
         warnings_to_errors=warnings_to_errors,
+        ignore_warnings=ignore_warnings,
         no_exc_wrap=no_exc_wrap,
         debug=debug,
         verbose=verbose,
@@ -111,6 +114,7 @@ def _booster_kompile(
     type_inference_mode: str | TypeInferenceMode | None,
     warnings: str | Warnings | None,
     warnings_to_errors: bool,
+    ignore_warnings: Iterable[str],
     no_exc_wrap: bool,
     # ---
     debug: bool,
@@ -146,6 +150,7 @@ def kompile_llvm() -> None:
             type_inference_mode=type_inference_mode,
             warnings=warnings,
             warnings_to_errors=warnings_to_errors,
+            ignore_warnings=ignore_warnings,
             no_exc_wrap=no_exc_wrap,
             debug=debug,
             verbose=verbose,
@@ -161,6 +166,7 @@ def kompile_haskell() -> None:
             type_inference_mode=type_inference_mode,
             warnings=warnings,
             warnings_to_errors=warnings_to_errors,
+            ignore_warnings=ignore_warnings,
             no_exc_wrap=no_exc_wrap,
             debug=debug,
             verbose=verbose,
@@ -273,6 +279,7 @@ def __call__(
         type_inference_mode: str | TypeInferenceMode | None = None,
         warnings: str | Warnings | None = None,
         warnings_to_errors: bool = False,
+        ignore_warnings: Iterable[str] = (),
         no_exc_wrap: bool = False,
         debug: bool = False,
         verbose: bool = False,
@@ -321,6 +328,9 @@ def __call__(
         if outer_parsed_json:
             args += ['--outer-parsed-json']
 
+        if ignore_warnings:
+            args += ['-Wno', ','.join(ignore_warnings)]
+
         try:
             proc_res = run_process(args, logger=_LOGGER, cwd=cwd, check=check)
         except CalledProcessError as err: