Add ephemeral paper and Lean uploads - #18
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b1a7757657
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| source: "lean", | ||
| file: activeLean.path, | ||
| selectedText, | ||
| surroundingText: activeLean.text.slice(0, 12_000), |
There was a problem hiding this comment.
For uploaded Lean files longer than 12,000 characters, highlighting code later in the file stores only the file prefix as surroundingText; uploadedExplainRequestSchema then rejects the request because the selected text is not contained in that context, so valid selections past the prefix get a generic 400 instead of an explanation. Build the bounded context around the actual selection rather than always slicing from the start.
Useful? React with 👍 / 👎.
| for (const file of sourceFiles) { | ||
| const lowerName = file.name.toLowerCase(); | ||
| if (lowerName.endsWith(".lean")) { | ||
| result.push(decodeLean(file.name, new Uint8Array(await file.arrayBuffer()))); |
There was a problem hiding this comment.
For direct .lean uploads, the browser reads the entire file into an ArrayBuffer before decodeLean enforces the 256 KiB limit. If a reader accidentally selects a very large Lean file, this can load far more data into memory than the documented resource cap permits, unlike the ZIP branch which checks file.size first. Reject oversized direct files before calling arrayBuffer().
Useful? React with 👍 / 👎.
| mappedLean: z.object({ | ||
| file: leanPathSchema, | ||
| text: z.string().trim().min(2).max(8_000), | ||
| }).strict().optional(), | ||
| mappedPaper: z.object({ page: z.number().int().min(1).max(100), text: z.string().trim().min(2).max(8_000) }).strict().optional(), |
There was a problem hiding this comment.
A crafted /api/explain-upload request can include both mappedLean and mappedPaper for either selection type because these fields are independently optional. buildUploadedExplanationContext forwards both into the model context, but only exposes the opposite-source mapping in publicContext.sources, so the model can ground or cite a hidden/conflicting mapped source that the reader never sees as evidence. Add a refinement that only accepts the mapped source type valid for the current selection, and not both.
Useful? React with 👍 / 👎.
| source: "paper", | ||
| page: pageNumber, | ||
| selectedText: value.selectedText, | ||
| surroundingText: activePage.text.slice(0, 12_000), |
There was a problem hiding this comment.
For an uploaded PDF page with more than 12,000 extracted characters, selecting a passage after that prefix stores only the start of the page as surroundingText. The upload schema requires the selected text to occur in the supplied surrounding text, so these otherwise valid page selections are rejected by /api/explain-upload with a generic invalid-context error. Slice a bounded window around the selected passage instead of always taking the page prefix.
Useful? React with 👍 / 👎.
| const browserSelection = window.getSelection()?.toString() ?? ""; | ||
| const selectedText = boundedSelection(browserSelection || activeLean.text); |
There was a problem hiding this comment.
When the browser still has text selected outside the Lean <pre>—for example after highlighting a paper passage and then switching tabs—the Explain this Lean file button uses that stale global selection instead of the file contents. If that text is not in the Lean source the request is rejected, and if it happens to match somewhere the explanation is for the wrong passage. Only use window.getSelection() when its anchor/focus are inside the active Lean source; otherwise fall back to the file text.
Useful? React with 👍 / 👎.
1 participant
Summary
/uploadworkspace for reader-provided PDF papers and optional Lean source/api/explain-uploadcontext boundaryTrust and privacy
Original PDF, Lean, and ZIP bytes stay in the browser. The server receives only the selected passage and bounded nearby text after an explicit explanation request. Uploaded context always reports verification as
not-run; it cannot inherit verification evidence from registered proof packages.ZIP inputs are bounded before expansion and reject traversal paths, absolute/backslash paths, oversized entries, invalid UTF-8, duplicates, and collection limit violations.
Validation
npm run proof:validatenpm run eval:validatenpm test— 29 files, 107 tests passednpm run typechecknpm run lintnpm run buildnpm run build:sitesnpm run test:e2e— 31 passed, 7 intentional skipsnpx playwright test tests/e2e/upload-workspace.spec.tsafter mobile coverage expansion — 4 passed across desktop and mobileReview notes
This PR intentionally does not run Lean, persist uploads, publish user material into the proof library, or claim that an uploaded Lean theorem formalizes the uploaded paper.