Move PL tutorial link out of main "learn K" section (#3717)

Partially addresses #3704 by de-emphasising the PL tutorial on the main K webpage. Happy to bikeshed the specific placement and wording used here. --------- Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Oct 19, 2023 · 350dc5e · 350dc5e
1 parent 2ea8c60
commit 350dc5e
Show file tree

Hide file tree

Showing 6 changed files with 21 additions and 1 deletion.
diff --git a/k-distribution/pl-tutorial/1_k/5_types/lesson_4/lambda.k b/k-distribution/pl-tutorial/1_k/5_types/lesson_4/lambda.k
@@ -1,5 +1,9 @@
 // Copyright (c) K Team. All Rights Reserved.
 
+// NOTE: this definition is not up to date with the latest version of K, as it
+// uses both substitution and symbolic reasoning.
+// It is intended for documentation and academic purposes only.
+
 require "substitution.md"
 
 module LAMBDA

diff --git a/k-distribution/pl-tutorial/1_k/5_types/lesson_7/lambda.k b/k-distribution/pl-tutorial/1_k/5_types/lesson_7/lambda.k
@@ -1,5 +1,9 @@
 // Copyright (c) K Team. All Rights Reserved.
 
+// NOTE: this definition is not up to date with the latest version of K, as it
+// uses both substitution and symbolic reasoning.
+// It is intended for documentation and academic purposes only.
+
 require "substitution.md"
 
 module LAMBDA

diff --git a/k-distribution/pl-tutorial/1_k/5_types/lesson_8/lambda.k b/k-distribution/pl-tutorial/1_k/5_types/lesson_8/lambda.k
@@ -1,5 +1,9 @@
 // Copyright (c) K Team. All Rights Reserved.
 
+// NOTE: this definition is not up to date with the latest version of K, as it
+// uses both substitution and symbolic reasoning.
+// It is intended for documentation and academic purposes only.
+
 require "substitution.md"
 
 module LAMBDA

diff --git a/k-distribution/pl-tutorial/1_k/5_types/lesson_9.5/lambda.k b/k-distribution/pl-tutorial/1_k/5_types/lesson_9.5/lambda.k
@@ -1,5 +1,9 @@
 // Copyright (c) K Team. All Rights Reserved.
 
+// NOTE: this definition is not up to date with the latest version of K, as it
+// uses substitution, unification and symbolic reasoning.
+// It is intended for documentation and academic purposes only.
+
 require "unification.k"
 require "substitution.md"
 

diff --git a/k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k b/k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k
@@ -1,5 +1,9 @@
 // Copyright (c) K Team. All Rights Reserved.
 
+// NOTE: this definition is not up to date with the latest version of K, as it
+// uses both unification and symbolic reasoning.
+// It is intended for documentation and academic purposes only.
+
 require "unification.k"
 
 module LAMBDA

diff --git a/web/pages/index.md b/web/pages/index.md
@@ -27,7 +27,6 @@ call/cc.
 ## Learn K
 
 - <a href="/k-distribution/k-tutorial/README.md">Do the K Tutorial!</a>
-- <a href="/k-distribution/pl-tutorial/README.md">Build programming languages in K!</a>
 - <a href="/docs/user_manual.md">Reference Documentation</a>
 - <a href="/docs/cheat_sheet.md">K Cheat Sheet</a>
 - <a href="/docs/ktools.md">K Tool Reference</a>
@@ -41,6 +40,7 @@ call/cc.
 
 ## Resources
 
+- A set of <a href="/k-distribution/pl-tutorial/README.md">reference implementations and tutorials</a> for common programming language features and paradigms is available, although parts of these implementations may not be fully up to date with modern K features.
 - Read some papers about K on the [Formal Systems Laboratory (FSL)](https://fsl.cs.illinois.edu/publications/).
 - [Matching logic](http://matching-logic.org/) webpage at UIUC (USA).
 - A ten-minute overview video [slide presentation](./overview.md).