Skip to content

TOOLCHAIN_README.md

Latest commit

 

History

History
142 lines (102 loc) · 3.64 KB

TOOLCHAIN_README.md

File metadata and controls

142 lines (102 loc) · 3.64 KB
Raw

Local Verification Toolchain

This workflow expects verification tools to live outside paper project folders. The default shared tool root on Windows is:

C:\Tools\CodexVerification

You can override this location by setting CODEX_VERIFICATION_HOME or by passing -ToolRoot to verify_toolchain.ps1.

The toolchain check is diagnostic. It does not install large tools, modify PATH, or change system environment variables.

Shared Tool Layout

  • Python 3.12.10: C:\Tools\CodexVerification\Python312\python.exe
  • Python packages:
    • sympy for symbolic algebra
    • numpy and scipy for numerical computation and counterexample search
    • matplotlib for plots
    • pandas for tables/logs
    • z3-solver for SMT-style checks
  • Lean 4 via elan:
    • lean: C:\Tools\CodexVerification\elan\bin\lean.exe
    • lake: C:\Tools\CodexVerification\elan\bin\lake.exe
  • Optional shared Lake packages:
    • C:\Tools\CodexVerification\lean_packages\lean-vX.Y.Z\

For Lean projects with Mathlib, keep the project files in the paper folder:

lakefile.toml
lake-manifest.json
lean-toolchain
YourLeanLibrary/

Keep large package caches in the shared tool root when possible, especially when working inside cloud-synced folders such as Dropbox.

Mathematica

Mathematica 13.0 is installed locally, and wolframscript exists at:

C:\Program Files\Wolfram Research\Mathematica\13.0\wolframscript.exe

Codex can run wolframscript successfully when the command is allowed to run outside the default sandbox. In the default sandbox, WolframScript may fail because it cannot read the user configuration directory:

C:\Users\viplee110\AppData\Roaming\Wolfram\WolframScript

When using Mathematica from Codex, approve the wolframscript command if prompted. Mathematica is useful for:

  • FullSimplify
  • Reduce
  • Resolve
  • symbolic derivatives
  • inequality checks under assumptions
  • exact parameter-region analysis

Quick Self-Test

Run:

.\verify_toolchain.ps1 -WriteStatus

This writes a reusable computer-level status file to:

C:\Users\<user>\.econ-theorist-ai\toolchain_status.md

Use a non-default tool root:

$env:CODEX_VERIFICATION_HOME = "D:\Tools\CodexVerification"
.\verify_toolchain.ps1 -WriteStatus

or:

.\verify_toolchain.ps1 -ToolRoot "D:\Tools\CodexVerification" -WriteStatus

Use a persistent local config:

.\verify_toolchain.ps1 -ConfigPath "$HOME\.econ-theorist-ai\config.json" -WriteStatus

Example config.json:

{
  "toolRoot": "D:\\Tools\\CodexVerification",
  "pythonPath": "D:\\Tools\\CodexVerification\\Python312\\python.exe",
  "elanHome": "D:\\Tools\\CodexVerification\\elan",
  "wolframScriptPath": "C:\\Program Files\\Wolfram Research\\Mathematica\\13.0\\wolframscript.exe"
}

Direct Mathematica test:

& "C:\Program Files\Wolfram Research\Mathematica\13.0\wolframscript.exe" -code "Print[2+2]"
& "C:\Program Files\Wolfram Research\Mathematica\13.0\wolframscript.exe" -code "Print[FullSimplify[D[x^3,x]]]"

Python Command

Use:

& "C:\Tools\CodexVerification\Python312\python.exe"

Example:

& "C:\Tools\CodexVerification\Python312\python.exe" -c "import sympy as sp; x=sp.symbols('x'); print(sp.diff(x**3, x))"

Lean Command

Use:

$env:ELAN_HOME = "C:\Tools\CodexVerification\elan"
& "C:\Tools\CodexVerification\elan\bin\lean.exe" --version
& "C:\Tools\CodexVerification\elan\bin\lake.exe" --version

Mathlib should be installed only when needed, because it is a large dependency. Prefer shared package storage under C:\Tools\CodexVerification\lean_packages.