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 already installs the remote helper scripts and uploads the generic bundled hpc_connect def-file set. ATP prover definitions stay in atp_benchmark_runner/priv/provers, so ATP-specific image prep still goes through the benchmark-runner helpers below.

3. Pick provers and select problems from TPTP_ROOT

selected_provers = [:vampire, :cvc5]

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

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. Optionally submit the run

submit_run? = false

results =
    if submit_run? do
        AtpBenchmarkRunner.run_benchmark(plan)
    else
        []
    end

IO.inspect(results, label: "Results")