From 48f4808af3dbf7102b06f63b5bc3557ab5276725 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Wed, 24 Jun 2026 15:44:05 +0100
Subject: [PATCH] =?UTF-8?q?revert(policy):=20Kotlin=20is=20goodbye=20?=
 =?UTF-8?q?=E2=80=94=20remove=20JVM-interop=20carve-out=20(#417)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Reverts the bindings/kotlin + bindings/groovy + clients/jetbrains exemptions
added in #417. There is NO carve-out for hand-written JVM bindings: FFI/interop
must be Idris2-ABI -> Zig FFI (or Idris2 -> C as a last resort). The proven /
proven-servers Kotlin/Java/Groovy bindings are an architecture violation to be
re-done as Zig FFI (owner directing the proven-servers bot). Mobile = Tauri/Dioxus.
Only the minimal Android Java platform shim carve-out remains.
---
 .github/workflows/governance-reusable.yml | 33 +++++++----------------
 1 file changed, 10 insertions(+), 23 deletions(-)

diff --git a/.github/workflows/governance-reusable.yml b/.github/workflows/governance-reusable.yml
index 45784e6b..e429e34d 100644
--- a/.github/workflows/governance-reusable.yml
+++ b/.github/workflows/governance-reusable.yml
@@ -309,29 +309,16 @@ jobs:
           # delegating wrapper (typically <10 LoC) that JNIs into Rust/Zig
           # immediately.
           #
-          # Kotlin/JVM INTEROP carve-out 2026-06-24 (parallel to the TS
-          # `bindings/typescript/` / `bindings/deno/` / `clients/vscode/`
-          # interop carve-outs): Kotlin/Groovy is banned for MOBILE app code
-          # (→ Tauri/Dioxus), but is PERMITTED as consumer-facing JVM interop
-          # — directories where we author bindings that expose an estate
-          # library to JVM consumers, or an IDE-host plugin whose plugin API
-          # is Kotlin-native. Tauri/Dioxus cannot replace a consumer binding
-          # or an editor-host plugin. Three path classes are exempt:
-          #   * **/bindings/kotlin/**  — Kotlin bindings exposing a library to
-          #     JVM consumers (exemplars: proven-servers, proven).
-          #   * **/bindings/groovy/**  — Groovy bindings, same rationale
-          #     (exemplar: proven).
-          #   * **/clients/jetbrains/** — JetBrains IDE plugin; the IntelliJ
-          #     Platform plugin API is Kotlin-native (exemplar:
-          #     universal-language-server-plugin).
-          # Unblock condition: never (consumer binding / editor-host plugin).
-          # `.groovy` is included in the ls-files set ONLY so the carve-out is
-          # explicit and future Groovy bindings outside these dirs are caught.
+          # Kotlin/Groovy: NO JVM-interop exemption (reverted 2026-06-24).
+          # Kotlin is goodbye. There is NO carve-out for hand-written JVM
+          # bindings: FFI/interop to other ecosystems MUST be authored as
+          # Idris2-ABI → Zig FFI/API (Idris2 → C only as an absolute last
+          # resort if Zig genuinely cannot reach the boundary), never as
+          # Kotlin/Java/Groovy `bindings/*`. Mobile uses Tauri/Dioxus. The
+          # only remaining Java carve-out is the minimal Android platform
+          # shim above. `.groovy` is detected so it is banned everywhere.
           JAVA_FILES=$(git ls-files '*.java' '*.kt' '*.kts' '*.groovy' \
-            | grep -vE '(^|/)android/.*/src/.*\.java$' \
-            | grep -vE '(^|/)bindings/kotlin/' \
-            | grep -vE '(^|/)bindings/groovy/' \
-            | grep -vE '(^|/)clients/jetbrains/' || true)
+            | grep -vE '(^|/)android/.*/src/.*\.java$' || true)
           SWIFT_FILES=$(git ls-files '*.swift' || true)
           DART_FILES=$(git ls-files '*.dart' 'pubspec.yaml' || true)
           # V-lang detected by manifest (v.mod / vpkg.json); the .v extension
@@ -344,7 +331,7 @@ jobs:
           enforce "Go files" "use Rust/WASM instead" "$GO_FILES"
           enforce "Python files" "Python is fully banned — use AffineScript/Rust/SPARK/Julia (SaltStack carveout removed 2026-01-03)" "$PY_FILES"
           enforce "Makefiles" "use Mustfile/justfile instead" "$MAKE_FILES"
-          enforce "Java/Kotlin/Groovy files" "use Rust/Tauri/Dioxus instead (consumer JVM interop is exempt under bindings/kotlin, bindings/groovy, clients/jetbrains)" "$JAVA_FILES"
+          enforce "Java/Kotlin/Groovy files" "Kotlin is goodbye — apps use Tauri/Dioxus; FFI/interop must be Idris2-ABI -> Zig FFI (or Idris2 -> C as a last resort), NOT hand-written JVM bindings" "$JAVA_FILES"
           enforce "Swift files" "use Tauri/Dioxus instead" "$SWIFT_FILES"
           enforce "Flutter/Dart files" "use Tauri/Dioxus instead (Google lock-in)" "$DART_FILES"
           enforce "V-lang manifests (v.mod / vpkg.json)" "V-lang is banned since 2026-04-10 — migrate to Zig" "$VMOD_FILES"