refactor: use a shared package

[robsimmons]

This PR moves some code into a different shared NPM workspace, which is itself separated into two exports: @leanprover/workbench-shared that can run in any setting, and @leanprover/workbench-shared/node which contains shared utilities that only work in nodeJS.

This PR mostly makes sense as preparation for a subsequent refactor that pulls VS Code session management out of next.js and into a separate "shard runner" package. In particular, because I plan to use Node.js Type Stripping for the shard runner, I added allowImportingTsExtensions: true — that permits the shared workspace to have imports that look like import { foo } from "./foo.ts", which is necessary for type stripping, without it tripping up the projects that import the shared workspace. (The shared project also requires erasableSyntaxOnly, verbatimModuleSyntax and moduleResolution: "nodenext", which enforce type strippability.)

The refactor is independently useful because it allows utility functions to be shared between Next.js and the collab-server and vscode-workbench subprojects — polling a filesystem repeatedly until a socket exists is one piece of repeated code that this eliminates, and this PR also shares a bunch of constants that previously weren't synced.

[robsimmons]

@jcreedcmu @Vtec234 this is a "does this plan for making stuff shared between projects make sense" level code review request — the actual code is basically just copy-paste-and-fixup mechanics and probably doesn't need line-by-line review, the deterministic and nondeterministic robots should be capable of detecting the mistake-in-copy-paste errors and eslint/tsc/pet-robots seem satisfied.

[robsimmons]

I copy-pasted this from its previous location (actually I changed Names to Project names because we definitely use usernames in file paths). Then the pet robots both alerted to the fact that this is not true — bwrapProjectDir, for example, uses /workspace/projectName as the project directory, which makes sense from the user's perspective but could cause issues if we added unicode names. I believe we only use project names in file paths inside the bubblewrap.

(CC @Vtec234 since you added the previous version of this note in #36)

[jcreedcmu]

The deprecation of fs.exists() is news to me that I discovered by trying to search around for why you had written this function, and I feel a little skeptical that nodejs has really offered the optimal api surface if we find ourselves wanting to write wrappers like this.

But... this is not a request for any change to this PR. I'm just noting this for the historical record. The only thing to watch out for is if we are in fact introducing any races by checking for existence and doing something assuming existence that might be invalidated by a concurrent process deleting it.

[jcreedcmu]

(and I think I'm inclined to be somewhat tolerant of races that are theoretically possible but practically extremely unlikely, as long as they have relatively benign consequences in the unlikely case)

[jcreedcmu]

also I notice that this function is merely moved not created by this PR, so no need to fixate on it.

[robsimmons]

To this end, I made the docstring a bit more pointed in 3c758e7

[jcreedcmu]

The goal of moving functionality to a common place to be shared by different bits of workbench seems desirable.