From 088232b7780719ef7705cf6ab043ae8756a34f59 Mon Sep 17 00:00:00 2001 From: Yogthos Date: Sat, 13 Jun 2026 13:46:16 -0400 Subject: [PATCH] feat: success checker on by default in direct-link builds, free (jolt audit) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Checking inherently needs an inference pass (~2.6x compile as a standalone pass). But direct-link builds ALREADY run one inference pass for specialization (run-passes' infer-top), so checking can ride along: set a check-mode flag, turn checking? on during that existing pass, and collect the diagnostics after — ~2% overhead measured on the ray tracer, vs 2.6x for the separate pass. So the checker now defaults to `warn` in direct-link builds (where it's nearly free) and stays OFF in plain REPL/dev builds (no inference to ride, no forced cost — opt in with JOLT_TYPE_CHECK there). JOLT_TYPE_CHECK still overrides in both directions (off to disable, error to escalate). It checks the POST-optimization IR, which matches what the optimized program actually evaluates — scalar-replace only drops provably-pure code, an accepted opt-mode divergence, so no real error is hidden. The loaders enable position tracking whenever checking will run (env-selected or direct-link). type-check! (the standalone pass) stays for plain builds; both paths share report-diags!. cli-test pins: plain build silent, direct-link warns by default, JOLT_TYPE_CHECK=off disables. Gate green, suite 4718, runtime bench even. --- jolt-core/jolt/passes.clj | 27 ++++++++++- src/jolt/api.janet | 6 ++- src/jolt/backend.janet | 84 +++++++++++++++++++++------------ src/jolt/evaluator.janet | 2 +- src/jolt/loader.janet | 2 +- test/integration/cli-test.janet | 25 ++++++++++ 6 files changed, 111 insertions(+), 35 deletions(-) diff --git a/jolt-core/jolt/passes.clj b/jolt-core/jolt/passes.clj index dd21a17..7b69114 100644 --- a/jolt-core/jolt/passes.clj +++ b/jolt-core/jolt/passes.clj @@ -1311,6 +1311,21 @@ (get fnode :arities)))) def-node))) +;; Piggyback checking (jolt audit). In direct-link mode infer-top already runs +;; one inference pass for specialization; turning checking? on during it makes +;; the success checker nearly free there (no extra traversal — just the +;; per-call error-domain predicates). The back end sets the mode before +;; run-passes and reads take-diags! after. It checks the POST-optimization IR, +;; which matches what the optimized program actually evaluates (scalar-replace +;; only drops provably-pure code, an accepted opt-mode divergence). +(def ^:private check-mode-box (atom {:on false :strict false})) +(defn set-check-mode! + "Enable/disable checking during the next run-passes inference (direct-link)." + [on strict?] (reset! check-mode-box {:on (if on true false) :strict (if strict? true false)})) +(defn take-diags! + "Diagnostics accumulated by the last checking run-passes; clears the buffer." + [] (let [d (vec @diag-box)] (reset! diag-box []) d)) + (defn run-passes "All passes, in order. The back end applies this to every analyzed form. When inlining is enabled for the unit (user code under direct-linking, jolt-87f), @@ -1327,5 +1342,15 @@ (if (and @dirty (< i 8)) (recur (inc i) n2) n2)))] - (infer-top opt)) + ;; specialization inference, optionally also emitting success diagnostics + (if (get @check-mode-box :on) + (do (reset! diag-box []) + (reset! checking-box #{}) + (reset! strict-box (get @check-mode-box :strict)) + (reset! checking? true) + (let [r (infer-top opt)] + (reset! checking? false) + (reset! strict-box false) + r)) + (infer-top opt))) (const-fold node))) diff --git a/src/jolt/api.janet b/src/jolt/api.janet index c657829..e935f3a 100644 --- a/src/jolt/api.janet +++ b/src/jolt/api.janet @@ -369,8 +369,10 @@ Returns the result of the last form evaluated." [ctx s &opt file] (default file "") - # record form positions so the checker can report file:line:col (jolt-fqy) - (when (checker-enabled?) + # record form positions so the checker can report file:line:col (jolt-fqy). + # The checker is on when JOLT_TYPE_CHECK selects it, OR by default in + # direct-link builds (where it piggybacks on inference for free). + (when (or (checker-enabled?) (get (ctx :env) :inline?)) (track-positions! true) (put (ctx :env) :tc-source s) (put (ctx :env) :tc-file file)) diff --git a/src/jolt/backend.janet b/src/jolt/backend.janet index 5181eb5..91de6d8 100644 --- a/src/jolt/backend.janet +++ b/src/jolt/backend.janet @@ -613,13 +613,32 @@ [ctx] (build-compiler! ctx)) -(defn type-check! - "Success-type check the analyzed IR (RFC 0006). Looks up jolt.passes/check-form - (absent during pre-passes bootstrap -> no-op), runs it protected so a checker - bug never breaks compilation, then reports each diagnostic per strictness: +(defn- report-diags! + "Render and emit success-type diagnostics (RFC 0006) at the given strictness: `warn` prints to stderr, `error` throws (failing this form's compilation). - Because the checker only fires on PROVABLY-wrong code, a correct program has - nothing to report under either level. + file:line:col when the diagnostic carries an offset and the source is on the + env (jolt-fqy); else the ns." + [ctx diags strictness ns] + (def src (get (ctx :env) :tc-source)) + (def file (or (get (ctx :env) :tc-file) (and ns (string ns)))) + (each d diags + (def off (get d :pos)) + (def loc + (if (and off src) + (let [lc (r/line-col src off)] + (string (or file "?") ":" (in lc 0) ":" (in lc 1))) + (string "in " (if ns (string ns) "?")))) + (def msg (string "type error " loc ": " (get d :msg))) + (if (= strictness "error") + (error msg) + (eprint " " msg)))) + +(defn type-check! + "Decoupled success-type check (RFC 0006): run jolt.passes/check-form as its OWN + inference pass over `ir` and report. Used in NON-direct-link builds, where the + optimization inference doesn't run — so checking costs a separate pass. (In + direct-link builds checking piggybacks on run-passes' inference instead, near + free; see analyze-form.) Protected so a checker bug never breaks compilation. JOLT_TYPE_CHECK_USER (an orthogonal opt-in knob, jolt-zo1) additionally reports calls to user functions whose concrete argument types provably make @@ -633,23 +652,7 @@ (when (r 0) (def diags (if (pv/pvec? (r 1)) (pv/pv->array (r 1)) (r 1))) (when (and diags (> (length diags) 0)) - # source + file for offset -> line:col (jolt-fqy). The loader stashes the - # current file's source + path on the env when checking is on. - (def src (get (ctx :env) :tc-source)) - (def file (or (get (ctx :env) :tc-file) (and ns (string ns)))) - (each d diags - (def off (get d :pos)) - # precise: file:line:col of the offending form when its offset and the - # source are both available; else the ns (no worse than before) - (def loc - (if (and off src) - (let [lc (r/line-col src off)] - (string (or file "?") ":" (in lc 0) ":" (in lc 1))) - (string "in " (if ns (string ns) "?")))) - (def msg (string "type error " loc ": " (get d :msg))) - (if (= strictness "error") - (error msg) - (eprint " " msg))))))) + (report-diags! ctx diags strictness ns))))) (defn analyze-form "Run the portable Clojure analyzer (jolt.analyzer/analyze) on a reader form, @@ -683,6 +686,21 @@ # Resolved lazily; absent during the pre-passes bootstrap window. (def pv (unless (= "1" (os/getenv "JOLT_NO_IR_PASSES")) (ns-find (ctx-find-ns ctx "jolt.passes") "run-passes"))) + # Success-type checking level (RFC 0006). JOLT_TYPE_CHECK wins when set; + # otherwise it defaults to `warn` in direct-link builds — where the + # optimization inference already runs, so checking piggybacks on it for nearly + # free — and stays OFF for plain REPL/dev builds (no inference -> no free ride; + # opt in with JOLT_TYPE_CHECK there). (jolt audit) + (def tc (os/getenv "JOLT_TYPE_CHECK")) + (def tc-off (or (= tc "off") (= tc "0"))) + (def direct-link? (if (get (ctx :env) :inline?) true false)) + (def level (cond tc-off nil tc tc direct-link? "warn" true nil)) + (def uenv (os/getenv "JOLT_TYPE_CHECK_USER")) + (def strict? (and uenv (not= uenv "0") (not= uenv "off") true)) + # piggyback: check DURING run-passes' inference (direct-link, the cheap path) + (def piggyback? (and level direct-link? pv true)) + (def scm (and piggyback? (ns-find (ctx-find-ns ctx "jolt.passes") "set-check-mode!"))) + (when scm ((var-get scm) true strict?)) (def result (if pv (let [pr (protect ((var-get pv) (r 1) ctx))] @@ -692,13 +710,19 @@ (ctx-set-current-ns ctx saved-ns) (if (pr 0) (pr 1) (r 1))) (r 1))) - # Success-type check (RFC 0006), decoupled from specialization: runs whenever - # JOLT_TYPE_CHECK is warn/error, regardless of :inline?. Read at runtime so it - # needs no rebuild. The analyzed IR (r 1) carries no specialization; the - # checker does its own inference. - (def tc (os/getenv "JOLT_TYPE_CHECK")) - (when (and tc (not= tc "off") (not= tc "0")) - (type-check! ctx (r 1) tc saved-ns)) + (when scm ((var-get scm) false false)) + (cond + # direct-link: collect the diagnostics infer-top emitted and report them + piggyback? + (let [td (ns-find (ctx-find-ns ctx "jolt.passes") "take-diags!")] + (when td + (def raw ((var-get td))) + (def diags (if (pv/pvec? raw) (pv/pv->array raw) raw)) + (when (and diags (> (length diags) 0)) + (report-diags! ctx diags level saved-ns)))) + # plain build with checking explicitly requested: a separate inference pass + (and level (not direct-link?)) + (type-check! ctx (r 1) level saved-ns)) result) # The analyzer's deliberate punt signal — (uncompilable why) throws the string diff --git a/src/jolt/evaluator.janet b/src/jolt/evaluator.janet index 72cc465..ff68c25 100644 --- a/src/jolt/evaluator.janet +++ b/src/jolt/evaluator.janet @@ -377,7 +377,7 @@ (def toplevel (get (ctx :env) :toplevel-eval)) # a require runs nested inside an outer file's eval; save/restore the outer # checker source so its later forms still convert offsets correctly (jolt-fqy) - (def checking (checker-enabled?)) + (def checking (or (checker-enabled?) (get (ctx :env) :inline?))) (def saved-src (and checking (get (ctx :env) :tc-source))) (def saved-file (and checking (get (ctx :env) :tc-file))) (when checking diff --git a/src/jolt/loader.janet b/src/jolt/loader.janet index d7e2028..7c82476 100644 --- a/src/jolt/loader.janet +++ b/src/jolt/loader.janet @@ -112,7 +112,7 @@ (load-ns ctx filepath) → namespace symbol string" [ctx filepath] (def source (slurp filepath)) - (when (checker-enabled?) + (when (or (checker-enabled?) (get (ctx :env) :inline?)) (track-positions! true) (put (ctx :env) :tc-source source) (put (ctx :env) :tc-file filepath)) diff --git a/test/integration/cli-test.janet b/test/integration/cli-test.janet index 8b490f6..d45e96d 100644 --- a/test/integration/cli-test.janet +++ b/test/integration/cli-test.janet @@ -118,6 +118,31 @@ r) (has "could not find method")) +# --- success checker default-on in direct-link, off in plain builds ---------- +# A provably-wrong defn (never called, so no runtime error): the checker is the +# only thing that can flag it. Plain build = silent (no dev regression); +# direct-link build = warns by default (free piggyback on inference). +(def tcw (string (or (os/getenv "TMPDIR") "/tmp") "/jolt-tcwarn-" (os/time) ".clj")) +(spit tcw "(ns tcw)\n\n(defn unused [s]\n (inc \"definitely-not-a-number\"))\n") +(check "plain build does not run the checker (no regression)" + (run-err tcw) + (fn [s] (nil? (string/find "type error" s)))) +(check "direct-link build warns by default (free checking)" + (do (os/setenv "JOLT_DIRECT_LINK" "1") + (def r (run-err tcw)) + (os/setenv "JOLT_DIRECT_LINK" nil) + r) + (fn [s] (and (string/find "type error" s) + (string/find "requires a number" s)))) +(check "JOLT_TYPE_CHECK=off disables it even in direct-link" + (do (os/setenv "JOLT_DIRECT_LINK" "1") + (os/setenv "JOLT_TYPE_CHECK" "off") + (def r (run-err tcw)) + (os/setenv "JOLT_DIRECT_LINK" nil) + (os/setenv "JOLT_TYPE_CHECK" nil) + r) + (fn [s] (nil? (string/find "type error" s)))) + (if (> fails 0) (error (string "cli-test: " fails " failing check(s)")) (print "\nAll CLI tests passed!"))