demo/INSTALLATION.md

# PAX-Coder Demo Installation & Quick Start

## Installation

No installation required! The demo works out of the box with Python 3.10+.

```bash

cd C:/Users/jessi/Desktop/pax-coder

python3 demo/demo.py

```

## Quick Start

### 1. Default Demo (Mock Mode, RTX 3080)
```bash

python3 demo/demo.py

```
Shows all 5 kernel categories with interactive pauses between demos.

### 2. Non-Interactive (Perfect for CI/Scripting)
```bash

python3 demo/demo.py --no-pause

```
Runs all 5 demos back-to-back without pausing.

### 3. Target H100 (Hopper, sm_90)

```bash

python3 demo/demo.py --arch sm_90 --no-pause
```

Same 5 demos but with sm_90 target instead of sm_86.



### 4. Plain Text (No Colored Output)

```bash

python3 demo/demo.py --no-rich --no-pause

```
Works on minimal terminals without color support.

## Optional Dependencies

Install `rich` for prettier terminal output:
```bash

pip install rich

```

For live Ollama mode, install `requests`:
```bash

pip install requests

```

Then run Ollama in one terminal:
```bash

ollama serve

ollama run Snapkitty/pax-coder-7b  # Download model

```

And query in another:
```bash

python3 demo/demo.py --live

```

## What Each Flag Does

| Flag | Purpose | Example |
|------|---------|---------|
| `--help` | Show all options | `python3 demo.py --help` |
| `--no-pause` | Skip pauses (CI mode) | `python3 demo.py --no-pause` |
| `--no-rich` | Plain text only | `python3 demo.py --no-rich` |
| `--arch sm_90` | Target H100 (default: sm_86) | `python3 demo.py --arch sm_90` |
| `--live` | Use Ollama model | `python3 demo.py --live` |
| `--speed 2.0` | 2x faster animation | `python3 demo.py --speed 2.0` |

## Expected Output

The demo produces ~680 lines showing:

1. **Banner** (14 lines) — PAX-Coder branding + copyright
2. **5 Demos** (~130 lines each):
   - Prompt
   - Lean 4 proof
   - PTX kernel
   - Futhark spec
   - PAX certificate
3. **VRAM Stats** (~10 lines) — RTX 3080 breakdown
4. **CTA** (~10 lines) — Sovereign Node Key link
5. **Footer** (~5 lines) — GitHub/HuggingFace links

Total: 680+ lines when run with `--no-pause`.

## Output Format

Each demo shows:

```

================================================================================

DEMO 1/5: FP16

================================================================================



📋 PROMPT:

  [User's request for verified kernel]



🔍 LEAN 4 PROOF:

  [15-26 lines of Lean 4 theorem + lemmas]



⚙️  PTX KERNEL:

  [34-77 lines of Ampere/Hopper assembly]



🌐 FUTHARK SPEC:

  [10-26 lines of functional reference]



✓ PAX CERTIFICATE: [PO1 | PO3 | PO5 | PO7 | PO8]

```

## Troubleshooting

### "UnicodeEncodeError" on Windows
The demo handles UTF-8 automatically. If issues persist:
```bash

python3 demo/demo.py --no-rich --no-pause

```

### "No module named 'rich'"
Rich is optional. Just run without it:
```bash

python3 demo/demo.py --no-rich

```

### Ollama connection refused (--live)
Ensure Ollama is running:
```bash

# Terminal 1: Start Ollama server

ollama serve



# Terminal 2: Download model (first time)

ollama pull Snapkitty/pax-coder-7b



# Terminal 3: Run demo with --live

python3 demo/demo.py --live

```

## File Structure

```

pax-coder/

├── demo/

│   ├── demo.py                  ← Main demo script

│   ├── README.md                ← Full documentation

│   ├── INSTALLATION.md          ← This file

│   └── DEMO_SUMMARY.txt         ← Detailed manifest

├── PAX/                         ← Lean 4 proofs

├── src/                         ← GPU kernels

├── docs/                        ← Architecture docs

└── README.md                    ← Main project README

```

## Next Steps

1. **Run the demo**:
   ```bash

   python3 demo/demo.py --no-pause

   ```

2. **Read the architecture**:
   - See `../PAX/` for Lean 4 proofs
   - See `../src/` for actual GPU kernels
   - See `../docs/` for detailed docs

3. **Get a Sovereign Node Key** (for production):
   - Submit request: See `../CONTACT.md`
   - Select tier (Community $0, Individual $250-500, Commercial $12-25K/yr)
   - Receive provisioned authorization
   - Required for production use

4. **Fine-tune your own**:
   ```bash

   python3 ../export_training_data.py

   pip install -r ../requirements.txt

   ./run_training.sh

   ```

## License

PAX-Coder is tri-licensed:
- BSL-1.1 (until 2028-08-08)
- AGPL-3.0 (from 2028-08-08)
- MPL-2.0 (alternative)

Copyright: Ahmad Ali Parr, Bel Esprit D'Accord Irrevocable Trust

---

Happy kernel proving! 🚀