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

…kend
runtimeverification · Nov 2, 2023 · c251164 · c251164
2 parents a734555 + 47ee46f
commit c251164
Show file tree

Hide file tree

Showing 296 changed files with 34,686 additions and 29,325 deletions.
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -102,7 +102,7 @@ jobs:
         with:
           os: ubuntu
           distro: jammy
-          llvm: 14
+          llvm: 15
           pkg-name: kframework_amd64_ubuntu_jammy.deb
           build-package: package/debian/build-package jammy
           test-package: package/debian/test-package
@@ -236,18 +236,18 @@ jobs:
         id: checkout
         with:
           repository: runtimeverification/homebrew-k
+          token: ${{ secrets.JENKINS_GITHUB_PAT }}
           path: homebrew-k
           ref: staging
-          persist-credentials: false
         continue-on-error: true
 
       - name: 'Check out homebrew repo master branch'
         uses: actions/checkout@v3
         if: ${{ steps.checkout.outcome == 'failure' }}
         with:
           repository: runtimeverification/homebrew-k
+          token: ${{ secrets.JENKINS_GITHUB_PAT }}
           path: homebrew-k
-          persist-credentials: false
 
       - name: 'Download bottle'
         uses: actions/download-artifact@v2
@@ -300,19 +300,16 @@ jobs:
           version=$(cat k-homebrew-checkout/package/version)
           mv homebrew-k-old/${BOTTLE_NAME} homebrew-k-old/${REMOTE_BOTTLE_NAME}
           gh release upload --repo runtimeverification/k --clobber v${version} homebrew-k-old/${REMOTE_BOTTLE_NAME}
-      # Deprecate After Homebrew tap migration
-      - name: 'Add ssh key'
-        uses: shimataro/ssh-key-action@v2
-        with:
-          key: ${{ secrets.HOMEBREW_SSH_KEY }}
-          known_hosts: ${{ secrets.KNOWN_HOSTS_GITHUB_COM }}
+
+      - run: |
+          git config --global user.name rv-jenkins
+          git config --global user.email [email protected]
 
       - name: 'Commit changes'
         run: |
           cp homebrew-k-old/Formula/kframework.rb homebrew-k/Formula/kframework.rb
           cd homebrew-k
           git commit -m 'Update brew package version' Formula/kframework.rb
-          git remote set-url origin [email protected]:runtimeverification/homebrew-k.git
           git push origin master
 
       - name: 'Delete Release'
@@ -352,7 +349,7 @@ jobs:
           tag: k-release-ci-${{ github.sha }}
           os: ubuntu
           distro: jammy
-          llvm: 14
+          llvm: 15
 
       - name: 'Push Maven Packages'
         shell: bash {0}

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -29,10 +29,32 @@ jobs:
             git push origin HEAD:${GITHUB_HEAD_REF}
           fi
 
+  format-check:
+    name: 'Check Java code formatting'
+    runs-on: ubuntu-latest
+    needs: version-sync
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v3
+        with:
+          token: ${{ secrets.JENKINS_GITHUB_PAT }}
+          # fetch-depth 0 means deep clone the repo
+          fetch-depth: 0
+      - name: 'Set up Java 17'
+        uses: actions/setup-java@v3
+        with:
+          distribution: 'zulu'
+          java-version: 17
+      - name: 'Check code is formatted correctly'
+        uses: axel-op/googlejavaformat-action@v3
+        with:
+          version: 1.18.1
+          args: "--dry-run --set-exit-if-changed"
+
   nix-maven:
     name: 'Nix: Maven'
     runs-on: ubuntu-20.04
-    needs: version-sync
+    needs: format-check
     steps:
 
       - name: 'Check out code, set up Git'
@@ -75,7 +97,7 @@ jobs:
   test-k:
     name: 'K Tests'
     runs-on: [self-hosted, linux, normal]
-    needs: version-sync
+    needs: format-check
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
@@ -87,7 +109,7 @@ jobs:
           tag: k-ci-${{ github.sha }}
           os: ubuntu
           distro: jammy
-          llvm: 14
+          llvm: 15
       - name: 'Build and Test K'
         run: docker exec -t k-ci-${GITHUB_SHA} /bin/bash -c 'mvn verify --batch-mode -U'
       - name: 'Check out k-exercises'
@@ -112,15 +134,15 @@ jobs:
   test-package-ubuntu-jammy:
     name: 'K Ubuntu Jammy Package'
     runs-on: [self-hosted, linux, normal]
-    needs: version-sync
+    needs: format-check
     steps:
       - uses: actions/checkout@v3
       - name: 'Build and Test'
         uses: ./.github/actions/test-package
         with:
           os: ubuntu
           distro: jammy
-          llvm: 14
+          llvm: 15
           build-package: package/debian/build-package jammy
           test-package: package/debian/test-package
       - name: On Failure, Upload the kore-exec.tar.gz file to the Summary Page

diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -11,7 +11,7 @@
     nixpkgs.follows = "haskell-backend/nixpkgs";
     flake-utils.url = "github:numtide/flake-utils";
     mavenix = {
-      url = "github:nix-community/mavenix";
+      url = "github:goodlyrottenapple/mavenix";
       inputs.nixpkgs.follows = "haskell-backend/nixpkgs";
       inputs.utils.follows = "flake-utils";
     };
@@ -34,7 +34,7 @@
     let
       allOverlays = [
         (_: _: {
-          llvm-version = 13;
+          llvm-version = 15;
           llvm-backend-build-type = "Release"; })
         mavenix.overlay
         llvm-backend.overlays.default
@@ -144,6 +144,7 @@
             ${pkgs.nix}/bin/nix-build --no-out-link -E 'import ./nix/flake-compat-k-unwrapped.nix' \
               || echo "^~~~ expected error"
 
+            export PATH="${pkgs.gnused}/bin:$PATH"
             ${pkgs.mavenix-cli}/bin/mvnix-update -l ./nix/mavenix.lock -E 'import ./nix/flake-compat-k-unwrapped.nix'
           '';
 

diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java
@@ -2,83 +2,83 @@
 package org.kframework.backend.haskell;
 
 import com.google.inject.Inject;
+import java.io.IOException;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
 import org.kframework.attributes.Att;
 import org.kframework.backend.kore.KoreBackend;
 import org.kframework.compile.Backend;
 import org.kframework.kompile.KompileOptions;
 import org.kframework.main.GlobalOptions;
 import org.kframework.main.Tool;
 import org.kframework.utils.Stopwatch;
-import org.kframework.utils.errorsystem.KExceptionManager;
 import org.kframework.utils.errorsystem.KEMException;
+import org.kframework.utils.errorsystem.KExceptionManager;
 import org.kframework.utils.file.FileUtil;
 
-import java.io.IOException;
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.List;
-import java.util.Set;
-import java.util.HashSet;
-
 public class HaskellBackend extends KoreBackend {
 
-    private final KompileOptions kompileOptions;
-    private final GlobalOptions globalOptions;
-    private final FileUtil files;
-    private final HaskellKompileOptions haskellKompileOptions;
-
-    @Inject
-    public HaskellBackend(
-            KompileOptions kompileOptions,
-            GlobalOptions globalOptions,
-            HaskellKompileOptions haskellKompileOptions,
-            FileUtil files,
-            KExceptionManager kem,
-            Tool tool) {
-        super(kompileOptions, files, kem, false, tool);
-        this.files = files;
-        this.haskellKompileOptions = haskellKompileOptions;
-        this.kompileOptions = kompileOptions;
-        this.globalOptions = globalOptions;
-    }
+  private final KompileOptions kompileOptions;
+  private final GlobalOptions globalOptions;
+  private final FileUtil files;
+  private final HaskellKompileOptions haskellKompileOptions;
 
+  @Inject
+  public HaskellBackend(
+      KompileOptions kompileOptions,
+      GlobalOptions globalOptions,
+      HaskellKompileOptions haskellKompileOptions,
+      FileUtil files,
+      KExceptionManager kem,
+      Tool tool) {
+    super(kompileOptions, files, kem, false, tool);
+    this.files = files;
+    this.haskellKompileOptions = haskellKompileOptions;
+    this.kompileOptions = kompileOptions;
+    this.globalOptions = globalOptions;
+  }
 
-    @Override
-    public void accept(Backend.Holder h) {
-        Stopwatch sw = new Stopwatch(globalOptions);
-        String kore = getKompiledString(h.def, true);
-        h.def = null;
-        files.saveToKompiled("definition.kore", kore);
-        sw.printIntermediate("  Print definition.kore");
-        ProcessBuilder pb = files.getProcessBuilder();
-        List<String> args = new ArrayList<>();
-        if (haskellKompileOptions.noHaskellBinary) {
-            args.add("kore-parser");
-            args.add("--no-print-definition");
-            args.add("definition.kore");
-        } else {
-            args.add(haskellKompileOptions.haskellBackendCommand);
-            args.add("definition.kore");
-            args.add("--module");
-            args.add(kompileOptions.mainModule(files));
-            args.add("--output");
-            args.add("haskellDefinition.bin");
-            args.add("--serialize");
-        }
-        try {
-          Process p = pb.command(args).directory(files.resolveKompiled(".")).inheritIO().start();
-          int exit = p.waitFor();
-          if (exit != 0) {
-              throw KEMException.criticalError("Haskell backend reported errors validating compiled definition.\nExamine output to see errors.");
-          }
-        } catch (IOException | InterruptedException e) {
-            throw KEMException.criticalError("Error with I/O while executing kore-parser", e);
-        }
-        sw.printIntermediate("  Validate def");
+  @Override
+  public void accept(Backend.Holder h) {
+    Stopwatch sw = new Stopwatch(globalOptions);
+    String kore = getKompiledString(h.def, true);
+    h.def = null;
+    files.saveToKompiled("definition.kore", kore);
+    sw.printIntermediate("  Print definition.kore");
+    ProcessBuilder pb = files.getProcessBuilder();
+    List<String> args = new ArrayList<>();
+    if (haskellKompileOptions.noHaskellBinary) {
+      args.add("kore-parser");
+      args.add("--no-print-definition");
+      args.add("definition.kore");
+    } else {
+      args.add(haskellKompileOptions.haskellBackendCommand);
+      args.add("definition.kore");
+      args.add("--module");
+      args.add(kompileOptions.mainModule(files));
+      args.add("--output");
+      args.add("haskellDefinition.bin");
+      args.add("--serialize");
     }
-
-    @Override
-    public Set<Att.Key> excludedModuleTags() {
-        return new HashSet<>(Arrays.asList(Att.CONCRETE(), Att.KAST()));
+    try {
+      Process p = pb.command(args).directory(files.resolveKompiled(".")).inheritIO().start();
+      int exit = p.waitFor();
+      if (exit != 0) {
+        throw KEMException.criticalError(
+            "Haskell backend reported errors validating compiled definition.\n"
+                + "Examine output to see errors.");
+      }
+    } catch (IOException | InterruptedException e) {
+      throw KEMException.criticalError("Error with I/O while executing kore-parser", e);
     }
+    sw.printIntermediate("  Validate def");
+  }
+
+  @Override
+  public Set<Att.Key> excludedModuleTags() {
+    return new HashSet<>(Arrays.asList(Att.CONCRETE(), Att.KAST()));
+  }
 }