Deployment Guide

Prerequisites

• Docker Engine ≥ 20.10
• Docker Compose ≥ 2.0
• (Optional) Nginx for reverse proxy with subpath

First-Time Installation

1. Get the image

Option A: Pull from Docker Hub

If you are deploying to the root path (/):

docker pull ganganray/logic-formalization-web:latest

If you are deploying to the /logictranslation subpath:

docker pull ganganray/logic-formalization-web:latest-subpath

Option B: Build from source

git clone https://github.com/ganganray/Logic-Translation.git
cd Logic-Translation

(If building from source for a subpath, see the Subpath Deployment section below).

2. Configure environment

cp .env.example .env

Edit .env — these are required:

# REQUIRED: Generate with python3 -c "import secrets; print(secrets.token_urlsafe(48))"
SECRET_KEY=your-random-secret-key-here

# REQUIRED: Strong database password
POSTGRES_PASSWORD=your-strong-db-password

# Optional: Custom admin username (default: admin)
ADMIN_USERNAME=admin

# Optional: Restrict CORS (comma-separated domains)
CORS_ORIGINS=https://your-domain.com

# Optional: For subpath deployment behind Nginx
# NEXT_PUBLIC_API_URL=/logictranslation/api

3. Start services

docker compose -f docker-compose.prod.yml up -d

4. Get initial admin password

docker logs logic_app 2>&1 | grep -A5 "INITIAL ADMIN"

Output example:

============================================================
  INITIAL ADMIN ACCOUNT CREATED
============================================================
  Username : admin
  Password : aB3xKm9pQr2sT7wZ1
============================================================
  ⚠️  Save this password — it will NOT be shown again!
============================================================

5. Verify

curl http://localhost:3000/health
curl http://localhost:3000/api/auth/login -X POST \
  -H 'Content-Type: application/x-www-form-urlencoded' \
  -d 'username=admin&password=YOUR_PASSWORD'

---

Deployment Scenarios

Root path (simplest)

Access directly at http://your-server:3000/. No external Nginx needed.

# .env — no NEXT_PUBLIC_API_URL needed (defaults to /api)
docker compose -f docker-compose.prod.yml up -d

Subpath deployment (behind Nginx)

Deploy at https://your-domain.com/logictranslation/.

To support Next.js static assets properly under a subpath, you MUST build the image with the NEXT_PUBLIC_BASE_PATH argument:

# 1. Set the base path in your .env BEFORE building
echo "NEXT_PUBLIC_BASE_PATH=/logictranslation" >> .env

# 2. Build the image (it reads the arg from .env or docker-compose)
docker compose build app

# 3. Start the service
docker compose -f docker-compose.prod.yml up -d

Then, configure your external Nginx (no rewrites needed, and NO trailing slashes!):

server {
    listen 80;
    server_name your-domain.com;

    # Notice there is NO trailing slash after /logictranslation
    location /logictranslation {
        proxy_pass http://127.0.0.1:3000;
        proxy_set_header Host $host;
        proxy_set_header X-Real-IP $remote_addr;
        proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for;
        proxy_set_header X-Forwarded-Proto $scheme;
        proxy_read_timeout 120s;
    }
}

How it works: The container dynamically generates its internal Nginx configuration on startup using the NEXT_PUBLIC_BASE_PATH. Next.js serves its app at the subpath, and the internal Nginx correctly routes /logictranslation/api/* to the backend.

---

Routine Maintenance

Database Backup

# Full backup
docker exec logic_db pg_dump -U postgres logictranslation > backup_$(date +%Y%m%d_%H%M%S).sql

# Compressed backup
docker exec logic_db pg_dump -U postgres logictranslation | gzip > backup_$(date +%Y%m%d).sql.gz

Database Restore

# From SQL file
cat backup.sql | docker exec -i logic_db psql -U postgres logictranslation

# From compressed file
gunzip -c backup.sql.gz | docker exec -i logic_db psql -U postgres logictranslation

Warning

: Restore replaces all existing data. Back up first!

Reset a User's Password

docker exec logic_app python3 /app/backend/scripts/reset_password.py <username_or_student_id> <new_password>

View Logs

# All logs
docker logs logic_app

# Follow logs in real time
docker logs -f logic_app

Update to New Version

When a new version is released (including database schema changes), follow this procedure:

# 1. Back up the database BEFORE updating
docker exec logic_db pg_dump -U postgres logictranslation > backup_$(date +%Y%m%d_%H%M%S).sql

# 2. Pull the new image (or rebuild from source)
docker pull ganganray/logic-formalization-web:latest
# For subpath: docker pull ganganray/logic-formalization-web:latest-subpath

# 3. Restart the service — database migrations run automatically on startup
docker compose -f docker-compose.prod.yml up -d

# 4. Verify the migration ran successfully
docker logs logic_app 2>&1 | grep -i "alembic\|upgrade\|migration"

How automatic migration works: The container runs alembic upgrade head on every startup (in entrypoint.sh). This applies any pending database schema changes (adding columns, indexes, etc.) without data loss. Your existing data is preserved.

If something goes wrong: Restore from the backup you created in step 1:

docker compose -f docker-compose.prod.yml down
cat backup_XXXXXXXX_XXXXXX.sql | docker exec -i logic_db psql -U postgres logictranslation
# Then revert to the previous image version and restart

Manual Database Migration

If you need to run migrations manually (e.g., for debugging):

docker exec -w /app/backend logic_app alembic upgrade head

# Check current migration version
docker exec -w /app/backend logic_app alembic current

# View migration history
docker exec -w /app/backend logic_app alembic history

---

Environment Variables Reference

Variable	Required	Default	Description
SECRET_KEY	Yes	—	JWT signing key. Must be random in production.
POSTGRES_PASSWORD	Yes	—	Database password
POSTGRES_USER	No	postgres	Database user
POSTGRES_DB	No	logictranslation	Database name
ADMIN_USERNAME	No	admin	Initial admin username
CORS_ORIGINS	No	*	Allowed CORS origins (comma-separated)
NEXT_PUBLIC_API_URL	No	/api	API URL for frontend (set to /subpath/api for subpath)
APP_PORT	No	3000	Host port for the application
Z3_TIMEOUT_PROP_MS	No	5000	Z3 timeout for propositional logic (ms)
Z3_TIMEOUT_FOL_MS	No	10000	Z3 timeout for first-order logic (ms)
Z3_MEMORY_LIMIT_MB	No	256	Z3 memory limit (MB)
SQL_ECHO	No	false	Enable SQL query logging
NEXT_PUBLIC_HEADER_TEXT	No	Mathematical Logic at Fudan	Header subtitle text (top-right corner)
NEXT_PUBLIC_HEADER_LINK	No	https://logic.fudan.edu.cn	Header subtitle link URL
NEXT_PUBLIC_ICP	No	(empty — hidden)	ICP filing / 备案号 displayed in the footer

---

Troubleshooting

Issue	Solution
"Set POSTGRES_PASSWORD in .env" error	Create .env file with POSTGRES_PASSWORD=...
Admin password lost	docker exec logic_app python3 /app/backend/scripts/reset_password.py admin NewPass123
Submissions not loading (500)	Check docker logs logic_app for migration errors
Hydration errors in browser	Hard refresh (Ctrl+Shift+R)
Z3 timeout on complex formulas	Increase Z3_TIMEOUT_FOL_MS in .env

---

UI Customization

The platform supports runtime customization of the header and footer via environment variables. No rebuild is needed — just set the values in .env and restart.

Header Subtitle

The top-right corner of every page shows a subtitle with a clickable link. By default it shows "Mathematical Logic at Fudan" linking to https://logic.fudan.edu.cn.

To customize:

# .env
NEXT_PUBLIC_HEADER_TEXT=Your Course Name
NEXT_PUBLIC_HEADER_LINK=https://your-institution.edu

Footer ICP Filing (备案号)

The footer shows the application version, copyright, and a Git repository link. Optionally, you can display an ICP filing number (required for websites hosted in mainland China):

# .env
NEXT_PUBLIC_ICP=沪ICP备XXXXXXX号

Leave empty or commented out to hide the ICP line.