Initial commit

1 files changed, 30 insertions, 0 deletions

diff --git a/generate-status-object.php b/generate-status-object.php
new file mode 100644
index 0000000..9d19070
--- /dev/null
+++ b/generate-status-object.php
@@ -0,0 +1,30 @@
+<?php
+
+if (empty($argv[1])) {
+    file_put_contents("php://stderr", "No runner ID specified");
+    exit(1);
+}
+
+define("WORK_DIR", __DIR__ . "/_runners/" . $argv[1] . "/results");
+
+function get(string $name): ?string {
+    $file = WORK_DIR . "/" . $name;
+    if (!is_file($file))
+        return null;
+    return file_get_contents($file);
+}
+
+$data = [
+    "compile" => [
+        "status" => get("c.s"),
+        "stdout" => get("c.0"),
+        "stderr" => get("c.1"),
+    ],
+    "run" => [
+        "status" => get("r.s"),
+        "stdout" => get("r.0"),
+        "stderr" => get("r.1"),
+    ],
+];
+
+echo json_encode($data, JSON_UNESCAPED_SLASHES | JSON_PRETTY_PRINT) . PHP_EOL;