Update simple-untyped to work with the modern backends.

.github/workflows/master-push.yml

@@ -39,17 +39,17 @@ jobs:
         uses: cachix/cachix-action@v10
         with:
           name: k-framework
-          signingKey: '${{ secrets.RV_DEVOPS_CACHIX_TOKEN }}'
+          authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
           skipPush: true
 
       - name: 'Build and cache K Framework'
         uses: workflow/nix-shell-action@v3
         env:
           GC_DONT_GC: 1
-          CACHIX_AUTH_TOKEN: '${{ secrets.RV_DEVOPS_CACHIX_TOKEN }}'
+          CACHIX_AUTH_TOKEN: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
         with:
           packages: jq
           script: |
             k=$(nix build .#k --json | jq -r '.[].outputs | to_entries[].value')
             drv=$(nix-store --query --deriver ${k})
-            nix-store --query --requisites --include-outputs ${drv} | cachix push k-framework
+            nix-store --query --requisites --include-outputs ${drv} | cachix push k-framework

.github/workflows/test-pr.yml

@@ -55,8 +55,8 @@ jobs:
       - name: 'Install Cachix'
         uses: cachix/cachix-action@v10
         with:
-          name: runtimeverification
-          signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
+          name: k-framework
+          authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
           skipPush: true
 
       - name: 'Update Maven dependencies, push changes'
@@ -155,9 +155,8 @@ jobs:
         if: ${{ !startsWith(matrix.os, 'self') }}
         uses: cachix/cachix-action@v10
         with:
-          name: runtimeverification
-          extraPullNames: kore
-          signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
+          name: k-framework
+          authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
 
       - name: 'Build K Framework'
         run: GC_DONT_GC=1 nix build .
@@ -191,20 +190,18 @@ jobs:
         run: brew install bash
 
       - name: 'Install Nix'
-        if: ${{ !startsWith(matrix.os, 'self') }}
         uses: cachix/install-nix-action@v14.1
         with:
-          install_url: 'https://releases.nixos.org/nix/nix-2.3.16/install'
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
+            substituters = http://cache.nixos.org https://cache.iog.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@v10
         with:
-          name: runtimeverification
-          extraPullNames: kore
-          signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
+          name: k-framework
+          authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
 
       - name: 'Build K Framework'
         run: nix-build -A k -A llvm-backend -A haskell-backend

.github/workflows/update-deps.yml

@@ -36,9 +36,8 @@ jobs:
       - name: 'Install Cachix'
         uses: cachix/cachix-action@v10
         with:
-          name: runtimeverification
-          extraPullNames: kore
-          signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
+          name: k-framework
+          authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
 
       - name: 'Update Nix flake inputs from submodules'
         run: |

k-distribution/pl-tutorial/2_languages/1_simple/1_untyped/Makefile

@@ -2,8 +2,8 @@ MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
 DEF=simple-untyped
 EXT=simple
 TESTDIR=tests/*
-KOMPILE_FLAGS=--transition strict
-KOMPILE_BACKEND?=java
+KOMPILE_FLAGS=--enable-search
+KOMPILE_BACKEND?=llvm
 KRUN_FLAGS=--output none --smt none
 
 include $(MAKEFILE_PATH)/../../../find-k.mak

k-distribution/pl-tutorial/2_languages/1_simple/1_untyped/exercises/break-continue/tests/diverse/div-nondet.simple.out

@@ -1,7 +1,17 @@
-  S ==K "0\n"
+  {
+    S:String
+  #Equals
+    "1\n"
+  }
 #Or
-  S ==K "1\n"
+  {
+    S:String
+  #Equals
+    "2\n"
+  }
 #Or
-  S ==K "2\n"
-#Or
-  S ==K "3\n"
+  {
+    S:String
+  #Equals
+    "3\n"
+  }

k-distribution/pl-tutorial/2_languages/1_simple/1_untyped/exercises/break-continue/tests/exceptions/exceptions_07.simple.out

@@ -1,3 +1,11 @@
-  S ==K "2 5\n"
+  {
+    S:String
+  #Equals
+    "2 5\n"
+  }
 #Or
-  S ==K "2 6\n"
+  {
+    S:String
+  #Equals
+    "2 6\n"
+  }

k-distribution/pl-tutorial/2_languages/1_simple/1_untyped/exercises/break-continue/tests/threads/threads_01.simple.out

@@ -1,3 +1,11 @@
-  S ==K "5\n"
+  {
+    S:String
+  #Equals
+    "5\n"
+  }
 #Or
-  S ==K "7\n"
+  {
+    S:String
+  #Equals
+    "7\n"
+  }

k-distribution/pl-tutorial/2_languages/1_simple/1_untyped/exercises/break-continue/tests/threads/threads_02.simple.out

@@ -1,3 +1,11 @@
-  S ==K "5\n"
+  {
+    S:String
+  #Equals
+    "5\n"
+  }
 #Or
-  S ==K "7\n"
+  {
+    S:String
+  #Equals
+    "7\n"
+  }

k-distribution/pl-tutorial/2_languages/1_simple/1_untyped/exercises/break-continue/tests/threads/threads_04.simple.out

@@ -1,3 +1,23 @@
-  S ==K "2 3 "
+  {
+    S:String
+  #Equals
+    "2 3 "
+  }
 #Or
-  S ==K "3 2 "
+  {
+    S:String
+  #Equals
+    "3 2 "
+  }
+#Or
+  {
+    S:String
+  #Equals
+    "23  "
+  }
+#Or
+  {
+    S:String
+  #Equals
+    "32  "
+  }