From 798ed5fbf299da8f2ad44aa5b74fdb7f64752ff7 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Thu, 28 May 2026 09:57:15 +0100
Subject: [PATCH] =?UTF-8?q?chore(v=E2=86=92zig):=20delete=20legacy=20V-lan?=
 =?UTF-8?q?g=20API=20shim=20(api/v/echidna.v)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Per estate-wide owner directive (2026-05-28): Zig is the default for
APIs/FFIs; Idris2 owns ABIs. The deleted file was a thin V wrapper around
the existing Zig FFI at ffi/zig/. With V removed from the estate, the
Zig FFI is the canonical API surface — no replacement needed.

NOTE: this repo retains Coq .v files at examples/ and tests/live_goals/
(theorem-prover input fixtures). Those are not V-lang and are exempted in
the hypatia banned_language_vlang rule's path_allow_prefixes.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 api/v/echidna.v | 69 -------------------------------------------------
 1 file changed, 69 deletions(-)
 delete mode 100644 api/v/echidna.v

diff --git a/api/v/echidna.v b/api/v/echidna.v
deleted file mode 100644
index 0f6d6223..00000000
--- a/api/v/echidna.v
+++ /dev/null
@@ -1,69 +0,0 @@
-// SPDX-License-Identifier: MPL-2.0
-// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-//
-// ECHIDNA zig API — Multi-backend theorem prover client.
-module echidna
-
-pub enum ProverBackend {
-	coq
-	lean4
-	idris2
-	z3
-	hol4
-	hol_light
-	isabelle
-	mizar
-	metamath
-	pvs
-	agda
-	acl2
-}
-
-pub enum ProofStatus {
-	proven
-	disproven
-	timeout
-	@error
-	unknown
-}
-
-pub struct ProofRequest {
-pub:
-	goal       string
-	hypotheses []string
-	backend    ProverBackend
-	timeout_ms int
-}
-
-pub struct ProofResult {
-pub:
-	status     ProofStatus
-	proof_text string
-	backend    ProverBackend
-	time_ms    int
-}
-
-fn C.echidna_prove(goal_ptr &u8, backend int, timeout_ms int) int
-fn C.echidna_valid_backend(backend int) int
-fn C.echidna_backend_count() int
-
-// prove submits a proof goal to the specified backend.
-pub fn prove(req ProofRequest) ProofResult {
-	result := C.echidna_prove(req.goal.str, int(req.backend), req.timeout_ms)
-	return ProofResult{
-		status: unsafe { ProofStatus(result) }
-		proof_text: ''
-		backend: req.backend
-		time_ms: 0
-	}
-}
-
-// is_valid_backend checks if a backend ID is supported.
-pub fn is_valid_backend(backend ProverBackend) bool {
-	return C.echidna_valid_backend(int(backend)) == 1
-}
-
-// backend_count returns the number of supported prover backends.
-pub fn backend_count() int {
-	return C.echidna_backend_count()
-}