ganganray/Logic-Translation
1
0
Fork 0
Code Issues Pull requests Projects Releases 3 Packages Wiki Activity Actions
Page: Developer Guide
Pages
Admin Guide Deployment Guide Developer Guide Home Student Guide Teacher Guide
5 Developer Guide
ganganray edited this page 2026-05-05 10:07:37 +08:00
Table of Contents

Developer Guide

Architecture Overview

                     External Nginx (optional)
                     strips /logictranslation/
                              │
                              ▼
┌─────────────────────────────────────────────────────────┐
│                 Container (:3000)                         │
│  ┌────────────────────────────────────────────────────┐  │
│  │              Internal Nginx (:3000)                 │  │
│  │   /api/*  →  Backend (127.0.0.1:8000)              │  │
│  │   /*      →  Frontend (127.0.0.1:3001)             │  │
│  └────────────────────────────────────────────────────┘  │
│  ┌───────────────────┐  ┌────────────────────────────┐  │
│  │ Frontend (:3001)  │  │     Backend (:8000)         │  │
│  │ Next.js 14 (SSR)  │  │     FastAPI (async)         │  │
│  │ React 18 + TS     │  │     SQLAlchemy + Pydantic   │  │
│  │ TailwindCSS       │  │     Z3 SMT Solver           │  │
│  │ KaTeX rendering   │  │     lark parser             │  │
│  └───────────────────┘  └────────────────────────────┘  │
├─────────────────────────────────────────────────────────┤
│                    PostgreSQL 15 (:5432)                  │
│                    JSONB for flexible content             │
└─────────────────────────────────────────────────────────┘

Local Development Setup

Prerequisites

  • Docker & Docker Compose
  • Node.js 18+ (for frontend tooling outside Docker)

Start in dev mode

git clone <repo-url>
cd Logic-Translation
docker compose up -d

This mounts the source code as volumes and enables hot-reload for both services:

TypeScript checking

cd frontend && npx tsc --noEmit

Backend Architecture

Directory Structure

backend/
├── main.py                    # FastAPI app instance, CORS, router
├── requirements.txt           # Python dependencies
├── alembic/                   # Database migrations
│   └── versions/              # Migration scripts
├── alembic.ini                # Alembic configuration
├── scripts/
│   ├── init_admin.py          # First-time admin creation
│   └── reset_password.py      # CLI password reset
└── app/
    ├── api/
    │   ├── router.py          # Route registration
    │   ├── auth.py            # Login, register, change-password
    │   ├── admin.py           # User CRUD, role management
    │   ├── deps.py            # Auth dependencies (get_current_user, etc.)
    │   ├── submissions.py     # CRUD for submissions
    │   └── validity.py        # Parse formulas + Z3 validity check
    ├── core/
    │   └── security.py        # JWT, bcrypt, token creation
    ├── db/
    │   └── session.py         # SQLAlchemy async engine + session
    ├── logic/
    │   ├── latex_parser.py    # Recursive-descent parser for LaTeX → SMT-LIB
    │   └── z3_checker.py      # Z3 solver wrapper
    ├── models/
    │   └── models.py          # SQLAlchemy ORM models (User, Submission)
    └── schemas/
        └── schemas.py         # Pydantic V2 schemas (request/response)

Key Design Decisions

JSONB Content Model

Submissions use PostgreSQL JSONB columns for content and review. This allows flexible, schema-evolving data without database migrations for every field change.

# Pydantic schemas use extra="allow" to preserve unknown fields
class SubmissionContentSchema(BaseModel):
    original: Optional[OriginalProblemSchema] = ...
    formalization: Optional[FormalizationSchema] = ...
    llmChallenge: Optional[LlmChallengeSchema] = None
    model_config = ConfigDict(extra="allow")

Review History Archival

When a teacher submits a new review, the previous review is automatically archived:

{
  "review": {
    "current": { "reviewText": "...", "passed": "good", ... },
    "history": [
      { "reviewText": "...", "passed": "pending", "contentSnapshot": {...} }
    ]
  }
}

LaTeX Parser (latex_parser.py)

A custom recursive-descent parser (not using lark grammar) that:

  1. Normalizes LaTeX input (e.g., ∧ → \wedge, -> → \rightarrow)
  2. Validates well-formed formulas (WFF)
  3. Generates SMT-LIB code for Z3
  4. Supports both propositional and first-order logic
  5. Handles juxtaposition notation (e.g., Px → P(x))
  6. Enforces arity consistency for predicates

Access Control

Student  → can only CRUD their own submissions
Teacher  → can read all submissions, write reviews
Admin    → full access to everything + user management

Adding a New API Endpoint

  1. Create or edit a file in backend/app/api/
  2. Register the router in backend/app/api/router.py: 
    from .your_module import router as your_router
api_router.include_router(your_router, prefix="/your-prefix", tags=["your-tag"])
  3. Add Pydantic schemas in backend/app/schemas/schemas.py
  4. Use auth dependencies: 
    from .deps import get_current_active_user, get_current_teacher_user, get_current_admin_user

Database Migrations

# Generate a new migration after model changes
docker exec -w /app/backend logic_backend alembic revision --autogenerate -m "description"

# Apply migrations
docker exec -w /app/backend logic_backend alembic upgrade head

# Rollback one step
docker exec -w /app/backend logic_backend alembic downgrade -1

Frontend Architecture

Directory Structure

frontend/src/
├── app/                          # Next.js App Router pages
│   ├── layout.tsx                # Root layout (Navbar, Providers)
│   ├── page.tsx                  # Landing/redirect page
│   ├── login/page.tsx            # Login form
│   ├── student/page.tsx          # Student submission workspace
│   ├── teacher/page.tsx          # Teacher review panel
│   ├── admin/page.tsx            # Admin user management
│   └── change-password/page.tsx  # Password change form
├── components/
│   ├── Navbar.tsx                # Navigation bar (role-aware)
│   ├── LatexRenderer.tsx         # KaTeX rendering component
│   └── ClientProviders.tsx       # Auth + i18n context wrapper
└── utils/
    ├── api.ts                    # API base URL + login helper
    ├── auth.tsx                  # AuthProvider + useAuth hook
    ├── i18n.ts                   # Translation strings (EN/ZH)
    ├── i18nContext.tsx            # I18nProvider + useI18n hook
    └── latexParser.ts            # Frontend LaTeX normalization

Key Patterns

Auth Hydration Safety

The auth system initializes synchronously from localStorage to avoid SSR/CSR hydration mismatches:

function getInitialAuth(): AuthState {
  if (typeof window === "undefined") return { token: null, role: null, isLoggedIn: false };
  const token = localStorage.getItem("token");
  // ...
}

All pages guard with initialized:

if (!initialized || !isLoggedIn) return null;

Change Detection

The student page uses a snapshot-based dirty check:

const savedSnapshot = useRef<string>("");
const hasChanges = () => JSON.stringify(currentState) !== savedSnapshot.current;

i18n

All UI text lives in utils/i18n.ts as a flat key-value object with en and zh variants. Add new labels to both language objects.

Adding a New Page

  1. Create frontend/src/app/your-page/page.tsx
  2. Add "use client" directive at top
  3. Use useAuth() for authentication and useI18n() for translations
  4. Add the initialized guard for hydration safety
  5. Add nav link in Navbar.tsx if needed
  6. Add i18n labels in utils/i18n.ts (both EN and ZH)

Testing

Manual Testing Workflow

  1. Start dev environment: docker compose up -d
  2. Log in as each role and test features
  3. Run TypeScript check: cd frontend && npx tsc --noEmit
  4. Check backend logs: docker logs logic_backend

API Testing with curl

# Login
TOKEN=$(curl -s -X POST http://localhost:8000/auth/login \
  -H 'Content-Type: application/x-www-form-urlencoded' \
  -d 'username=admin&password=YourPass123' \
  | python3 -c "import sys,json; print(json.load(sys.stdin)['access_token'])")

# List submissions
curl -s http://localhost:8000/submissions/my \
  -H "Authorization: Bearer $TOKEN" | python3 -m json.tool

# Parse formulas
curl -s -X POST http://localhost:8000/validity/test-id/parse-formulas \
  -H "Authorization: Bearer $TOKEN" \
  -H "Content-Type: application/json" \
  -d '{"premises":["P \\\\rightarrow Q","P"],"conclusion":"Q","is_propositional":true,"entails":true}'

Building the Production Image

We recommend providing two separate tags for users on Docker Hub: one for the root path (default) and one for your specific subpath (/logictranslation).

1. Build for Root Path (Default)

# Build the default image (no subpath)
docker build -t ganganray/logic-formalization-web:latest .

# Tag and push
docker tag ganganray/logic-formalization-web:latest ganganray/logic-formalization-web:<VERSION>
docker push ganganray/logic-formalization-web:latest
docker push ganganray/logic-formalization-web:<VERSION>

2. Build for Subpath

# Build with the subpath argument
docker build -t ganganray/logic-formalization-web:latest-subpath \
  --build-arg NEXT_PUBLIC_BASE_PATH=/logictranslation \
  .

# Tag and push
docker tag ganganray/logic-formalization-web:latest-subpath ganganray/logic-formalization-web:<VERSION>-subpath
docker push ganganray/logic-formalization-web:latest-subpath
docker push ganganray/logic-formalization-web:<VERSION>-subpath