demo/INSTALLATION.md

PAX-Coder Demo Installation & Quick Start

Installation

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

cd C:/Users/jessi/Desktop/pax-coder
python3 demo/demo.py

Quick Start

1. Default Demo (Mock Mode, RTX 3080)

python3 demo/demo.py

Shows all 5 kernel categories with interactive pauses between demos.

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

python3 demo/demo.py --no-pause

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

3. Target H100 (Hopper, sm_90)

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)

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

Works on minimal terminals without color support.

Optional Dependencies

Install rich for prettier terminal output:

pip install rich

For live Ollama mode, install requests:

pip install requests

Then run Ollama in one terminal:

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

And query in another:

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:

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

"No module named 'rich'"

Rich is optional. Just run without it:

python3 demo/demo.py --no-rich

Ollama connection refused (--live)

Ensure Ollama is running:

# 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:

   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:

   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! 🚀