|
| 1 | +# FireFlag - Build Instructions for Mozilla Reviewers |
| 2 | + |
| 3 | +This document explains how to build FireFlag from source code. |
| 4 | + |
| 5 | +## Prerequisites |
| 6 | + |
| 7 | +- **Deno** 2.1.4 or later (JavaScript/TypeScript runtime) |
| 8 | +- **ReScript** compiler (for .res → .js compilation) |
| 9 | +- **Idris2** 0.7.0 or later (optional - for rebuilding formally verified libraries) |
| 10 | + |
| 11 | +## Quick Build (Reviewers) |
| 12 | + |
| 13 | +The extension is **already built** - all `.res.js` files are included in the source. |
| 14 | + |
| 15 | +To verify the build: |
| 16 | + |
| 17 | +```bash |
| 18 | +# 1. Navigate to extension directory |
| 19 | +cd extension/ |
| 20 | + |
| 21 | +# 2. Package the extension |
| 22 | +zip -r ../fireflag-0.1.0.zip * -x "*.DS_Store" -x "__MACOSX/*" -x "web-ext-artifacts/*" |
| 23 | + |
| 24 | +# 3. Verify the package |
| 25 | +ls -lh ../fireflag-0.1.0.zip |
| 26 | +``` |
| 27 | + |
| 28 | +**Expected output:** `fireflag-0.1.0.zip` (approximately 122KB) |
| 29 | + |
| 30 | +## Full Build from Source (Optional) |
| 31 | + |
| 32 | +If you want to rebuild the ReScript files: |
| 33 | + |
| 34 | +### 1. Install Dependencies |
| 35 | + |
| 36 | +```bash |
| 37 | +# Install Deno (if not already installed) |
| 38 | +curl -fsSL https://deno.land/install.sh | sh |
| 39 | + |
| 40 | +# Install ReScript globally |
| 41 | +deno install -g @rescript/core |
| 42 | +``` |
| 43 | + |
| 44 | +### 2. Rebuild ReScript Files |
| 45 | + |
| 46 | +```bash |
| 47 | +# Navigate to lib/rescript directory |
| 48 | +cd extension/lib/rescript/ |
| 49 | + |
| 50 | +# Compile .res files to .res.js |
| 51 | +rescript build |
| 52 | + |
| 53 | +# OR use Deno to compile |
| 54 | +deno task build |
| 55 | +``` |
| 56 | + |
| 57 | +**Files compiled:** |
| 58 | +- `Types.res` → `Types.res.js` |
| 59 | +- `BrowserAPI.res` → (inline, no separate output) |
| 60 | +- `DevTools.res` → (inline, no separate output) |
| 61 | +- `DatabaseUpdater.res` → (inline, no separate output) |
| 62 | + |
| 63 | +### 3. Verify Compilation |
| 64 | + |
| 65 | +```bash |
| 66 | +# Check that .res.js files exist |
| 67 | +ls -l extension/lib/rescript/*.res.js |
| 68 | + |
| 69 | +# Should show: Types.res.js |
| 70 | +``` |
| 71 | + |
| 72 | +### 4. Package Extension |
| 73 | + |
| 74 | +```bash |
| 75 | +cd extension/ |
| 76 | +zip -r ../fireflag-0.1.0.zip * -x "*.DS_Store" -x "__MACOSX/*" -x "web-ext-artifacts/*" |
| 77 | +``` |
| 78 | + |
| 79 | +## Idris2 Files (Formally Verified Library) |
| 80 | + |
| 81 | +The Idris2 files in `extension/lib/idris/*.idr` are **not compiled** as part of the extension build. |
| 82 | + |
| 83 | +These files are: |
| 84 | +- Formally verified safety proofs |
| 85 | +- Type definitions with dependent types |
| 86 | +- Included for **transparency** and **auditing** |
| 87 | +- NOT executed at runtime (JavaScript implementation is separate) |
| 88 | + |
| 89 | +**Purpose:** Demonstrate formal verification of core safety logic. |
| 90 | + |
| 91 | +**To rebuild Idris2 proofs (optional, not required for extension):** |
| 92 | + |
| 93 | +```bash |
| 94 | +cd extension/lib/idris/ |
| 95 | +idris2 --build fireflag.ipkg |
| 96 | +``` |
| 97 | + |
| 98 | +This generates proof artifacts but does NOT affect the extension package. |
| 99 | + |
| 100 | +## Directory Structure |
| 101 | + |
| 102 | +``` |
| 103 | +fireflag/ |
| 104 | +├── extension/ # Extension source |
| 105 | +│ ├── manifest.json # Extension manifest |
| 106 | +│ ├── background/ # Background scripts |
| 107 | +│ ├── popup/ # Popup UI |
| 108 | +│ ├── sidebar/ # Sidebar UI |
| 109 | +│ ├── options/ # Options page |
| 110 | +│ ├── devtools/ # DevTools panel |
| 111 | +│ ├── lib/ # Libraries |
| 112 | +│ │ ├── rescript/ # ReScript source (.res) |
| 113 | +│ │ │ └── *.res.js # Compiled JavaScript |
| 114 | +│ │ ├── idris/ # Idris2 proofs (.idr) |
| 115 | +│ │ └── dom-utils.js # Safe DOM utilities |
| 116 | +│ ├── data/ # Flag database |
| 117 | +│ └── icons/ # Extension icons |
| 118 | +├── README.md # Project documentation |
| 119 | +├── LICENSE # PMPL-1.0-or-later |
| 120 | +└── BUILD_INSTRUCTIONS.md # This file |
| 121 | +``` |
| 122 | + |
| 123 | +## Build Verification |
| 124 | + |
| 125 | +To verify the build matches the submitted package: |
| 126 | + |
| 127 | +```bash |
| 128 | +# 1. Build extension |
| 129 | +cd extension/ |
| 130 | +zip -r ../fireflag-built.zip * -x "*.DS_Store" -x "__MACOSX/*" -x "web-ext-artifacts/*" |
| 131 | + |
| 132 | +# 2. Compare with submitted package |
| 133 | +cd .. |
| 134 | +unzip -l fireflag-0.1.0.zip > submitted.txt |
| 135 | +unzip -l fireflag-built.zip > built.txt |
| 136 | +diff submitted.txt built.txt |
| 137 | +``` |
| 138 | + |
| 139 | +**Expected result:** No differences (or only timestamp differences) |
| 140 | + |
| 141 | +## Third-Party Code |
| 142 | + |
| 143 | +**None.** All code is original, except: |
| 144 | +- Browser APIs (provided by Firefox) |
| 145 | +- Standard JavaScript built-ins |
| 146 | + |
| 147 | +## Code Generators Used |
| 148 | + |
| 149 | +1. **ReScript Compiler** |
| 150 | + - Version: Latest stable |
| 151 | + - Input: `.res` files (ReScript source) |
| 152 | + - Output: `.res.js` files (JavaScript) |
| 153 | + - Purpose: Type-safe JavaScript generation |
| 154 | + - Repository: https://github.com/rescript-lang/rescript-compiler |
| 155 | + |
| 156 | +2. **Idris2** (Optional, for proofs only) |
| 157 | + - Version: 0.7.0+ |
| 158 | + - Input: `.idr` files (Idris2 source) |
| 159 | + - Output: Proof artifacts (not included in extension) |
| 160 | + - Purpose: Formal verification of safety properties |
| 161 | + - Repository: https://github.com/idris-lang/Idris2 |
| 162 | + |
| 163 | +## License |
| 164 | + |
| 165 | +- **Extension Code:** PMPL-1.0-or-later (Palimpsest Meta-Project License) |
| 166 | +- **License File:** `LICENSE` in repository root |
| 167 | +- **License URL:** https://github.com/hyperpolymath/palimpsest-license |
| 168 | + |
| 169 | +## Support |
| 170 | + |
| 171 | +- **Author:** Jonathan D.A. Jewell <jonathan.jewell@open.ac.uk> |
| 172 | +- **Repository:** https://github.com/hyperpolymath/fireflag |
| 173 | +- **Issues:** https://github.com/hyperpolymath/fireflag/issues |
| 174 | + |
| 175 | +## Notes for Reviewers |
| 176 | + |
| 177 | +### Why ReScript? |
| 178 | + |
| 179 | +ReScript provides: |
| 180 | +- **Type safety:** Compile-time guarantees against common JavaScript errors |
| 181 | +- **Memory safety:** No null/undefined errors at runtime |
| 182 | +- **Performance:** Generates optimized JavaScript |
| 183 | +- **Readability:** `.res.js` output is human-readable, not minified |
| 184 | + |
| 185 | +### Why Include Idris2 Files? |
| 186 | + |
| 187 | +The Idris2 `.idr` files demonstrate: |
| 188 | +- **Formal verification:** Mathematical proofs of safety properties |
| 189 | +- **Transparency:** Auditable safety claims |
| 190 | +- **Documentation:** Self-documenting type guarantees |
| 191 | + |
| 192 | +These files are **NOT executed** - they're included for transparency and verification. |
| 193 | + |
| 194 | +### Source Code Availability |
| 195 | + |
| 196 | +All source code is available at: |
| 197 | +- **GitHub:** https://github.com/hyperpolymath/fireflag |
| 198 | +- **License:** Open source (PMPL-1.0-or-later) |
| 199 | + |
| 200 | +--- |
| 201 | + |
| 202 | +**Build Time:** < 5 seconds (ReScript compilation only) |
| 203 | +**Build Reproducibility:** Deterministic (same source → same output) |
| 204 | +**Build Dependencies:** Deno + ReScript (optional: Idris2 for proofs) |
0 commit comments