feat: template creation in the admin menu

[robsimmons]

This PR makes it possible to create templates in the admin menu. Addresses (but does not close) #21. After selecting an installed toolchain, the interface will let you select:

• A "Basic Lean" template, similar to the seed script's "hello" template
• A "Mathlib template", identical (or nearly identical) to the seed script's mathlib template
• A "CSLib template", like the mathlib tempate but for cslib

The Mathlib and CSLib options will only be presented for standard release toolchains (no nightly-testing) where we've checked that the tag corresponds to a valid Mathlib/CSLib (respectively) tag. This is done with the GitHub API, and uses the higher 5000-requests-an-hour rate limit by authorizing with the configured GitHub OAuth App.

[jcreedcmu]

Is it the case that seed-volume.sh makes package-sets/mathlib-$LEAN_VERSION e.g. mathlib-v4.32.0 and yet create-tagged-lib.sh makes package-sets/mathlib-${LEAN_VERSION//./-} e.g. mathlib-v4-32-0? Seems like it would be better to be consistent. (I think the template name always has dashes in either path)

[jcreedcmu]

Also: totally optional but I think I would add like padding: 0.5em to the <select> tags that hold "Installed Toolchain" and "Template Schema".

[robsimmons]

Is it the case that seed-volume.sh makes package-sets/mathlib-$LEAN_VERSION e.g. mathlib-v4.32.0 and yet create-tagged-lib.sh makes package-sets/mathlib-${LEAN_VERSION//./-} e.g. mathlib-v4-32-0? Seems like it would be better to be consistent. (I think the template name always has dashes in either path)

It would be better to be consistent - but it might be better to be consistent between package-sets and templates, leave this PR's behavior alone, and let the seed-volume.sh behavior go away anyway in #121. Do you agree?

[jcreedcmu]

Is it the case that seed-volume.sh makes package-sets/mathlib-$LEAN_VERSION e.g. mathlib-v4.32.0 and yet create-tagged-lib.sh makes package-sets/mathlib-${LEAN_VERSION//./-} e.g. mathlib-v4-32-0? Seems like it would be better to be consistent. (I think the template name always has dashes in either path)

It would be better to be consistent - but it might be better to be consistent between package-sets and templates, leave this PR's behavior alone, and let the seed-volume.sh behavior go away anyway in #121. Do you agree?

ah, if #121 obviates this, then my concern is moot. Thanks for explaining.

[jcreedcmu]

Approved now given changes you are planning.