[fix] I/P: Forward SMT/ATP solver env vars to the remote ML process

[david-wang-0]

Fixes #273.

Problem

ip/ml_proxy.py builds the remote poly process environment from a filtered dump of the remote's isabelle env, keeping only ISABELLE_|ML_|POLYML_ variables. This drops Z3_SOLVER, CVC5_SOLVER and friends — and Isabelle decides SMT-solver availability by a pure env probe inside the ML process (HOL/Tools/SMT/smt_systems.ML: getenv (name ^ "_SOLVER") <> ""). So under the proxy every such proof fails with The SMT solver "z3" is not installed (the message names the requested solver), even though the solvers are installed on the remote. The same filter hides the sledgehammer ATPs (E_HOME, SPASS_HOME, VAMPIRE_HOME, ZIPPERPOSITION_HOME) and the nitpick/quickcheck backends (KODKODI*, MINISAT_HOME, …). smt (verit) was unaffected because its probe is keyed on ISABELLE_VERIT, which already passed the filter.

Fix

Widen the allowlist to the bundled prover/counterexample-generator prefixes. The forwarded values come from the remote's own settings, so they are already correct remote paths and need no rewriting; the downstream env assembly iterates the parsed dict generically, so no other change is needed.

An allowlist (rather than forwarding everything minus a denylist) is kept deliberately: the raw env dump contains multi-line BASH_FUNC_* bodies that would break the proxy's line-based parsing.

Verification

Reproduced and verified with the self-contained loopback setup from #273 (unprivileged sshd on 127.0.0.1:2222, "remote" = the local Isabelle2025-2 installation) and against a real SSH remote (Isabelle2025-2 on both ends), using a minimal session containing

lemma "(a::int) + b = b + a"
  by (smt (verit))

lemma "(a::int) + b = b + a"
  by (smt (z3))

• Before: smt (verit) passes, smt (z3) fails with The SMT solver "z3" is not installed.
• After: the proxied build finishes and the heap is copied back; forwarded env vars go from 111 to 138.

The ip-test CI job that exercises the proxy is currently disabled (#263), so no CI covers this path; the loopback script in #273 avoids the Isabelle download that broke that job and could serve as a basis for re-enabling it.

Licensing

I confirm this contribution is made under the terms of the MIT license of this repository (see LICENSE).

[hanno-becker]

Thank you for spotting and fixing this @david-wang-0. LGTM