From 350dc5e6e4d2ae03c33c0e2cb74d6ad60fbb207c Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Thu, 19 Oct 2023 10:42:46 +0100 Subject: [PATCH] Move PL tutorial link out of main "learn K" section (#3717) Partially addresses https://github.com/runtimeverification/k/issues/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 --- k-distribution/pl-tutorial/1_k/5_types/lesson_4/lambda.k | 4 ++++ k-distribution/pl-tutorial/1_k/5_types/lesson_7/lambda.k | 4 ++++ k-distribution/pl-tutorial/1_k/5_types/lesson_8/lambda.k | 4 ++++ k-distribution/pl-tutorial/1_k/5_types/lesson_9.5/lambda.k | 4 ++++ k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k | 4 ++++ web/pages/index.md | 2 +- 6 files changed, 21 insertions(+), 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 index d5321436a09..97be6dd994d 100644 --- 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 index 5f5dec6bcda..ea120a67caa 100644 --- 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 index 2a6009f34a6..4e6c2558c35 100644 --- 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 index ff09a894ab2..207bd60f618 100644 --- 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 index 0d6dba1770f..1cf1cf4f033 100644 --- 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 index 856c99d10c8..07fd8c62480 100644 --- a/web/pages/index.md +++ b/web/pages/index.md @@ -27,7 +27,6 @@ call/cc. ## Learn K - Do the K Tutorial! -- Build programming languages in K! - Reference Documentation - K Cheat Sheet - K Tool Reference @@ -41,6 +40,7 @@ call/cc. ## Resources +- A set of reference implementations and tutorials 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).