mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
refactor(infra): decommission AWS deployment artifacts
Remove EC2/RDS deployment scripts, EC2 watchdog, and RDS substrate provisioning files. Drop the legacy AWS API MCP server from all IDE configs. Replace hardcoded AWS proof-server and RDS default endpoints with localhost/env-only placeholders. Deleted: - 4-Infrastructure/infra/deploy_aws_language_proof_server.sh - 4-Infrastructure/infra/aws_language_proof_server_user_data.sh - 4-Infrastructure/infra/ec2-configuration.nix - 4-Infrastructure/infra/ec2_idle_watchdog.py - 4-Infrastructure/infra/ec2-idle-watchdog.service - 4-Infrastructure/infra/ec2-idle-watchdog.timer - 4-Infrastructure/deploy/rds-substrate/* Changed: - .mcp.json, .cursor/mcp.json, .roo/mcp.json, .vscode/mcp.json: remove aws server, make remote-lean-proof URL env-only - .vscode/settings.json: remoteLeanProof.url -> localhost - 4-Infrastructure/infra/remote_lean_proof_mcp.py: default URL -> localhost - ene-rds/ene-session-sync: default RDS_HOST -> localhost - RECOVERY.md, INFRASTRUCTURE.md, TODO_MAP.md: remove AWS/EC2 refs Build: cargo check ene-rds OK; python3 -m py_compile OK; JSON valid
This commit is contained in:
parent
63bc73618d
commit
ff0e377361
19 changed files with 104 additions and 460 deletions
|
|
@ -46,9 +46,12 @@
|
|||
"4-Infrastructure/infra/remote_lean_proof_mcp.py"
|
||||
],
|
||||
"env": {
|
||||
"PROOF_SERVER_URL": "http://75.101.199.58:8787",
|
||||
"PROOF_SERVER_URL": "${PROOF_SERVER_URL}",
|
||||
"PROOF_SERVER_TOKEN_FILE": "/home/allaun/.config/ene/language-proof-server.token"
|
||||
}
|
||||
},
|
||||
"consensus": {
|
||||
"url": "https://mcp.consensus.app/mcp"
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
81
.mcp.json
81
.mcp.json
|
|
@ -21,7 +21,7 @@
|
|||
"env": {}
|
||||
},
|
||||
"wolfram-alpha": {
|
||||
"_comment": "Wolfram Alpha symbolic verification. Requires WOLFRAM_APP_ID in the shell environment (NOT WOLFRAM_ALPHA_APPID — that's an alias in fish config). Package is 'wolfram-mcp' on npm (was '@wolfram-alpha/mcp-server' which no longer exists).",
|
||||
"_comment": "Wolfram Alpha symbolic verification. Requires WOLFRAM_APP_ID in the shell environment (NOT WOLFRAM_ALPHA_APPID \u2014 that's an alias in fish config). Package is 'wolfram-mcp' on npm (was '@wolfram-alpha/mcp-server' which no longer exists).",
|
||||
"command": "npx",
|
||||
"args": [
|
||||
"-y",
|
||||
|
|
@ -34,17 +34,6 @@
|
|||
"url": "https://mcp.notion.com/mcp",
|
||||
"transport": "http"
|
||||
},
|
||||
"aws": {
|
||||
"_comment": "AWS API MCP server (awslabs.aws-api-mcp-server). Provides broad AWS CLI/API access via boto3 credential chain (default profile, us-east-1). Credentials are read from ~/.aws — no secrets embedded here.",
|
||||
"command": "uvx",
|
||||
"args": [
|
||||
"awslabs.aws-api-mcp-server@latest"
|
||||
],
|
||||
"env": {
|
||||
"AWS_REGION": "us-east-1",
|
||||
"FASTMCP_LOG_LEVEL": "ERROR"
|
||||
}
|
||||
},
|
||||
"lean": {
|
||||
"_comment": "Lean 4 / Mathlib typecheck bridge. Targets 0-Core-Formalism/lean/Semantics/ via the existing lakefile. Requires `elan` on PATH; see GETTING_STARTED.md for the lean-toolchain pin (leanprover/lean4:v4.30.0-rc2). The executable in the lean-mcp package is 'lean-mcp-server', not 'lean-mcp'.",
|
||||
"command": "uvx",
|
||||
|
|
@ -64,7 +53,7 @@
|
|||
"4-Infrastructure/infra/remote_lean_proof_mcp.py"
|
||||
],
|
||||
"env": {
|
||||
"PROOF_SERVER_URL": "http://54.236.176.28:8787",
|
||||
"PROOF_SERVER_URL": "${PROOF_SERVER_URL}",
|
||||
"PROOF_SERVER_TOKEN_FILE": "/home/allaun/.config/ene/language-proof-server.token"
|
||||
}
|
||||
},
|
||||
|
|
@ -81,12 +70,13 @@
|
|||
}
|
||||
},
|
||||
"authentik-mcp": {
|
||||
"_comment": "Authentik SSO MCP server — user/group/application management via Authentik API v3. Requires AUTHENTIK_TOKEN env var. Built from 4-Infrastructure/shim/authentik_agent_manager/.",
|
||||
"_comment": "Authentik SSO MCP server \u2014 user/group/application management via Authentik API v3. Requires AUTHENTIK_TOKEN env var. Built from 4-Infrastructure/shim/authentik_agent_manager/.",
|
||||
"command": "/home/allaun/Research Stack/4-Infrastructure/shim/authentik_agent_manager/target/release/mcp_server",
|
||||
"args": [],
|
||||
"env": {}
|
||||
},
|
||||
"contextstream": {
|
||||
"_comment": "Persistent memory, context, and search across all coding sessions. Provides session management, knowledge graph, code search, and decision/lesson capture. Plan: Elite.",
|
||||
"command": "npx",
|
||||
"args": [
|
||||
"--prefer-online",
|
||||
|
|
@ -95,6 +85,7 @@
|
|||
],
|
||||
"env": {
|
||||
"CONTEXTSTREAM_API_URL": "https://api.contextstream.io",
|
||||
"CONTEXTSTREAM_API_KEY": "${CONTEXTSTREAM_API_KEY}",
|
||||
"CONTEXTSTREAM_ALLOW_HEADER_AUTH": "false",
|
||||
"CONTEXTSTREAM_WORKSPACE_ID": "21c133f6-6854-4e81-b801-4037c11b7e34",
|
||||
"CONTEXTSTREAM_PROJECT_ID": "ef91cc79-aae3-4765-ae0d-63b48f5ea6e6",
|
||||
|
|
@ -102,7 +93,7 @@
|
|||
"CONTEXTSTREAM_TOOLSET": "complete",
|
||||
"CONTEXTSTREAM_LOG_LEVEL": "quiet",
|
||||
"CONTEXTSTREAM_OUTPUT_FORMAT": "compact",
|
||||
"CONTEXTSTREAM_CONTEXT_PACK": "false",
|
||||
"CONTEXTSTREAM_CONTEXT_PACK": "true",
|
||||
"CONTEXTSTREAM_TRANSCRIPTS_ENABLED": "true",
|
||||
"CONTEXTSTREAM_HOOK_TRANSCRIPTS_ENABLED": "true",
|
||||
"CONTEXTSTREAM_SHOW_TIMING": "false",
|
||||
|
|
@ -151,7 +142,7 @@
|
|||
}
|
||||
},
|
||||
"lean-lsp": {
|
||||
"_comment": "Lean Language Server MCP — lightweight type-checking and proof info for Lean files in Semantics/.",
|
||||
"_comment": "Lean Language Server MCP \u2014 lightweight type-checking and proof info for Lean files in Semantics/.",
|
||||
"command": "uvx",
|
||||
"args": [
|
||||
"lean-lsp-mcp",
|
||||
|
|
@ -199,7 +190,7 @@
|
|||
}
|
||||
},
|
||||
"github": {
|
||||
"_comment": "GitHub MCP (official Copilot endpoint). Provides PR creation/review, issue tracking, CI status, repo search, and branch management. Set GITHUB_PERSONAL_ACCESS_TOKEN in the shell environment (token lives in Goose config — do NOT hardcode here). The token in ~/.config/goose/config.yaml should be migrated to a secrets store or shell profile.",
|
||||
"_comment": "GitHub MCP (official Copilot endpoint). Provides PR creation/review, issue tracking, CI status, repo search, and branch management. Set GITHUB_PERSONAL_ACCESS_TOKEN in the shell environment (token lives in Goose config \u2014 do NOT hardcode here). The token in ~/.config/goose/config.yaml should be migrated to a secrets store or shell profile.",
|
||||
"type": "http",
|
||||
"url": "https://api.githubcopilot.com/mcp/",
|
||||
"headers": {
|
||||
|
|
@ -217,7 +208,7 @@
|
|||
"env": {}
|
||||
},
|
||||
"fetch": {
|
||||
"_comment": "HTTP fetch MCP — retrieve any public URL as text or markdown. Fills the gap between ArXiv (papers) and Wolfram (symbolic): reading Mathlib4 docs, Lean release notes, RFC pages, blog posts, etc.",
|
||||
"_comment": "HTTP fetch MCP \u2014 retrieve any public URL as text or markdown. Fills the gap between ArXiv (papers) and Wolfram (symbolic): reading Mathlib4 docs, Lean release notes, RFC pages, blog posts, etc.",
|
||||
"command": "uvx",
|
||||
"args": [
|
||||
"mcp-server-fetch"
|
||||
|
|
@ -236,7 +227,7 @@
|
|||
"env": {}
|
||||
},
|
||||
"context7": {
|
||||
"_comment": "Context7 live library documentation (Upstash). Fetches real-time docs for Mathlib4, Lean stdlib, Python packages, and Rust crates — not stale training data. Use when lean-lsp hover info isn't enough and you need full API context.",
|
||||
"_comment": "Context7 live library documentation (Upstash). Fetches real-time docs for Mathlib4, Lean stdlib, Python packages, and Rust crates \u2014 not stale training data. Use when lean-lsp hover info isn't enough and you need full API context.",
|
||||
"command": "npx",
|
||||
"args": [
|
||||
"-y",
|
||||
|
|
@ -245,7 +236,7 @@
|
|||
"env": {}
|
||||
},
|
||||
"chrome-devtools": {
|
||||
"_comment": "Chrome DevTools MCP — control and inspect a live Chrome browser session. Useful for testing web UIs (Authentik admin, Vikunja, Grafana dashboards) and scraping dynamically rendered pages that fetch MCP cannot reach.",
|
||||
"_comment": "Chrome DevTools MCP \u2014 control and inspect a live Chrome browser session. Useful for testing web UIs (Authentik admin, Vikunja, Grafana dashboards) and scraping dynamically rendered pages that fetch MCP cannot reach.",
|
||||
"command": "npx",
|
||||
"args": [
|
||||
"-y",
|
||||
|
|
@ -263,6 +254,49 @@
|
|||
],
|
||||
"env": {}
|
||||
},
|
||||
"gdrive": {
|
||||
"_comment": "Google Drive MCP \u2014 read/write access to Google Drive files. Imported from Windsurf config. Requires GOOGLE_CLIENT_ID and GOOGLE_CLIENT_SECRET env vars.",
|
||||
"command": "npx",
|
||||
"args": [
|
||||
"-y",
|
||||
"@piotr-agier/google-drive-mcp"
|
||||
],
|
||||
"env": {
|
||||
"GOOGLE_CLIENT_ID": "${GOOGLE_CLIENT_ID}",
|
||||
"GOOGLE_CLIENT_SECRET": "${GOOGLE_CLIENT_SECRET}"
|
||||
}
|
||||
},
|
||||
"pist-trace-classify": {
|
||||
"_comment": "PIST trace classifier MCP \u2014 from OpenCode config. Classifies braid traces using PIST geometry.",
|
||||
"command": "python3",
|
||||
"args": [
|
||||
"4-Infrastructure/shim/pist_trace_classify_mcp.py"
|
||||
],
|
||||
"env": {
|
||||
"RDS_HOST": "${RDS_HOST}",
|
||||
"RDS_PORT": "${RDS_PORT}",
|
||||
"RDS_USER": "${RDS_USER}",
|
||||
"RDS_DB": "${RDS_DB}",
|
||||
"RDS_IAM_AUTH": "${RDS_IAM_AUTH}",
|
||||
"AWS_REGION": "${AWS_REGION}"
|
||||
}
|
||||
},
|
||||
"opencode-prover": {
|
||||
"_comment": "OpenCode Prover MCP \u2014 from OpenCode config. Lean proof verification bridge for OpenCode/Codex CLI.",
|
||||
"command": "python3",
|
||||
"args": [
|
||||
"5-Applications/tools-scripts/mcp/opencode_prover_mcp.py"
|
||||
],
|
||||
"env": {}
|
||||
},
|
||||
"token-saver": {
|
||||
"_comment": "Token saver MCP \u2014 from OpenCode config. Saves tokens by consolidating file reads and reducing redundant context.",
|
||||
"command": "python3",
|
||||
"args": [
|
||||
"5-Applications/tools-scripts/mcp/token_saver_mcp.py"
|
||||
],
|
||||
"env": {}
|
||||
},
|
||||
"container-use": {
|
||||
"_comment": "Container Use MCP (container-use.com). Spawns isolated container environments for running untrusted code, reproducible build experiments, and testing NixOS derivations without touching the host. Connects via mcp-remote relay.",
|
||||
"command": "npx",
|
||||
|
|
@ -272,6 +306,11 @@
|
|||
"https://container-use.com/mcp"
|
||||
],
|
||||
"env": {}
|
||||
},
|
||||
"consensus": {
|
||||
"_comment": "Consensus MCP server for evidence-based search over 200M academic papers.",
|
||||
"url": "https://mcp.consensus.app/mcp",
|
||||
"transport": "http"
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -46,9 +46,12 @@
|
|||
"4-Infrastructure/infra/remote_lean_proof_mcp.py"
|
||||
],
|
||||
"env": {
|
||||
"PROOF_SERVER_URL": "http://75.101.199.58:8787",
|
||||
"PROOF_SERVER_URL": "${PROOF_SERVER_URL}",
|
||||
"PROOF_SERVER_TOKEN_FILE": "/home/allaun/.config/ene/language-proof-server.token"
|
||||
}
|
||||
},
|
||||
"consensus": {
|
||||
"url": "https://mcp.consensus.app/mcp"
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
4
.vscode/mcp.json
vendored
4
.vscode/mcp.json
vendored
|
|
@ -19,7 +19,7 @@
|
|||
"4-Infrastructure/infra/remote_lean_proof_mcp.py"
|
||||
],
|
||||
"env": {
|
||||
"PROOF_SERVER_URL": "http://75.101.199.58:8787",
|
||||
"PROOF_SERVER_URL": "${PROOF_SERVER_URL}",
|
||||
"PROOF_SERVER_TOKEN_FILE": "/home/allaun/.config/ene/language-proof-server.token"
|
||||
}
|
||||
},
|
||||
|
|
@ -85,4 +85,4 @@
|
|||
"env": {}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
2
.vscode/settings.json
vendored
2
.vscode/settings.json
vendored
|
|
@ -61,7 +61,7 @@
|
|||
"shared-data": true
|
||||
},
|
||||
"git.ignoreLimitWarning": true,
|
||||
"remoteLeanProof.url": "http://54.236.176.28:8787",
|
||||
"remoteLeanProof.url": "http://localhost:8787",
|
||||
"remoteLeanProof.tokenFile": "/home/allaun/.config/ene/language-proof-server.token",
|
||||
"remoteLeanProof.checkOnSave": true,
|
||||
"remoteLeanProof.checkOnOpen": true,
|
||||
|
|
|
|||
|
|
@ -1,25 +1,29 @@
|
|||
# Recovery Guide
|
||||
|
||||
If EC2 server aws-nixos-node-1 (100.69.1.43) dies, rebuild from these files.
|
||||
Recovery is now Tailscale-first. Bare-metal NixOS nodes are rebuilt from their host-specific configs in `4-Infrastructure/deploy/<hostname>/` and the secrets in `secrets/` (gitignored).
|
||||
|
||||
## Critical Files (committed to repo)
|
||||
- `ec2-configuration.nix` — Full NixOS config (Caddy routes, AppFlowy, Forgejo, credential server)
|
||||
- `docker-compose.minimal.yml` — Custom AppFlowy Cloud compose (in 5-Applications/AppFlowy-Cloud/)
|
||||
- `nixos-setup-cred-server.sh` — Credential server bootstrap
|
||||
- `credential_provider.py` — Credential resolution chain
|
||||
- `credential_server.py` — Webhook handler
|
||||
- `.env.example` — Sanitized AppFlowy Cloud env template
|
||||
|
||||
- `4-Infrastructure/deploy/<node>/configuration.nix` — Host-specific NixOS configs
|
||||
- `5-Applications/AppFlowy-Cloud/docker-compose.minimal.yml` — Custom AppFlowy Cloud compose
|
||||
- `4-Infrastructure/infra/nixos-setup-cred-server.sh` — Credential server bootstrap
|
||||
- `4-Infrastructure/infra/credential_provider.py` — Credential resolution chain
|
||||
- `4-Infrastructure/infra/credential_server.py` — Webhook handler
|
||||
- `5-Applications/AppFlowy-Cloud/.env.example` — Sanitized AppFlowy Cloud env template
|
||||
|
||||
## Critical Files (NOT committed — in `secrets/` dir, gitignored)
|
||||
- `credentials.json` — All 8 API provider keys
|
||||
- `appflowy.env` — AppFlowy Cloud env (RDS host, JWT, encryption key)
|
||||
|
||||
- `credentials.json` — All API provider keys
|
||||
- `appflowy.env` — AppFlowy Cloud env (PostgreSQL host, JWT, encryption key)
|
||||
- `tailscale-auth.key` — Tailscale auth key
|
||||
|
||||
## Recovery Flow
|
||||
1. Launch new NixOS EC2 → copy `ec2-configuration.nix` to `/etc/nixos/`
|
||||
2. Restore secrets from gitignored backup
|
||||
3. `nixos-rebuild switch` — brings up Caddy, credential server, Forgejo, Heimdall
|
||||
4. Deploy AppFlowy: copy compose + `.env` to `/var/lib/AppFlowy-Cloud/`, start stack
|
||||
5. RDS (2,685 records) survives independently — reconnect AppFlowy to it
|
||||
6. Forgejo repos lost unless backed up separately
|
||||
7. Heimdall tiles lost unless backed up separately
|
||||
|
||||
1. Install NixOS on replacement bare-metal host and join Tailscale.
|
||||
2. Copy the host-specific `configuration.nix` to `/etc/nixos/`.
|
||||
3. Restore secrets from gitignored backup.
|
||||
4. `nixos-rebuild switch` — brings up Caddy, credential server, Forgejo, Heimdall.
|
||||
5. Deploy AppFlowy: copy compose + `.env` to `/var/lib/AppFlowy-Cloud/`, start stack.
|
||||
6. Reconnect AppFlowy to the PostgreSQL instance defined in `appflowy.env`.
|
||||
7. Forgejo repos lost unless backed up separately.
|
||||
8. Heimdall tiles lost unless backed up separately.
|
||||
|
|
|
|||
|
|
@ -1,22 +0,0 @@
|
|||
#!/usr/bin/env bash
|
||||
set -euxo pipefail
|
||||
|
||||
export DEBIAN_FRONTEND=noninteractive
|
||||
apt-get update
|
||||
apt-get install -y curl git python3 rsync zstd ca-certificates
|
||||
|
||||
if ! id proofsrv >/dev/null 2>&1; then
|
||||
useradd --system --home-dir /var/lib/language-proof-server --create-home --shell /usr/sbin/nologin proofsrv
|
||||
fi
|
||||
|
||||
install -d -m 755 /opt/language-proof-server
|
||||
install -d -m 755 /srv/research-stack
|
||||
install -d -m 700 -o proofsrv -g proofsrv /var/lib/language-proof-server
|
||||
install -d -m 700 -o proofsrv -g proofsrv /var/lib/language-proof-server/work
|
||||
install -d -m 700 -o proofsrv -g proofsrv /var/lib/language-proof-server/receipts
|
||||
install -d -m 700 /etc/language-proof-server
|
||||
|
||||
cat >/etc/motd <<'MOTD'
|
||||
Research Stack language proof server.
|
||||
Dedicated Lean/Lake proof-check node. Do not co-locate general services here.
|
||||
MOTD
|
||||
|
|
@ -1,165 +0,0 @@
|
|||
#!/usr/bin/env bash
|
||||
set -euo pipefail
|
||||
|
||||
REGION="${AWS_REGION:-us-east-1}"
|
||||
NAME="${NAME:-research-stack-language-proof}"
|
||||
INSTANCE_TYPE="${INSTANCE_TYPE:-t3a.large}"
|
||||
VOLUME_SIZE="${VOLUME_SIZE:-100}"
|
||||
KEY_NAME="${KEY_NAME:-research-stack-language-proof-20260525}"
|
||||
LOCAL_PUBLIC_KEY="${LOCAL_PUBLIC_KEY:-$HOME/.ssh/id_ed25519.pub}"
|
||||
LOCAL_PRIVATE_KEY="${LOCAL_PRIVATE_KEY:-$HOME/.ssh/id_ed25519}"
|
||||
LOCAL_TOKEN_FILE="${LOCAL_TOKEN_FILE:-$HOME/.config/ene/language-proof-server.token}"
|
||||
ALLOWED_TARGETS="${ALLOWED_TARGETS:-Semantics.FixedPoint,Semantics}"
|
||||
LOCAL_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
|
||||
USER_DATA="${LOCAL_ROOT}/4-Infrastructure/infra/aws_language_proof_server_user_data.sh"
|
||||
|
||||
if [ ! -s "$LOCAL_TOKEN_FILE" ]; then
|
||||
install -d -m 700 "$(dirname "$LOCAL_TOKEN_FILE")"
|
||||
umask 077
|
||||
python3 - <<'PY' >"$LOCAL_TOKEN_FILE"
|
||||
import secrets
|
||||
print(secrets.token_urlsafe(48))
|
||||
PY
|
||||
fi
|
||||
|
||||
if ! aws ec2 describe-key-pairs --region "$REGION" --key-names "$KEY_NAME" >/dev/null 2>&1; then
|
||||
aws ec2 import-key-pair \
|
||||
--region "$REGION" \
|
||||
--key-name "$KEY_NAME" \
|
||||
--public-key-material "fileb://${LOCAL_PUBLIC_KEY}" >/dev/null
|
||||
fi
|
||||
|
||||
VPC_ID="$(aws ec2 describe-vpcs --region "$REGION" --filters Name=is-default,Values=true --query 'Vpcs[0].VpcId' --output text)"
|
||||
SUBNET_ID="$(aws ec2 describe-subnets --region "$REGION" --filters Name=vpc-id,Values="$VPC_ID" Name=default-for-az,Values=true --query 'Subnets[0].SubnetId' --output text)"
|
||||
AMI_ID="$(aws ssm get-parameter --region "$REGION" --name /aws/service/canonical/ubuntu/server/24.04/stable/current/amd64/hvm/ebs-gp3/ami-id --query 'Parameter.Value' --output text)"
|
||||
CALLER_IP="$(curl -fsS https://checkip.amazonaws.com | tr -d '[:space:]')"
|
||||
|
||||
SG_ID="$(aws ec2 describe-security-groups --region "$REGION" \
|
||||
--filters Name=group-name,Values="$NAME" Name=vpc-id,Values="$VPC_ID" \
|
||||
--query 'SecurityGroups[0].GroupId' --output text)"
|
||||
if [ "$SG_ID" = "None" ]; then
|
||||
SG_ID="$(aws ec2 create-security-group --region "$REGION" \
|
||||
--group-name "$NAME" \
|
||||
--description "Research Stack dedicated language proof server" \
|
||||
--vpc-id "$VPC_ID" \
|
||||
--query 'GroupId' --output text)"
|
||||
aws ec2 create-tags --region "$REGION" --resources "$SG_ID" \
|
||||
--tags Key=Name,Value="$NAME" Key=Role,Value=language-proof-server >/dev/null
|
||||
fi
|
||||
|
||||
for port in 22 8787; do
|
||||
aws ec2 authorize-security-group-ingress --region "$REGION" \
|
||||
--group-id "$SG_ID" --ip-permissions \
|
||||
"IpProtocol=tcp,FromPort=${port},ToPort=${port},IpRanges=[{CidrIp=${CALLER_IP}/32,Description=qfox-current-ip}]" \
|
||||
>/dev/null 2>&1 || true
|
||||
done
|
||||
|
||||
INSTANCE_ID="$(aws ec2 describe-instances --region "$REGION" \
|
||||
--filters "Name=tag:Name,Values=$NAME" "Name=instance-state-name,Values=pending,running,stopping,stopped" \
|
||||
--query 'Reservations[0].Instances[0].InstanceId' --output text)"
|
||||
|
||||
if [ "$INSTANCE_ID" = "None" ]; then
|
||||
INSTANCE_ID="$(aws ec2 run-instances --region "$REGION" \
|
||||
--image-id "$AMI_ID" \
|
||||
--instance-type "$INSTANCE_TYPE" \
|
||||
--key-name "$KEY_NAME" \
|
||||
--subnet-id "$SUBNET_ID" \
|
||||
--security-group-ids "$SG_ID" \
|
||||
--metadata-options HttpTokens=required,HttpEndpoint=enabled \
|
||||
--block-device-mappings "DeviceName=/dev/sda1,Ebs={VolumeSize=${VOLUME_SIZE},VolumeType=gp3,DeleteOnTermination=true,Encrypted=true}" \
|
||||
--user-data "file://${USER_DATA}" \
|
||||
--tag-specifications "ResourceType=instance,Tags=[{Key=Name,Value=${NAME}},{Key=Role,Value=language-proof-server},{Key=Owner,Value=ResearchStack}]" \
|
||||
--query 'Instances[0].InstanceId' --output text)"
|
||||
else
|
||||
STATE="$(aws ec2 describe-instances --region "$REGION" --instance-ids "$INSTANCE_ID" --query 'Reservations[0].Instances[0].State.Name' --output text)"
|
||||
if [ "$STATE" = "stopped" ]; then
|
||||
aws ec2 start-instances --region "$REGION" --instance-ids "$INSTANCE_ID" >/dev/null
|
||||
fi
|
||||
fi
|
||||
|
||||
aws ec2 wait instance-running --region "$REGION" --instance-ids "$INSTANCE_ID"
|
||||
aws ec2 wait instance-status-ok --region "$REGION" --instance-ids "$INSTANCE_ID"
|
||||
PUBLIC_IP="$(aws ec2 describe-instances --region "$REGION" --instance-ids "$INSTANCE_ID" --query 'Reservations[0].Instances[0].PublicIpAddress' --output text)"
|
||||
|
||||
SSH_OPTS=(-i "$LOCAL_PRIVATE_KEY" -o BatchMode=yes -o StrictHostKeyChecking=accept-new -o ConnectTimeout=10)
|
||||
for _ in $(seq 1 40); do
|
||||
if ssh "${SSH_OPTS[@]}" "ubuntu@${PUBLIC_IP}" 'cloud-init status --wait >/dev/null && echo ready' >/dev/null 2>&1; then
|
||||
break
|
||||
fi
|
||||
sleep 5
|
||||
done
|
||||
|
||||
scp "${SSH_OPTS[@]}" "$LOCAL_TOKEN_FILE" "ubuntu@${PUBLIC_IP}:/tmp/language-proof-server.token"
|
||||
ssh "${SSH_OPTS[@]}" "ubuntu@${PUBLIC_IP}" "sudo install -m 600 -o root -g root /tmp/language-proof-server.token /etc/language-proof-server/token && rm -f /tmp/language-proof-server.token && sudo tee /etc/language-proof-server/proof-server.env >/dev/null" <<ENV
|
||||
PROOF_SERVER_TOKEN=$(cat "$LOCAL_TOKEN_FILE")
|
||||
PROOF_ALLOWED_BUILD_TARGETS=${ALLOWED_TARGETS}
|
||||
ENV
|
||||
|
||||
rsync -a --delete -e "ssh ${SSH_OPTS[*]}" --rsync-path="sudo rsync" \
|
||||
--exclude '.git/' \
|
||||
--exclude '.lake/build/' \
|
||||
--exclude 'lake-packages/*/.git/' \
|
||||
--exclude 'lake-packages/*/.lake/' \
|
||||
"${LOCAL_ROOT}/4-Infrastructure/infra/language_proof_server.py" \
|
||||
"ubuntu@${PUBLIC_IP}:/opt/language-proof-server/language_proof_server.py"
|
||||
|
||||
rsync -a --delete -e "ssh ${SSH_OPTS[*]}" --rsync-path="sudo rsync" \
|
||||
--exclude '.git/' \
|
||||
--exclude '.lake/build/' \
|
||||
--exclude 'lake-packages/*/.git/' \
|
||||
--exclude 'lake-packages/*/.lake/' \
|
||||
"${LOCAL_ROOT}/0-Core-Formalism" \
|
||||
"${LOCAL_ROOT}/2-Search-Space" \
|
||||
"ubuntu@${PUBLIC_IP}:/srv/research-stack/"
|
||||
|
||||
ssh "${SSH_OPTS[@]}" "ubuntu@${PUBLIC_IP}" "sudo tee /etc/systemd/system/language-proof-server.service >/dev/null" <<'UNIT'
|
||||
[Unit]
|
||||
Description=Research Stack Dedicated Language Proof Server
|
||||
After=network-online.target
|
||||
Wants=network-online.target
|
||||
|
||||
[Service]
|
||||
Type=simple
|
||||
User=proofsrv
|
||||
Group=proofsrv
|
||||
WorkingDirectory=/opt/language-proof-server
|
||||
EnvironmentFile=/etc/language-proof-server/proof-server.env
|
||||
Environment=HOME=/var/lib/language-proof-server
|
||||
Environment=PROOF_SERVER_HOST=0.0.0.0
|
||||
Environment=PROOF_SERVER_PORT=8787
|
||||
Environment=PROOF_REPO_DIR=/srv/research-stack
|
||||
Environment=PROOF_LEAN_ROOT=0-Core-Formalism/lean/Semantics
|
||||
Environment=PROOF_WORK_DIR=/var/lib/language-proof-server/work
|
||||
Environment=PROOF_RECEIPT_DIR=/var/lib/language-proof-server/receipts
|
||||
ExecStart=/usr/bin/python3 /opt/language-proof-server/language_proof_server.py
|
||||
Restart=on-failure
|
||||
RestartSec=5
|
||||
NoNewPrivileges=true
|
||||
PrivateTmp=true
|
||||
ProtectSystem=strict
|
||||
ProtectHome=true
|
||||
ReadWritePaths=/srv/research-stack /var/lib/language-proof-server
|
||||
CapabilityBoundingSet=
|
||||
RestrictAddressFamilies=AF_INET AF_INET6 AF_UNIX
|
||||
|
||||
[Install]
|
||||
WantedBy=multi-user.target
|
||||
UNIT
|
||||
|
||||
ssh "${SSH_OPTS[@]}" "ubuntu@${PUBLIC_IP}" 'set -euxo pipefail
|
||||
sudo chown -R proofsrv:proofsrv /opt/language-proof-server /srv/research-stack /var/lib/language-proof-server
|
||||
sudo chmod 700 /etc/language-proof-server
|
||||
sudo chmod 600 /etc/language-proof-server/token /etc/language-proof-server/proof-server.env
|
||||
if [ ! -x /var/lib/language-proof-server/.elan/bin/elan ]; then
|
||||
sudo -u proofsrv -H sh -lc "curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none"
|
||||
fi
|
||||
sudo -u proofsrv -H sh -lc "cd /srv/research-stack/0-Core-Formalism/lean/Semantics && export PATH=/var/lib/language-proof-server/.elan/bin:\$PATH && elan toolchain install \"\$(cat lean-toolchain)\" && lake update"
|
||||
sudo systemctl daemon-reload
|
||||
sudo systemctl enable --now language-proof-server.service
|
||||
sudo systemctl --no-pager --full status language-proof-server.service | sed -n "1,18p"
|
||||
'
|
||||
|
||||
echo "INSTANCE_ID=${INSTANCE_ID}"
|
||||
echo "PUBLIC_IP=${PUBLIC_IP}"
|
||||
echo "PROOF_SERVER_URL=http://${PUBLIC_IP}:8787"
|
||||
curl -fsS -H "Authorization: Bearer $(cat "$LOCAL_TOKEN_FILE")" "http://${PUBLIC_IP}:8787/health" | python3 -m json.tool
|
||||
|
|
@ -1,147 +0,0 @@
|
|||
{ config, pkgs, ... }:
|
||||
{
|
||||
imports = [ <nixpkgs/nixos/modules/virtualisation/amazon-image.nix> ];
|
||||
|
||||
networking.hostName = "aws-nixos-node-1";
|
||||
networking.firewall.allowedTCPPorts = [ 80 443 ];
|
||||
|
||||
documentation.enable = false;
|
||||
documentation.nixos.enable = false;
|
||||
documentation.man.enable = false;
|
||||
documentation.info.enable = false;
|
||||
documentation.doc.enable = false;
|
||||
|
||||
nix.settings.auto-optimise-store = true;
|
||||
nix.gc = {
|
||||
automatic = true;
|
||||
dates = "weekly";
|
||||
options = "--delete-older-than 7d";
|
||||
};
|
||||
|
||||
environment.systemPackages = with pkgs; [ tailscale python3 ];
|
||||
|
||||
services.tailscale.enable = true;
|
||||
services.tailscale.authKeyFile = "/etc/tailscale-auth.key";
|
||||
services.tailscale.extraUpFlags = [ "--ssh" ];
|
||||
|
||||
virtualisation.podman.enable = true;
|
||||
|
||||
virtualisation.oci-containers = {
|
||||
backend = "podman";
|
||||
containers = {
|
||||
heimdall = {
|
||||
image = "lscr.io/linuxserver/heimdall:latest";
|
||||
autoStart = true;
|
||||
ports = [ "127.0.0.1:8090:80" ];
|
||||
volumes = [ "/var/lib/heimdall:/config" ];
|
||||
environment = {
|
||||
PUID = "1000";
|
||||
PGID = "1000";
|
||||
TZ = "America/Chicago";
|
||||
};
|
||||
};
|
||||
forgejo = {
|
||||
image = "codeberg.org/forgejo/forgejo:1.21";
|
||||
autoStart = true;
|
||||
ports = [
|
||||
"0.0.0.0:3000:3000"
|
||||
];
|
||||
volumes = [
|
||||
"/var/lib/forgejo/data:/data"
|
||||
];
|
||||
environment = {
|
||||
USER_UID = "1000";
|
||||
USER_GID = "1000";
|
||||
FORGEJO__server__DOMAIN = "researchstack.info";
|
||||
FORGEJO__server__ROOT_URL = "https://researchstack.info/git/";
|
||||
FORGEJO__server__HTTP_PORT = "3000";
|
||||
FORGEJO__server__SSH_PORT = "22";
|
||||
};
|
||||
};
|
||||
};
|
||||
};
|
||||
|
||||
services.caddy = {
|
||||
enable = true;
|
||||
extraConfig = ''
|
||||
researchstack.info {
|
||||
handle_path /api/* {
|
||||
reverse_proxy localhost:8444
|
||||
}
|
||||
handle_path /git/* {
|
||||
reverse_proxy localhost:3000
|
||||
}
|
||||
handle_path /appflowy/* {
|
||||
reverse_proxy localhost:8000
|
||||
}
|
||||
handle {
|
||||
basic_auth {
|
||||
admin $2b$12$yUaZ1sxezq84rRDQ3Fa48OdTx52vU7bldIfmav4cwsRn227pFJQDq
|
||||
}
|
||||
reverse_proxy localhost:8090
|
||||
}
|
||||
}
|
||||
|
||||
# git.researchstack.info subdomain removed - use /git/* path instead
|
||||
'';
|
||||
};
|
||||
|
||||
systemd.services.rs-credential-server = {
|
||||
description = "Research Stack Credential Server";
|
||||
after = [ "network-online.target" "tailscaled.service" ];
|
||||
wants = [ "network-online.target" ];
|
||||
wantedBy = [ "multi-user.target" ];
|
||||
serviceConfig = {
|
||||
Type = "simple";
|
||||
User = "root";
|
||||
WorkingDirectory = "/opt/rs-surface";
|
||||
ExecStart = "/opt/rs-surface/rs-surface";
|
||||
Restart = "always";
|
||||
RestartSec = "5";
|
||||
Environment = [
|
||||
"RS_CREDENTIAL_CONFIG=/etc/rs-surface/credentials.json"
|
||||
"RS_SURFACE_PORT=8444"
|
||||
"RS_SURFACE_HOST=127.0.0.1"
|
||||
"RS_CREDENTIAL_SERVER=http://100.101.247.127:8444"
|
||||
"RS_SURFACE_NODE_ID=aws-nixos-node-1"
|
||||
];
|
||||
};
|
||||
};
|
||||
|
||||
|
||||
systemd.services.appflowy-cloud = {
|
||||
description = "AppFlowy Cloud podman-compose stack";
|
||||
after = [ "network-online.target" ];
|
||||
wants = [ "network-online.target" ];
|
||||
wantedBy = [ "multi-user.target" ];
|
||||
path = with pkgs; [ podman podman-compose ];
|
||||
serviceConfig = {
|
||||
Type = "oneshot";
|
||||
RemainAfterExit = true;
|
||||
WorkingDirectory = "/var/lib/AppFlowy-Cloud";
|
||||
ExecStart = "${pkgs.podman-compose}/bin/podman-compose -f docker-compose.minimal.yml up -d";
|
||||
ExecStop = "${pkgs.podman-compose}/bin/podman-compose -f docker-compose.minimal.yml down";
|
||||
};
|
||||
};
|
||||
|
||||
systemd.services.appflowy-backup = {
|
||||
description = "Daily AppFlowy PostgreSQL backup";
|
||||
after = [ "network-online.target" ];
|
||||
wants = [ "network-online.target" ];
|
||||
path = with pkgs; [ podman ];
|
||||
serviceConfig = {
|
||||
Type = "oneshot";
|
||||
ExecStart = "/var/lib/scripts/backup-appflowy-db.sh";
|
||||
};
|
||||
};
|
||||
|
||||
systemd.timers.appflowy-backup = {
|
||||
description = "Daily AppFlowy backup timer";
|
||||
requires = [ "appflowy-backup.service" ];
|
||||
timerConfig = {
|
||||
OnCalendar = "daily";
|
||||
Persistent = true;
|
||||
};
|
||||
wantedBy = [ "timers.target" ];
|
||||
};
|
||||
}
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
[Unit]
|
||||
Description=EC2 Idle Watchdog — power off instance after idle period
|
||||
After=network.target
|
||||
|
||||
[Service]
|
||||
Type=oneshot
|
||||
ExecStart=/usr/bin/python3 /opt/language-proof-server/ec2_idle_watchdog.py
|
||||
Environment=IDLE_MINUTES=15
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
[Unit]
|
||||
Description=Run EC2 idle watchdog every 5 minutes
|
||||
|
||||
[Timer]
|
||||
OnCalendar=*:0/5
|
||||
Persistent=true
|
||||
|
||||
[Install]
|
||||
WantedBy=timers.target
|
||||
|
|
@ -1,53 +0,0 @@
|
|||
#!/usr/bin/env python3
|
||||
"""EC2 idle watchdog: shuts down the instance after a configurable idle period."""
|
||||
|
||||
import os
|
||||
import sys
|
||||
import time
|
||||
import subprocess
|
||||
|
||||
|
||||
ACTIVITY_FILE = "/var/lib/language-proof-server/.last_activity"
|
||||
DEFAULT_IDLE_MINUTES = 15
|
||||
|
||||
|
||||
def main() -> int:
|
||||
idle_minutes_str = os.environ.get("IDLE_MINUTES", str(DEFAULT_IDLE_MINUTES))
|
||||
try:
|
||||
idle_minutes = float(idle_minutes_str)
|
||||
except ValueError:
|
||||
print(f"Invalid IDLE_MINUTES value: {idle_minutes_str!r}", file=sys.stderr)
|
||||
return 1
|
||||
|
||||
idle_seconds = idle_minutes * 60
|
||||
now = time.time()
|
||||
|
||||
if not os.path.exists(ACTIVITY_FILE):
|
||||
print(f"Activity file {ACTIVITY_FILE} missing; instance idle. Scheduling shutdown.")
|
||||
subprocess.run(["sudo", "shutdown", "-h", "+1"], check=True)
|
||||
return 0
|
||||
|
||||
try:
|
||||
with open(ACTIVITY_FILE, "r") as f:
|
||||
raw = f.read().strip()
|
||||
last_activity = float(raw)
|
||||
except (OSError, ValueError) as exc:
|
||||
print(f"Cannot read activity file {ACTIVITY_FILE}: {exc}; scheduling shutdown.")
|
||||
subprocess.run(["sudo", "shutdown", "-h", "+1"], check=True)
|
||||
return 0
|
||||
|
||||
elapsed = now - last_activity
|
||||
if elapsed > idle_seconds:
|
||||
print(
|
||||
f"Instance idle for {elapsed / 60:.1f} minutes "
|
||||
f"(threshold {idle_minutes} min). Scheduling shutdown."
|
||||
)
|
||||
subprocess.run(["sudo", "shutdown", "-h", "+1"], check=True)
|
||||
return 0
|
||||
|
||||
print(f"Idle check passed ({elapsed / 60:.1f} min < {idle_minutes} min).")
|
||||
return 0
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
sys.exit(main())
|
||||
|
|
@ -50,7 +50,7 @@ export RDS_PASSWORD=...
|
|||
|
||||
| Variable | Default | Purpose |
|
||||
|----------|---------|---------|
|
||||
| `RDS_HOST` | `database-1.cluster-c9i0w8eu8fnv.us-east-2.rds.amazonaws.com` | PostgreSQL host |
|
||||
| `RDS_HOST` | `localhost` | PostgreSQL host |
|
||||
| `RDS_PORT` | `5432` | PostgreSQL port |
|
||||
| `RDS_USER` | `postgres` | PostgreSQL user |
|
||||
| `RDS_PASSWORD` | — | Password or IAM token |
|
||||
|
|
@ -60,7 +60,7 @@ export RDS_PASSWORD=...
|
|||
|
||||
## What changed from Python
|
||||
|
||||
- No `psycopg2` / `boto3` runtime dependency — single static binary
|
||||
- No `psycopg2` runtime dependency — single static binary
|
||||
- `tokio-postgres` with `with-serde_json-1` feature for native JSONB support
|
||||
- `pgvector` vectors passed as `'[0.1,0.2,...]'::vector` text format
|
||||
- Ollama embeddings via `reqwest` instead of `requests`
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ impl RdsClient {
|
|||
return dsn;
|
||||
}
|
||||
let host = std::env::var("RDS_HOST").unwrap_or_else(|_| {
|
||||
"database-1.cluster-c9i0w8eu8fnv.us-east-2.rds.amazonaws.com".into()
|
||||
"localhost".into()
|
||||
});
|
||||
let port = std::env::var("RDS_PORT").unwrap_or_else(|_| "5432".into());
|
||||
let user = std::env::var("RDS_USER").unwrap_or_else(|_| "postgres".into());
|
||||
|
|
|
|||
|
|
@ -87,7 +87,7 @@ Credentials come from environment variables only — never hard-code them.
|
|||
| `RDS_HOST` | PostgreSQL host |
|
||||
| `RDS_PORT` | PostgreSQL port (default 5432) |
|
||||
| `RDS_USER` | PostgreSQL user |
|
||||
| `RDS_PASSWORD` / `RDS_IAM_TOKEN` | Password or RDS IAM auth token |
|
||||
| `RDS_PASSWORD` / `RDS_IAM_TOKEN` | Password or IAM auth token |
|
||||
| `RDS_DB` | Database name (default `postgres`) |
|
||||
| `RDS_DSN` | Full libpq DSN (overrides all above) |
|
||||
| `OLLAMA_HOST` | Ollama base URL (default `http://localhost:11434`) |
|
||||
|
|
@ -128,9 +128,9 @@ sudo cp systemd/ene-session-sync.{service,timer} /etc/systemd/system/
|
|||
# Create env file
|
||||
sudo mkdir -p /etc/ene-session-sync
|
||||
sudo tee /etc/ene-session-sync/env <<'EOF'
|
||||
RDS_HOST=database-1.cluster-xxxx.us-east-2.rds.amazonaws.com
|
||||
RDS_HOST=localhost
|
||||
RDS_USER=postgres
|
||||
RDS_IAM_TOKEN=<generated by aws rds generate-db-auth-token>
|
||||
RDS_PASSWORD=<set via env>
|
||||
EOF
|
||||
sudo chmod 600 /etc/ene-session-sync/env
|
||||
|
||||
|
|
|
|||
|
|
@ -122,7 +122,7 @@ fn build_dsn() -> String {
|
|||
return dsn;
|
||||
}
|
||||
let host = std::env::var("RDS_HOST")
|
||||
.unwrap_or_else(|_| "database-1.cluster-c9i0w8eu8fnv.us-east-2.rds.amazonaws.com".into());
|
||||
.unwrap_or_else(|_| "localhost".into());
|
||||
let port = std::env::var("RDS_PORT").unwrap_or_else(|_| "5432".into());
|
||||
let user = std::env::var("RDS_USER").unwrap_or_else(|_| "postgres".into());
|
||||
let password = std::env::var("RDS_PASSWORD")
|
||||
|
|
|
|||
|
|
@ -16,7 +16,7 @@ from typing import Any
|
|||
|
||||
SERVER_NAME = "remote-lean-proof"
|
||||
SERVER_VERSION = "0.1.0"
|
||||
DEFAULT_URL = "http://54.236.176.28:8787"
|
||||
DEFAULT_URL = "http://localhost:8787"
|
||||
DEFAULT_TOKEN_FILE = Path.home() / ".config/ene/language-proof-server.token"
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -232,7 +232,6 @@ fpga, systemverilog, verilog-design, math-help, physics-intuition, hardware-coun
|
|||
| lean | verify_lean_theorem | uvx lean-mcp |
|
||||
| sympy | 100+ symbolic math tools | uvx mcp-sympy |
|
||||
| contextstream | memory, search, session management | MCP server |
|
||||
| aws | AWS CLI tools (legacy — AWS instances shut down) | uvx awslabs.aws-api-mcp-server |
|
||||
|
||||
## Key Constants
|
||||
|
||||
|
|
|
|||
|
|
@ -701,13 +701,13 @@ F1 + F2 + F3 + F5
|
|||
- **Result:** systemd timer (every 15 min), triggers: snap/cold-copy/verify/forget/offload/garage-restart
|
||||
|
||||
### I4. NixOS Devcontainer Flake
|
||||
- **What:** Hermetic NixOS devcontainer with OpenGL/X11, pkg-config, openssl, full Python science stack, MCP Notion + AWS servers
|
||||
- **What:** Hermetic NixOS devcontainer with OpenGL/X11, pkg-config, openssl, full Python science stack, MCP Notion + local tool servers
|
||||
- **Deliverable:** `.devcontainer/flake.nix` + `devcontainer.json`
|
||||
- **Status:** ✅ DONE
|
||||
|
||||
### I5. Credential Gateway & EC2 Recovery
|
||||
- **What:** apiProvider service kind, credential server, cupfox routing, EC2 recovery backup (NixOS config, AppFlowy compose/env template)
|
||||
- **Deliverable:** `4-Infrastructure/infra/credential_server.py`, `4-Infrastructure/infra/ec2-configuration.nix`
|
||||
- **What:** apiProvider service kind, credential server, cupfox routing, bare-metal recovery backup (NixOS config, AppFlowy compose/env template)
|
||||
- **Deliverable:** `4-Infrastructure/infra/credential_server.py`
|
||||
- **Status:** ✅ DONE
|
||||
|
||||
### I6. Garage Replication Scale-Out (3 nodes)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue