Validate project files, add order, insert version

[robsimmons]

Makes a few changes to the project validation structure.

• uses Zod parsing to take care of remaining to-dos around validating project configurations
• adds a sort order field that allows the frontend to order projects by a custom sort
• Allows project names to use templating:
  • _Vers_ will get replaced by the toolchain (e.g. v4.30.0) or by Lean if the toolchain format isn't recognized and
  • _LeanVers_ will get replaced by the toolchain plus "Lean" (e.g. Lean v4.30.0) or by Lean if the toolchain format isn't recognized

[joneugster]

Thank you for the PR, Rob :D I think these are all great ideas!

• The failing CI is just a test checking for leanprover/lean4:stable. That can be fixed easily.
• The docs need to be completed with these two new features.

[joneugster]

what's these day the recommended way of automatically follow stable releases? the file leanweb-build.sh contains lake update -R this will not be good enough to automatically update to v4.30.0, v4.31.0, ... when they are released, will it?

[robsimmons]

For live.lean-lang.org, we're currently getting the stable release by following the cslib stable tag: we literally

curl -L https://raw.githubusercontent.com/leanprover/cslib/stable/lean-toolchain | tee lean-toolchain

But this doesn't work for "latest release" where there's no corresponding tag in mathlib or cslib, and it doesn't work as soon as you want to say "I want the latest stable release where there's a version of cslib, and lean4export, and comparator"... which is also something I want. So I'm planning on doing something a bit more complicated, I can try upstreaming if it would be helpful because there's not currently a great answer here.

[joneugster]

ok that sounds even hackier indeed.

I'm going to revert that for this PR, but I'd be happy to have a look at that in another PR seperately.

Ideally lake would provide an official way for projects to update to the latest stable Lean release, something like lake update --stable. Currently, to my best knowledge, the "most official" way to follow stable Lean is setting the toolchain to stable. Therefore, I would like to keep that in this demo project.

[joneugster]

I've put all these suggestions into a commit (including fixing the tests and adding doc). It seems you've disabled pushing to the PR branch for reviewers, so it is here:

robsimmons#4

I've also added a second commit reverting the toolchain to stable and fixing the build script to update the stable toolchain. Less sure about this. I would like a way so that running the .sh script automatically updates the project to the latest stable Lean release. If you have insider knowledge how to do this correctly, please feel free to update the bash script

Feel free to take these commits as you agree and leave out parts where you don't think that's on the line of your PR.

[joneugster]

Thanks Rob for the PR! I created and merged a copy of this PR at #122, since I wanted to push a couple of fixes (fixing tests; reverting to stable toolchain - see above) before merging.

This is a setting the PR creator could enable: to allow maintainers of the repo to push directly to the PR branch.

I'm looking forward to see more fixes and features from you :)