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}")

This notebook is the HPC counterpart to the local example. It uses the local workspace versions of both libraries because atp_benchmark_runner depends on the sibling hpc_connect path from its mix.exs.

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"
)

HpcConnect.bootstrap/1 installs the remote helper scripts and uploads the generic bundled hpc_connect def-file set.

2b. Download problems

selected_problems = [
  "ALG001+0.p",
  "GRP001-0.p",
  "GRP002+0.p",
  "GRP003+0.p",
  "GRP004+0.p",
  "GRP720+1.p",
  "GRP752-1.p",
  "LAT001+0.p",
  "PUZ001+0.p",
  "REL001+0.p",
  "SET001^0.p",
  "SMT001+0.p",
  "SYN000+0.p",
  "THF001+0.p"
]

{downloaded, download_warnings} =
    AtpBenchmarkRunner.download_tptp_problems!(selected_problems, 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

3. Pick provers and select problems from TPTP_ROOT

selected_provers = [
   :tableaux,
   :eprover,
   :vampire,
   :cvc5,
   :zipperposition,
   :leo3,
   :leo2,
   :lash
]

# 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: selected_problems,
        limit: 10
    )

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

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 an HPC benchmark plan

Select the execution mode and resource strategy:

node_size controls how many CPUs of a node are requested. Auto-detected per cluster (Helma CPU: 384/192, Fritz: 72/36, spr*: 104/52).

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

IO.inspect(plan, label: "Single-node sequential, full node (default)", limit: :infinity)

# ── Single-node sequential, half node ────────────────────────
plan_half =
    AtpBenchmarkRunner.bootstrap(
        session,
        selected_provers,
        problems,
        mode: :hpc,
        hpc_mode: :single_node,
        single_node_mode: :sequential,
        node_size: :half,
        timeout_seconds: 30,
        wait_for_completion: false,
        prepare_images: false
    )

IO.inspect(plan_half, label: "Single-node sequential, half node", limit: :infinity)

# ── Single-node parallel, full node ──────────────────────────
plan_parallel =
    AtpBenchmarkRunner.bootstrap(
        session,
        selected_provers,
        problems,
        mode: :hpc,
        hpc_mode: :single_node,
        single_node_mode: :parallel,
        max_parallel_jobs: 4,
        timeout_seconds: 30,
        wait_for_completion: false,
        prepare_images: false
    )

IO.inspect(plan_parallel, label: "Single-node parallel plan", limit: :infinity)

# ── Multi-node ────────────────────────────────────────────────
# Each prover gets its own node (default full).
plan_multi =
    AtpBenchmarkRunner.bootstrap(
        session,
        selected_provers,
        problems,
        mode: :hpc,
        hpc_mode: :multi_node,
        timeout_seconds: 30,
        wait_for_completion: false,
        prepare_images: false
    )

IO.inspect(plan_multi, label: "Multi-node plan", limit: :infinity)

If you want the runner itself to prepare missing prover images immediately before launch, set prepare_images: true in the benchmark plan above.

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}")