Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 26 additions & 0 deletions shared/node/index.ts
Original file line number Diff line number Diff line change
Expand Up @@ -50,3 +50,29 @@ export const execFileAsync = promisify(execFile)

export * from './bwrap.ts'
export * from './directories.ts'

/**
* Turns an iterator into a ReadableStream.
* Node has had this as `ReadableStream.from` for years,
* but Next's TypeScript story expects us to always use the least-common-denominator of browser-available and node-available.
* (we should replace this with `ReadableStream.from` once typescript includes types for it).
*
* Adapted from
* https://developer.mozilla.org/en-US/docs/Web/API/ReadableStream#convert_an_iterator_or_async_iterator_to_a_stream
* which lacks the `cancel` function.
*/
export function iteratorToStream<T>(iterator: AsyncGenerator<T, void>): ReadableStream<T> {
return new ReadableStream({
async pull(controller) {
const { value, done } = await iterator.next()
if (done) {
controller.close()
} else {
controller.enqueue(value)
}
},
async cancel() {
await iterator.return()
},
})
}
1 change: 1 addition & 0 deletions src/app/[userName]/ProjectRow.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,7 @@ export function ProjectRow({
<MenuItem onAction={() => setRenaming(true)} isDisabled={actionPending}>
Rename
</MenuItem>
<MenuItem href={`/${username}/${encodeURIComponent(project.name)}/download`}>Download</MenuItem>
<MenuItem
onAction={() => {
if (!confirm(`Delete project "${project.name}"? Project files will be kept.`)) return
Expand Down
53 changes: 53 additions & 0 deletions src/app/[userName]/[projectName]/download/route.ts
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', '.'], {
Comment on lines +17 to +18

Copy link
Copy Markdown
Collaborator Author

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 .lake in its entirety. If we have overlay files in the future that aren't part of .lake I'd think those should be part of the download.

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

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The 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?

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The 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"`,
},
})
}
Loading