HPC Benchmark

Mix.install([
  {:atp_benchmark_runner, path: "item_14_ATP_Benchmark_Runner/atp_benchmark_runner", force: true}
])

1. Configure paths from .env

project_root = Path.expand("..", __DIR__)
env_file = Path.join(project_root, ".env")

# Load .env values into System.put_env so Config.get() picks them up
env_map = HpcConnect.load_env_file(env_file)
Enum.each(env_map, fn {k, v} -> System.put_env(k, v) end)

IO.puts("Configured paths:")
IO.puts("  TPTP_ROOT:      #{AtpBenchmarkRunner.tptp_dir()}")
IO.puts("  Store dir:      #{AtpBenchmarkRunner.store_dir()}")
IO.puts("  SMT temp dir:   #{AtpBenchmarkRunner.Config.smt_tmp_dir()}")
IO.puts("  .env file:      #{env_file}")

2. Bootstrap the HPC session

boot =
    HpcConnect.bootstrap(
        mode: :local,
        env_file: env_file
    )

session = boot.session

IO.inspect(
    %{
        cluster: session.cluster.name,
        ssh_alias: session.ssh_alias,
        username: session.username,
        work_dir: session.work_dir,
        vault_dir: session.vault_dir
    },
    label: "Resolved HPC session"
)

3. Pick provers and select problems from TPTP_ROOT

selected_provers = [:vampire, :leo3]

# Use the configured TPTP_ROOT (C:\tmp\tptp from .env).
# Problems can be selected by name — they resolve from the TPTP archive,
# bundled examples, or a livebook cache automatically.
problems =
    AtpBenchmarkRunner.select_problems(
        names: ["GRP001-0.p", "GRP002+0.p", "LAT001+0.p"],
        limit: 2
    )

IO.inspect(Enum.map(problems, &%{name: &1.name, path: &1.path}), label: "Problems")

3b. Download the smoke problems individually (no full archive)

Instead of pulling the whole TPTP .tgz, download only the named problems from the official SeeTPTP CGI. These three names are bundled smoke examples (not on the official server), so the local fallback resolves them from priv/tptp_examples (usable from the bundled tmp dir, never written into <TPTP_ROOT>/Problems/).

download_names = ["GRP001-0.p", "GRP002+0.p", "LAT001+0.p"]

{downloaded, download_warnings} =
    AtpBenchmarkRunner.download_tptp_problems!(download_names, force: false)

IO.puts("Downloaded #{length(downloaded)} problem(s):")
Enum.each(downloaded, fn problem ->
    IO.puts("  ✅ #{problem.name}  status=#{problem.expected_status}  rating=#{problem.rating}")
    IO.puts("     -> #{problem.path}")
end)

if download_warnings == [] do
    IO.puts("No warnings.")
else
    IO.puts("Warnings (#{length(download_warnings)}):")
    Enum.each(download_warnings, fn w ->
        IO.puts("  ⚠️  #{w.name}: #{inspect(w.reason)}")
    end)
end

4. Inspect the remote image prep plan

prover_structs = Enum.map(selected_provers, &AtpBenchmarkRunner.Prover.builtin!/1)

image_plan =
    AtpBenchmarkRunner.image_build_plan(
        session,
        prover_structs
    )

IO.inspect(image_plan, label: "Remote image build plan", limit: :infinity)

5. Optionally prepare ATP prover images now

prepare_images_now? = false

if prepare_images_now? do
    uploaded_defs =
        AtpBenchmarkRunner.upload_prover_definitions!(
            session,
            prover_structs,
            install_scripts: false
        )

    IO.inspect(uploaded_defs, label: "Uploaded ATP prover defs")

    built_images =
        AtpBenchmarkRunner.build_prover_images!(
            session,
            prover_structs,
            install_scripts: false
        )

    IO.inspect(built_images, label: "Built ATP prover images")
else
    :ok
end

6. Bootstrap the benchmark plan

This bootstraps a single-node sequential plan with prepare_images: true (auto-builds missing .sif images on the cluster) and wait_for_completion: true (submits and waits for all results before returning).

# ── Single-node sequential, full node ─────────────────────────
plan =
    AtpBenchmarkRunner.bootstrap(
        session,
        selected_provers,
        problems,
        mode: :hpc,
        hpc_mode: :single_node,
        single_node_mode: :sequential,
        timeout_seconds: 30,
        wait_for_completion: true,
        prepare_images: true
    )

IO.inspect(plan, label: "Benchmark plan", limit: :infinity)

7. Submit the run and collect results

IO.puts("Starting HPC benchmark run...")
IO.puts("  Provers: #{inspect(Enum.map(selected_provers, & &1))}")
IO.puts("  Problems: #{length(problems)}")
IO.puts("  Plan mode: #{plan.metadata[:hpc][:hpc_mode]}/#{plan.metadata[:hpc][:single_node_mode]}")
IO.puts("  Partition: #{plan.metadata[:hpc][:partition]}")
IO.puts("")

{t_ms, results} =
    :timer.tc(fn ->
        AtpBenchmarkRunner.run_benchmark(plan)
    end)

elapsed_s = t_ms / 1_000_000
IO.puts("Benchmark completed in #{Float.round(elapsed_s, 2)}s")
IO.puts("Total results: #{length(results)}")

8. Results table

IO.puts("| # | Problem | Prover | SZS Status | Wall (ms) | Memory (KB) | Solved? |")
IO.puts("|---|---------|--------|------------|-----------|-------------|---------|")

results
|> Enum.with_index(1)
|> Enum.each(fn {r, i} ->
    solved = if AtpBenchmarkRunner.Result.solved?(r), do: "✅", else: "❌"
    IO.puts("| #{i} | #{r.problem_id} | #{r.prover} | #{r.szs_status || "?"} | #{r.wall_time_ms || "?"} | #{r.memory_kb || "?"} | #{solved} |")
end)

9. Aggregated report

report = AtpBenchmarkRunner.report(results, plan)

IO.puts("Run ID: #{report.run_id}")
IO.puts("Generated: #{report.generated_at}")
IO.puts("")
IO.puts(report.markdown)

Per-prover breakdown

IO.puts("| Prover | Total | Solved | Failed | Solve Rate |")
IO.puts("|--------|------:|-------:|-------:|-----------:|")

Enum.each(report.by_prover, fn p ->
    IO.puts("| #{p.prover} | #{p.total} | #{p.solved} | #{p.failed} | #{Float.round(p.solve_rate * 100, 1)}% |")
end)

Per-problem comparison

AtpBenchmarkRunner.print_per_problem(report)

Full explained results

IO.puts("Full explained results with proofs:\n")
AtpBenchmarkRunner.explain_full(results) |> IO.puts()

Filtered results by prover

target_prover = :vampire

IO.puts("Verbose report for prover #{target_prover}:\n")
AtpBenchmarkRunner.verbose_report(results, prover: target_prover, solved_only: true)
|> Enum.each(&IO.puts/1)

View a specific proof

target_prover = :vampire
target_problem = "GRP001-0"

AtpBenchmarkRunner.show_proof(results, target_prover, target_problem)

Raw prover debug output

target_prover = :vampire
target_problem = "GRP001-0"

result = Enum.find(results, fn r ->
  r.prover == target_prover and r.problem_id == target_problem
end)

if result && result.raw_output do
  IO.puts("Raw output for #{result.problem_id} / #{result.prover}:\n")
  IO.puts(result.raw_output)
else
  IO.puts("Result not found or no raw output stored (rerun with include_raw_output: true)")
end

10. Persist results to local store

run = AtpBenchmarkRunner.new_run(
    title: "HPC smoke test",
    problems: problems,
    provers: Enum.map(selected_provers, & &1),
    walltime: "00:30:00",
    problem_timeout_seconds: 30
)

run_path = AtpBenchmarkRunner.save_run!(run)
IO.puts("Run saved: #{run_path}")

results_path = AtpBenchmarkRunner.save_results!(run, results)
IO.puts("Results saved: #{results_path}")

report_path = AtpBenchmarkRunner.save_report!(run, report)
IO.puts("Report saved: #{report_path}")