Skip to content

Commit 881ca72

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(fly): deploy config for nesy-solver playground backend (Phase E3)
Adds fly.io deployment for verisim-api and ClickHouse to support the nesy-solver.dev proof playground: * Containerfile.api — slim Rust-only build (no Elixir), Chainguard wolfi base, non-root user, VERISIM_CLICKHOUSE_URL env * fly.toml — verisim-api app, internal-only TCP :8080, shared-cpu-1x / 512MB, auto-stop when idle * clickhouse.fly.toml — ClickHouse app with 1GB persistent volume, internal-only (HTTP :8123, native TCP :9000), min_machines=1 always on * deploy/nesy-playground-schema.sql — minimal schema (proof_attempts table + mv_prover_success_by_class materialised view) extracted from connectors/test-infra/seed/clickhouse-init.sql Both apps internal-only (no public HTTP) — reached via .internal DNS from nesy-solver-api, which is the only public edge in the stack. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 7347f85 commit 881ca72

4 files changed

Lines changed: 247 additions & 0 deletions

File tree

‎Containerfile.api‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# VeriSimDB API-only Container (for fly.io deploy in nesy-solver playground).
5+
#
6+
# Slim variant of container/Containerfile that skips the Elixir orchestration
7+
# layer — the playground only needs the Rust HTTP API on :8080 talking to
8+
# ClickHouse via VERISIM_CLICKHOUSE_URL.
9+
#
10+
# Build (from repo root):
11+
# podman build -f Containerfile.api -t verisim-api:0.1.0 .
12+
# Run (against ClickHouse on host):
13+
# podman run --rm -p 8080:8080 \
14+
# -e VERISIM_CLICKHOUSE_URL=http://host.containers.internal:8123 \
15+
# verisim-api:0.1.0
16+
17+
# ─── Stage 1: Build Rust ────────────────────────────────────────────────
18+
FROM cgr.dev/chainguard/wolfi-base:latest AS rust-builder
19+
20+
RUN apk add --no-cache rust pkgconf build-base
21+
22+
WORKDIR /build
23+
24+
COPY Cargo.toml ./
25+
COPY rust-core/ ./rust-core/
26+
COPY benches/ ./benches/
27+
28+
RUN cargo build --release -p verisim-api
29+
30+
# ─── Stage 2: Runtime ───────────────────────────────────────────────────
31+
FROM cgr.dev/chainguard/wolfi-base:latest
32+
33+
LABEL org.opencontainers.image.title="verisim-api" \
34+
org.opencontainers.image.description="VeriSimDB HTTP API — Rust core only (no Elixir)" \
35+
org.opencontainers.image.source="https://github.com/hyperpolymath/verisimdb" \
36+
org.opencontainers.image.licenses="PMPL-1.0-or-later"
37+
38+
RUN apk add --no-cache ca-certificates curl
39+
40+
RUN addgroup -S verisim && adduser -S verisim -G verisim
41+
42+
WORKDIR /app
43+
COPY --from=rust-builder /build/target/release/verisim-api /app/verisim-api
44+
45+
RUN mkdir -p /data && chown -R verisim:verisim /app /data
46+
47+
# Fly.io default: listen on IPv6 for 6PN network. Switch to 0.0.0.0 via
48+
# VERISIM_HOST env if you need IPv4-only deployment.
49+
ENV RUST_LOG=info
50+
ENV VERISIM_HOST=::
51+
ENV VERISIM_PORT=8080
52+
ENV VERISIM_LOG_FORMAT=json
53+
ENV VERISIM_PERSISTENCE_DIR=/data
54+
ENV VERISIM_ENABLE_CORS=true
55+
# VERISIM_CLICKHOUSE_URL set via `flyctl secrets set` at deploy time.
56+
57+
VOLUME ["/data"]
58+
USER verisim
59+
EXPOSE 8080
60+
61+
HEALTHCHECK --interval=30s --timeout=5s --start-period=15s --retries=3 \
62+
CMD curl -sf http://localhost:8080/health || exit 1
63+
64+
ENTRYPOINT ["/app/verisim-api"]

‎clickhouse.fly.toml‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# fly.io deployment for ClickHouse (Phase E3 nesy-solver playground backend).
3+
#
4+
# Deploy:
5+
# flyctl apps create clickhouse-nesy
6+
# flyctl volumes create clickhouse_data --size 1 --region lhr -a clickhouse-nesy
7+
# flyctl deploy -c clickhouse.fly.toml
8+
#
9+
# Internal-only: no public edge, reachable only from other fly apps in the
10+
# same org via clickhouse-nesy.internal:8123 (HTTP) / :9000 (native).
11+
#
12+
# After first deploy, initialise the schema:
13+
# flyctl ssh console -a clickhouse-nesy
14+
# clickhouse-client --queries-file /init/clickhouse-init.sql
15+
# (or use the deploy script which runs it over HTTP from the host)
16+
17+
app = "clickhouse-nesy"
18+
primary_region = "lhr"
19+
kill_signal = "SIGTERM"
20+
kill_timeout = "30s" # ClickHouse needs time to flush parts
21+
22+
[build]
23+
image = "docker.io/clickhouse/clickhouse-server:24.8"
24+
25+
[env]
26+
CLICKHOUSE_DB = "verisimdb"
27+
CLICKHOUSE_USER = "verisim"
28+
CLICKHOUSE_DEFAULT_ACCESS_MANAGEMENT = "1"
29+
# CLICKHOUSE_PASSWORD via `flyctl secrets set`
30+
31+
[mounts]
32+
source = "clickhouse_data"
33+
destination = "/var/lib/clickhouse"
34+
35+
# HTTP interface :8123 (internal-only)
36+
[[services]]
37+
protocol = "tcp"
38+
internal_port = 8123
39+
auto_stop_machines = "off" # keep hot — verisim-api expects it up
40+
auto_start_machines = true
41+
min_machines_running = 1
42+
processes = ["app"]
43+
44+
[[services.ports]]
45+
port = 8123
46+
handlers = []
47+
48+
[[services.tcp_checks]]
49+
interval = "30s"
50+
timeout = "5s"
51+
grace_period = "30s"
52+
53+
# Native TCP interface :9000 (internal-only, for admin clickhouse-client)
54+
[[services]]
55+
protocol = "tcp"
56+
internal_port = 9000
57+
auto_stop_machines = "off"
58+
auto_start_machines = true
59+
min_machines_running = 1
60+
processes = ["app"]
61+
62+
[[services.ports]]
63+
port = 9000
64+
handlers = []
65+
66+
[[services.tcp_checks]]
67+
interval = "30s"
68+
timeout = "5s"
69+
grace_period = "30s"
70+
71+
[[vm]]
72+
size = "shared-cpu-1x"
73+
memory = "1024mb" # ClickHouse needs real RAM even for small workloads
74+
cpu_kind = "shared"
75+
cpus = 1

‎deploy/nesy-playground-schema.sql‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
-- nesy-solver playground schema — minimal subset of clickhouse-init.sql.
5+
-- Creates just the tables verisim-api needs to serve the playground:
6+
-- verisimdb.proof_attempts — row-per-attempt log
7+
-- verisimdb.mv_prover_success_by_class — strategy aggregate view
8+
--
9+
-- Apply (via HTTP):
10+
-- curl -s 'http://clickhouse-nesy.internal:8123/' \
11+
-- --data-binary @nesy-playground-schema.sql
12+
--
13+
-- Or via clickhouse-client:
14+
-- clickhouse-client --host clickhouse-nesy.internal \
15+
-- --multiquery < nesy-playground-schema.sql
16+
17+
CREATE DATABASE IF NOT EXISTS verisimdb;
18+
19+
CREATE TABLE IF NOT EXISTS verisimdb.proof_attempts
20+
(
21+
attempt_id String,
22+
obligation_id String,
23+
repo String,
24+
file String,
25+
claim String,
26+
obligation_class String,
27+
prover_used Enum8('coq' = 0, 'lean' = 1, 'agda' = 2, 'isabelle' = 3,
28+
'idris2' = 4, 'fstar' = 5, 'z3' = 6, 'cvc5' = 7,
29+
'altergo' = 8, 'dafny' = 9, 'why3' = 10, 'metamath' = 11,
30+
'hol_light' = 12, 'mizar' = 13, 'hol4' = 14, 'pvs' = 15,
31+
'acl2' = 16, 'tlaps' = 17, 'vampire' = 18, 'eprover' = 19,
32+
'other' = 99),
33+
outcome Enum8('success' = 0, 'timeout' = 1, 'failure' = 2, 'unknown' = 3),
34+
duration_ms UInt64,
35+
confidence Float32,
36+
parent_attempt_id Nullable(String),
37+
strategy_tag String,
38+
started_at DateTime64(3),
39+
completed_at DateTime64(3),
40+
prover_output String,
41+
error_message Nullable(String)
42+
)
43+
ENGINE = MergeTree()
44+
ORDER BY (obligation_class, prover_used, started_at)
45+
PARTITION BY toYYYYMM(started_at)
46+
SETTINGS index_granularity = 8192;
47+
48+
CREATE MATERIALIZED VIEW IF NOT EXISTS verisimdb.mv_prover_success_by_class
49+
ENGINE = SummingMergeTree()
50+
ORDER BY (obligation_class, prover_used)
51+
AS SELECT
52+
obligation_class,
53+
prover_used,
54+
countIf(outcome = 'success') AS success_count,
55+
count() AS total_attempts,
56+
sum(duration_ms) AS total_duration_ms
57+
FROM verisimdb.proof_attempts
58+
GROUP BY obligation_class, prover_used;

‎fly.toml‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# fly.io deployment for verisim-api (Phase E3 nesy-solver playground).
3+
#
4+
# Deploy:
5+
# flyctl launch --no-deploy --copy-config --name verisim-api
6+
# flyctl secrets set VERISIM_CLICKHOUSE_URL=http://clickhouse.internal:8123
7+
# flyctl deploy -c fly.toml -f Containerfile.api
8+
#
9+
# Internal-only: no http_service block, so only reachable via 6PN .internal
10+
# DNS from other fly apps in the same org.
11+
12+
app = "verisim-api"
13+
primary_region = "lhr"
14+
kill_signal = "SIGTERM"
15+
kill_timeout = "10s"
16+
17+
[build]
18+
dockerfile = "Containerfile.api"
19+
20+
[env]
21+
RUST_LOG = "info,tower_http=debug"
22+
VERISIM_HOST = "::"
23+
VERISIM_PORT = "8080"
24+
VERISIM_LOG_FORMAT = "json"
25+
VERISIM_ENABLE_CORS = "true"
26+
# VERISIM_CLICKHOUSE_URL via `flyctl secrets set`
27+
28+
# Internal-only service: bind to 6PN network, no public HTTP edge.
29+
[[services]]
30+
protocol = "tcp"
31+
internal_port = 8080
32+
auto_stop_machines = "stop"
33+
auto_start_machines = true
34+
min_machines_running = 0
35+
processes = ["app"]
36+
37+
[[services.ports]]
38+
port = 8080
39+
handlers = [] # no TLS — internal 6PN only
40+
41+
[[services.tcp_checks]]
42+
interval = "30s"
43+
timeout = "5s"
44+
grace_period = "15s"
45+
46+
[[vm]]
47+
size = "shared-cpu-1x"
48+
memory = "512mb" # verisim-api can handle 512MB; 256MB is too tight
49+
cpu_kind = "shared"
50+
cpus = 1

0 commit comments

Comments
 (0)