From 5c7ea358dcdbb44a1f0d469f00f7ad85bc50bdf8 Mon Sep 17 00:00:00 2001
From: Radu Mereuta <headness13@gmail.com>
Date: Thu, 14 Dec 2023 20:42:41 +0200
Subject: [PATCH] Add -kompiled dir readme (#3873)

Fixes: #3869
Please let me know if I missed something.
This will be added to every -kompiled dir.
---
 .../kframework/kompile/KompileFrontEnd.java   | 12 +++++
 .../org/kframework/utils/file/README.md       | 48 +++++++++++++++++++
 2 files changed, 60 insertions(+)
 create mode 100644 kernel/src/main/resources/org/kframework/utils/file/README.md

diff --git a/kernel/src/main/java/org/kframework/kompile/KompileFrontEnd.java b/kernel/src/main/java/org/kframework/kompile/KompileFrontEnd.java
index f6da03a19f3..8bc831e1451 100644
--- a/kernel/src/main/java/org/kframework/kompile/KompileFrontEnd.java
+++ b/kernel/src/main/java/org/kframework/kompile/KompileFrontEnd.java
@@ -4,6 +4,10 @@
 import com.google.inject.Inject;
 import com.google.inject.Module;
 import com.google.inject.Provider;
+import java.io.BufferedReader;
+import java.io.IOException;
+import java.io.InputStreamReader;
+import java.net.URL;
 import java.util.ArrayList;
 import java.util.List;
 import org.kframework.compile.Backend;
@@ -93,6 +97,14 @@ public int run() {
     kompile = null;
     files.get().saveToKompiled("mainModule.txt", def.executionModule().name());
     files.get().saveToKompiled("mainSyntaxModule.txt", def.mainSyntaxModuleName());
+    try {
+      URL rdmUrl = JarInfo.class.getResource("README.md");
+      if (rdmUrl != null) {
+        String rdm = FileUtil.read(new BufferedReader(new InputStreamReader(rdmUrl.openStream())));
+        files.get().saveToKompiled("README.md", rdm);
+      }
+    } catch (IOException ignored) {
+    }
     sw.printIntermediate("Kompile to kore");
     loader.saveOrDie(files.get().resolveKompiled("compiled.bin"), def);
     files.get().saveToKompiled("backend.txt", options.backend); // used by the krun script
diff --git a/kernel/src/main/resources/org/kframework/utils/file/README.md b/kernel/src/main/resources/org/kframework/utils/file/README.md
new file mode 100644
index 00000000000..a90ed11a71b
--- /dev/null
+++ b/kernel/src/main/resources/org/kframework/utils/file/README.md
@@ -0,0 +1,48 @@
+---
+copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+---
+
+Description of files contained in the `-kompiled` directory.
+While most files are binaries, some are user readable and contain useful debugging information.
+Most notably `parsed.txt` and `compiled.txt`.
+
+Some temporary files can also be inspected by running the tools with `--debug`, `--temp-dir <dir>`
+or `--save-temps`. Users are encouraged to use the PYK library to efficiently interact with these
+files.
+
+List of files:
+- `parsed.txt` - user readable definition as seen by kompile immediately after parsing.
+- `compiled.txt` - user readable definition after all the kompile steps have been applied. Variable
+  renaming, configuration concretization, macro expansion, extra sorts and rules... This is
+  what the backend will take as input.
+- `parsed.json`, `compiled.json` - same as above but as JSON. Useful for loading into pyk.
+  Generated when `--emit-json` is provided.
+- `definition.kore` - the actual input for the backends - a close reflection of compiled.txt
+- helper files for the scripts:
+  - `backend.txt` - the backend used to kompile: haskell|llvm
+  - `mainModule.txt` - main module name
+  - `mainSyntaxModule.txt` - main syntax module name
+  - `allRules.txt` - a hash list for all the rules
+  - `configVars.sh` - the list of configuration variables, used by krun to initialize the config
+  - `macros.kore` - macros to apply after parsing
+- `cache.bin` - parsing cache. A mapping from bubble to the AST returned by the parser. On
+  subsequent kompile calls only the newly modified rules will be parsed. This is the main file
+  used by the KLSP to find occurrences and go to definition.
+- `compiled.bin` - the entire definition as a binary dump from Java. Used by `kprove`.
+- `scanner` - the tokenizer used by the parser.
+- `timestamp` -  used by make to determine if it needs to rekompile.
+- `haskellDefintion.bin` - haskell backend only. Binary format of definition.kore for efficient
+  loading in the backend.
+- `interpreter` - llvm backend only. Executable called by krun for concrete execution.
+- `dt` folder - llvm temporary files to calculate the decision tree fast matching algorithm.
+- `kore-exec.tar.gz` - archive with the input of the haskell backend in case it crashes. Useful
+  for submitting bug reports.
+
+Note 1: right now, we need to kompile the definition separately for each backend because the
+compilation pipeline is very rigid. The differences between the backends start right from the very
+first step, choosing what modules to include. That affects the syntax/functions/hooks available
+in your definition, and mixing those can cause the backends to crash or, worse, give unsound
+results.
+
+Note 2: the content and the format of these files are subject to change without warning and they
+should not be relied on for automation outside of what is already tested on CI.