Skip to content

Commit 7fcb6ef

Browse files
committed
ci: adopt canonical Julia ABI-FFI gate (estate standard, matches verisimiser) in place of the interim Bash port
1 parent 890973f commit 7fcb6ef

3 files changed

Lines changed: 124 additions & 114 deletions

File tree

.github/workflows/abi-ffi-gate.yml

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,15 @@ jobs:
2121
runs-on: ubuntu-latest
2222
steps:
2323
- uses: actions/checkout@v4
24+
- name: Install Julia 1.11.5
25+
run: |
26+
curl -fsSL https://julialang-s3.julialang.org/bin/linux/x64/1.11/julia-1.11.5-linux-x86_64.tar.gz -o /tmp/julia.tar.gz
27+
tar -xf /tmp/julia.tar.gz -C /tmp
28+
echo "/tmp/julia-1.11.5/bin" >> "$GITHUB_PATH"
2429
- name: Run ABI-FFI gate
25-
run: bash scripts/abi-ffi-gate.sh
30+
run: |
31+
julia --version # confirms the pinned 1.11.5 is on PATH, not the runner default
32+
julia scripts/abi-ffi-gate.jl
2633
2734
zig-build:
2835
name: Zig FFI builds + tests (Zig 0.14.0)

scripts/abi-ffi-gate.jl

Lines changed: 116 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
#!/usr/bin/env julia
2+
# SPDX-License-Identifier: MPL-2.0
3+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
4+
#
5+
# abi-ffi-gate.jl — fail (exit 1) if the Zig FFI does not conform to the Idris2
6+
# ABI. The Idris2 ABI is the source of truth. Checks, with no compile toolchain
7+
# needed (pure base-Julia text analysis):
8+
#
9+
# 1. the Zig FFI carries no unrendered `{{...}}` template tokens;
10+
# 2. every `%foreign "C:<name>"` symbol declared anywhere in the ABI .idr
11+
# sources is exported by the Zig FFI (`export fn <name>`);
12+
# 3. the Zig `Result = enum(c_int)` and the Idris `resultToInt` agree on BOTH
13+
# names and integer values (the `Error`/`err` spelling is treated as one).
14+
#
15+
# Usage: julia scripts/abi-ffi-gate.jl [repo_root] (defaults to cwd)
16+
#
17+
# Julia port of the former scripts/abi-ffi-gate.py (Python is banned estate-wide,
18+
# RSR-H4); behaviour is identical.
19+
20+
"camelCase / PascalCase → snake_case (insert `_` before each non-initial capital)."
21+
camel_to_snake(s) = lowercase(replace(s, r"(?<!^)(?=[A-Z])" => "_"))
22+
23+
"Canonical result-code key: lowercased, with `err`/`error` unified to `error`."
24+
function canon_rc(name)
25+
n = lowercase(name)
26+
(n == "err" || n == "error") ? "error" : n
27+
end
28+
29+
"Return {variant => value} for the C-ABI `Result` enum (the `enum(c_int)` block whose `ok = 0`), or empty."
30+
function find_result_enum(zig::AbstractString)
31+
best = Dict{String,Int}()
32+
for m in eachmatch(r"enum\s*\(\s*c_int\s*\)\s*\{(.*?)\}"s, zig)
33+
body = m.captures[1]
34+
variants = Dict{String,Int}()
35+
for vm in eachmatch(r"@?\"?([A-Za-z_][A-Za-z0-9_]*)\"?\s*=\s*(\d+)", body)
36+
variants[canon_rc(vm.captures[1])] = parse(Int, vm.captures[2])
37+
end
38+
# The Result enum is the one starting at ok = 0.
39+
if get(variants, "ok", nothing) == 0 && length(variants) > length(best)
40+
best = variants
41+
end
42+
end
43+
return best
44+
end
45+
46+
"Collect every `*.idr` under `abi_dir`, skipping any `build/` output directory."
47+
function idr_sources(abi_dir::AbstractString)
48+
files = String[]
49+
isdir(abi_dir) || return files
50+
for (root, _dirs, fs) in walkdir(abi_dir)
51+
occursin("/build/", root * "/") && continue
52+
for f in fs
53+
endswith(f, ".idr") && push!(files, joinpath(root, f))
54+
end
55+
end
56+
return files
57+
end
58+
59+
function main(root::AbstractString)::Int
60+
name = basename(rstrip(abspath(root), '/'))
61+
abi_dir = joinpath(root, "src/interface/abi")
62+
zig_path = joinpath(root, "src/interface/ffi/src/main.zig")
63+
errs = String[]
64+
65+
idr_files = idr_sources(abi_dir)
66+
if isempty(idr_files)
67+
println("ABI-FFI GATE: SKIP ($name) — no Idris2 ABI .idr files under $abi_dir")
68+
return 0
69+
end
70+
if !isfile(zig_path)
71+
println("ABI-FFI GATE: FAIL ($name) — no Zig FFI at $zig_path")
72+
return 1
73+
end
74+
75+
idr = join((read(p, String) for p in idr_files), "\n")
76+
zig = read(zig_path, String)
77+
78+
# 1. unrendered template tokens
79+
toks = sort(unique(String(m.match) for m in eachmatch(r"\{\{[A-Za-z0-9_]+\}\}", zig)))
80+
isempty(toks) || push!(errs, "Zig FFI has unrendered template tokens: $(toks)")
81+
82+
# 2. foreign C symbols must be exported
83+
csyms = sort(unique(String(m.captures[1]) for m in eachmatch(r"C:([A-Za-z0-9_]+)", idr)))
84+
exports = Set(String(m.captures[1]) for m in eachmatch(r"export fn ([A-Za-z0-9_]+)", zig))
85+
missing_syms = [s for s in csyms if !(s in exports)]
86+
isempty(missing_syms) ||
87+
push!(errs, "$(length(missing_syms)) ABI function(s) not exported by the Zig FFI: $(missing_syms)")
88+
89+
# 3. result-code map (names + values) must agree
90+
idr_rc = Dict{String,Int}()
91+
for m in eachmatch(r"resultToInt\s+([A-Za-z0-9]+)\s*=\s*(\d+)", idr)
92+
idr_rc[canon_rc(camel_to_snake(m.captures[1]))] = parse(Int, m.captures[2])
93+
end
94+
zig_rc = find_result_enum(zig)
95+
if !isempty(idr_rc) && isempty(zig_rc)
96+
push!(errs, "no Zig `enum(c_int)` Result block (with `ok = 0`) found to compare result codes")
97+
elseif !isempty(idr_rc) && !isempty(zig_rc) && idr_rc != zig_rc
98+
push!(errs, "Result-code map differs (name or value):\n" *
99+
" Idris resultToInt: $(sort(collect(idr_rc)))\n" *
100+
" Zig Result enum: $(sort(collect(zig_rc)))")
101+
end
102+
103+
if !isempty(errs)
104+
println("ABI-FFI GATE: FAIL ($name)")
105+
for e in errs
106+
println(" - " * e)
107+
end
108+
return 1
109+
end
110+
println("ABI-FFI GATE: OK ($name) — $(length(csyms)) ABI functions exported, " *
111+
"$(length(idr_rc)) result codes match")
112+
return 0
113+
end
114+
115+
root = length(ARGS) >= 1 ? ARGS[1] : "."
116+
exit(main(root))

scripts/abi-ffi-gate.sh

Lines changed: 0 additions & 113 deletions
This file was deleted.

0 commit comments

Comments
 (0)