Merge remote-tracking branch 'origin/develop' into _update-deps/runti…

…meverification/llvm-backend
runtimeverification · Jan 17, 2024 · d91a5e8 · d91a5e8
2 parents cb498c5 + c41b31c
commit d91a5e8
Show file tree

Hide file tree

Showing 3,538 changed files with 240 additions and 34,913 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -73,6 +73,13 @@ jobs:
           token: ${{ secrets.JENKINS_GITHUB_PAT }}
           submodules: recursive
           path: k-exercises
+      - name: 'Check out pl-tutorial'
+        uses: actions/checkout@v3
+        with:
+          repository: runtimeverification/pl-tutorial
+          token: ${{ secrets.JENKINS_GITHUB_PAT }}
+          submodules: recursive
+          path: k-distribution/pl-tutorial
       - name: 'Tutorial Integration Tests'
         run: |
           docker exec -t k-ci-${GITHUB_SHA} /bin/bash -c 'k-distribution/target/release/k/bin/spawn-kserver kserver.log'

diff --git a/deps/hs-backend-booster_release b/deps/hs-backend-booster_release
@@ -1 +1 @@
-2d2dd7f5572f574175b20d58f4081c947b5c929d
+6067fee77da53ac357ce5d17ad34e4639070804a
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -3,7 +3,7 @@
   inputs = {
     haskell-backend.url = "github:runtimeverification/haskell-backend/ca05f14b7957fec9f2a5ab3444cae01c5a76f12f";
     booster-backend = {
-      url = "github:runtimeverification/hs-backend-booster/2d2dd7f5572f574175b20d58f4081c947b5c929d";
+      url = "github:runtimeverification/hs-backend-booster/6067fee77da53ac357ce5d17ad34e4639070804a";
       inputs.nixpkgs.follows = "haskell-backend/nixpkgs";
       inputs.haskell-backend.follows = "haskell-backend";
       inputs.stacklock2nix.follows = "haskell-backend/stacklock2nix";

diff --git a/hs-backend-booster/src/main/native/hs-backend-booster b/hs-backend-booster/src/main/native/hs-backend-booster
diff --git a/k-distribution/INSTALL.md b/k-distribution/INSTALL.md
@@ -175,27 +175,16 @@ Testing Packages
 The easiest way to test the K package is to copy a K tutorial language and
 check if you can compile and run an included example.
 
-1.  Start by copying the K tutorial to some work directory
-    (e.g. `$HOME/pl-tutorial`) from the K distribution root. Using a Linux
-    package, this command typically will be like:
+1.  Start by cloning the K tutorial from the [K PL Tutorial](https://www.github.com/runtimeverification/pl-tutorial). This command typically will be like:
 
     ```sh
-    $ cp -R /usr/share/kframework/pl-tutorial $HOME/pl-tutorial
+    $ git clone https://www.github.com/runtimeverification/pl-tutorial
     ```
 
-    On macOS/brew, this command typically will be like:
-
-    ```sh
-    $ cp -R /usr/local/share/kframework/pl-tutorial $HOME/pl-tutorial
-    ```
-
-    This step is needed because sometimes only the `root` user can run the
-    examples in the default installation directory.
-
 2.  Now you can try to run some programs:
 
     ```sh
-    $ cd $HOME/pl-tutorial/2_languages/1_simple/1_untyped
+    $ cd pl-tutorial/2_languages/1_simple/1_untyped
     $ make kompile
     $ krun tests/diverse/factorial.simple
     ```
diff --git a/k-distribution/Makefile b/k-distribution/Makefile
@@ -1,3 +1,3 @@
-SUBDIRS=pl-tutorial tests/regression-new tests/builtins/collections
+SUBDIRS=tests/regression-new tests/builtins/collections
 
 include include/kframework/ktest-group.mak
diff --git a/k-distribution/k-tutorial/README.md b/k-distribution/k-tutorial/README.md
@@ -9,7 +9,7 @@ K. While the primary use of K is in the specification of operational semantics
 of programming languages, this tutorial is agnostic on how the knowledge of K
 is used. For a more detailed tutorial explaining the basic principles of
 programming language design, refer to the
-[K PL Tutorial](../pl-tutorial/README.md). Note that that tutorial is somewhat
+[K PL Tutorial](https://www.github.com/runtimeverification/pl-tutorial). Note that that tutorial is somewhat
 out of date presently.
 
 This K tutorial is a work in progress. Many lessons are currently simply

diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/Makefile b/k-distribution/pl-tutorial/1_k/1_lambda/Makefile
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/README.md b/k-distribution/pl-tutorial/1_k/1_lambda/README.md
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/Makefile b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/Makefile
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/NOTES.md b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/NOTES.md
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/README.md b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/README.md
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/lambda.k b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/lambda.k
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/media.properties b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/media.properties
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/tests/closed-variable-capture.lambda.out b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/tests/closed-variable-capture.lambda.out
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/tests/free-variable-capture.lambda.out b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/tests/free-variable-capture.lambda.out
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/tests/omega.lambda b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/tests/omega.lambda
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/tests/omega.lambda.out b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/tests/omega.lambda.out
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/Makefile b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/Makefile
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/NOTES.md b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/NOTES.md
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/lambda.k b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/lambda.k
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/media.properties b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/media.properties
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/tests/closed-variable-capture.lambda.out b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/tests/closed-variable-capture.lambda.out
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/tests/identity.lambda.out b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2.5/tests/identity.lambda.out
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2/Makefile b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2/Makefile
diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2/NOTES.md b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_2/NOTES.md
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		2d2dd7f5572f574175b20d58f4081c947b5c929d
		6067fee77da53ac357ce5d17ad34e4639070804a