Merge remote-tracking branch 'origin/develop'

runtimeverification · Jan 16, 2024 · d86e735 · d86e735
2 parents 044e141 + 0d49f11
commit d86e735
Show file tree

Hide file tree

Showing 3,534 changed files with 233 additions and 34,906 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/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