Repository navigation
feat: project download #194
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,53 @@ | ||
| import { spawn } from 'node:child_process' | ||
|
|
||
| import { zProjectName, zUserName } from '@leanprover/workbench-shared' | ||
| import { getProjectDir, iteratorToStream } from '@leanprover/workbench-shared/node' | ||
| import { notFound } from 'next/navigation' | ||
| import z from 'zod' | ||
|
|
||
| import { requireAuth } from '@/lib/server/auth' | ||
| import { getDb } from '@/lib/server/db' | ||
| import { canAccessProject } from '@/lib/server/util' | ||
|
|
||
| const zParams = z.object({ | ||
| userName: zUserName, | ||
| projectName: zProjectName, | ||
| }) | ||
|
|
||
| async function* generateProjectTgz(owner: { id: string }, projectId: string): AsyncGenerator<Uint8Array, void> { | ||
| const tar = spawn('tar', ['-czf', '-', '--exclude=./.lake', '.'], { | ||
| stdio: ['ignore', 'pipe', 'inherit'], | ||
| cwd: getProjectDir(owner, projectId), | ||
| }) | ||
| const closed = new Promise(resolve => tar.on('close', resolve)) | ||
| try { | ||
| yield* tar.stdout | ||
| const code = await closed | ||
| if (code !== 0) throw new Error(`tar of project ${owner.id}/${projectId} exited with ${code}`) | ||
| } finally { | ||
| tar.kill() | ||
| } | ||
| } | ||
|
|
||
| export async function GET(_req: Request, { params }: { params: Promise<unknown> }) { | ||
| const parsed = zParams.safeParse(await params) | ||
| if (!parsed.success) return new Response(parsed.error.issues[0]!.message, { status: 400 }) | ||
| const { userName, projectName } = parsed.data | ||
|
|
||
| const session = await requireAuth() | ||
| const db = getDb() | ||
| const owner = await db.user.findUnique({ where: { name: userName } }) | ||
| if (!owner) notFound() | ||
| const project = await db.project.findUnique({ | ||
| where: { userId_name: { userId: owner.id, name: projectName } }, | ||
| }) | ||
| // 404 rather than 403 to avoid leaking the existence of inaccessible projects. | ||
| if (!project || !canAccessProject(session.user, project)) notFound() | ||
|
Comment on lines
+44
to
+45
Collaborator
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. thought that needn't be for this PR but I'm noticing a repeated pattern: should we extract a helper function that makes "check if this project seems to exist according to our current auth'ed user" easier to naturally get right?
Collaborator
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Took a crack at this for #204 |
||
|
|
||
| return new Response(iteratorToStream(generateProjectTgz(owner, project.id)), { | ||
| headers: { | ||
| 'Content-Type': 'application/gzip', | ||
| 'Content-Disposition': `attachment; filename="${project.name}.tgz"`, | ||
| }, | ||
| }) | ||
| } | ||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@Vtec234 I'm actually explicitly excluding
.lakein its entirety. If we have overlay files in the future that aren't part of.lakeI'd think those should be part of the download.