chore(training): EchidnaML CUDA logging fix + 2026-06-02 run doc

docs/training-runs/2026-06-02.md

@@ -0,0 +1,91 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-->
+
+# GNN training run — 2026-06-02
+
+First owner-authorised GNN training run after the post-wave3 wiring
+PR landed (#207, merged 2026-06-02T04:14:04Z).
+
+## Provenance
+
+| Field | Value |
+|---|---|
+| Branch | `gnn-training-run-2026-06-02` (local-only, no main pollution per Option 4) |
+| Worktree | `/home/hyperpolymath/developer/repos/echidna-training-2026-06-02` |
+| Launcher | `/tmp/echidna-training-launcher.sh` |
+| Log | `/tmp/echidna-training-2026-06-02.log` |
+| Status file | `/tmp/echidna-training-2026-06-02.status` |
+| Pre-requisite PRs merged | #198 saturation+typing, #206 wave3 closeout, #207 GNN wiring, #210 JSON dep fix |
+| Hardware | 4 CPU / 5GB RAM / WSL2 with CUDA passthrough (libcuda.so.535.309.01) |
+| Julia | 1.12.6 via juliaup |
+
+## Pipeline
+
+1. **Stage 0** — `Pkg.instantiate()` to verify Julia env
+2. **Stage 1** — `just provision-corpora` (shallow clones of all upstream sources to `external_corpora/`)
+3. **Stage 2** — loop over 17 saturation adapters via `just corpus-ingest-saturation <name> training_data/<name>/`
+4. **Stage 3** — `just train-from-corpus lean`
+5. **Stage 4** — `just train-from-corpus coq`
+6. **Stage 5** — list `models/neural/` artefacts
+
+## Run outcomes (filled in as stages complete)
+
+### Stage 0 — Julia env
+
+- _2026-06-02T10:46:36Z_ — `Pkg.status()` green; 14 direct deps + JSON (added in #210)
+
+### Stage 1 — provision-corpora
+
+- _2026-06-02T10:46:55Z_ — **43 upstream corpora present** (idempotent cache hits after v2 run)
+- Known per-source failures: several GitLab sources return `Gitlab::GitAccess::NotFoundError`; matita returns 404 (rocq-prover/matita repo unavailable). Non-fatal — script tolerates per-source failures.
+
+### Stage 2 — ingest 17 adapters
+
+- _2026-06-02T10:48:05Z_ — **4 of 17 adapters ingested**: `agda`, `coq` confirmed; lean + idris2 expected.
+- Known cause for the 13 failures: `corpus-ingest-saturation` recipe (Justfile:988) only knows the 4 dependent-typed provers. The other 13 (`isabelle`, `metamath`, `mizar`, `hol_light`, `hol4`, `dafny`, `why3`, `fstar`, `acl2_books`, `tptp`, `smtlib`, `proofnet`, `minif2f`) need per-adapter ingest scripts written. Sketch §7 promised 17; reality is 4. Tracked as roadmap follow-up.
+
+### Stage 3 — train-from-corpus lean
+
+- _TBD_ — first run blocked on Julia `JSON` dep (fixed in #210); awaiting v3 run completion.
+- Wall-clock target: ~10min CPU baseline / ~2hr GPU on small corpus
+
+### Stage 4 — train-from-corpus coq
+
+- _TBD_
+
+### Stage 5 — artefacts
+
+- _TBD_ — should populate `models/neural/`. Existing `models/neural/` in the local checkout's wave3 worktree has prior weights; this run uses the dedicated branch worktree so artefacts don't pollute main.
+
+## Outcomes summary
+
+- **Models produced**: _TBD_
+- **MRR vs cosine baseline**: _TBD_
+- **Comparable to wave3 baseline**: _TBD — needs side-by-side once wave3 lands its first GNN run_
+
+## Known issues discovered this run
+
+1. **JSON dep mismatch** — fixed via #210. `corpus_loader.jl` uses `JSON.parse` but `Project.toml` had only `JSON3`.
+2. **`CUDA.version()` MethodError** — cosmetic logging error; CUDA.jl 5.x removed the method. Fixed via this PR.
+3. **`corpus-ingest-saturation` 4-vs-17 gap** — known; tracked separately.
+
+## Follow-up tickets
+
+- (TBD if needed) Extend `corpus-ingest-saturation` recipe to all 17 adapters — large scope, requires per-adapter Rust extractor scripts.
+- (TBD) Compare `models/neural/` outputs vs wave3 baseline once both land.
+
+## Re-running
+
+Owner-side re-run after corpus refresh:
+```bash
+just provision-corpora extract-corpora
+for adapter in agda coq lean idris2; do
+    just corpus-ingest-saturation "$adapter" "training_data/$adapter/"
+done
+just train-from-corpus lean
+just train-from-corpus coq
+```
+
+Note `extract-corpora` is a *separate* recipe call — not a positional arg to `provision-corpora` (that was an early-run mistake; cost 1 launcher iteration).

src/julia/EchidnaML.jl

@@ -198,7 +198,15 @@ function __init__()
     # Check CUDA availability
     if CUDA.functional()
         @info "CUDA available - using GPU acceleration"
-        @info "CUDA version: $(CUDA.version())"
+        # CUDA.jl 5.x uses runtime_version() / driver_version();
+        # legacy CUDA.version() was removed. Wrap defensively so a
+        # logging-only probe can't kill the init path.
+        try
+            @info "CUDA runtime version: $(CUDA.runtime_version())"
+            @info "CUDA driver version: $(CUDA.driver_version())"
+        catch e
+            @debug "CUDA version probe failed (non-fatal)" exception=e
+        end
         @info "Device: $(CUDA.device())"
     else
         @info "CUDA not available - using CPU"