[1/2] Defer tactic argument rendering until trace dump

[Wilson1211]

Summary

• store tactic argument renderers as Lazy.t
• force arguments only for tactic records retained until exptrace_dump
• leave conversion argument rendering unchanged

This first PR intentionally contains only the core implementation: one commit and one changed file.

Stack

1. This PR: core lazy tactic-argument implementation.
2. PR #2: focused evaluation-timing regression test, Makefile integration, generated-test ignores, and README documentation.

PR #2 is a draft based on main. After this PR merges, GitHub will remove the shared core commit from PR #2, leaving only its test and documentation diff.

Motivation

Tactic argument rendering can dominate trace collection when a tactic has reached its record limit. The current replacement path renders the arguments for every candidate before sorting, even when that candidate is immediately discarded.

A downstream s2n-bignum experiment with relaxed retention limits measured:

• mldsa_caddq: 1,549 s -> 639 s (2.4x faster), with all 414 trace files byte-for-byte identical
• bignum_mux: 160 s -> 162 s, with all 352 trace files byte-for-byte identical

The experiment report and breakdown are available in sep17-report.md.

Validation

• built tracer and types_test with OCaml 5.4
• ran the existing tactic and conversion examples through the full wrapper/compile/link pipeline
• compared generated traces with examples/*.answer; both suites matched
• PR [2/2] Add regression coverage for lazy tactic arguments #2 adds a focused regression proving insertion remains lazy, discarded candidates are never rendered, and retained arguments are rendered once during dump

Scope and known risk

This PR changes tactic records only. Conversion records remain eager and should be considered separately.

Lazy rendering observes HOL Light printer settings at dump time rather than at tactic execution time. The two downstream proof comparisons above produced identical output, but they do not prove equivalence for proofs that change printer settings between recording and dumping. This PR remains a draft so that this tradeoff and any additional validation can be reviewed before merge.