Validate project files, add order, insert version#116
Conversation
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
revert? This seems accidental. But I think changing the name of the stable project to Lean _Vers_, as you had in an intermediate commit, is a good idea!
There was a problem hiding this comment.
I'll revert the typo — I undid this because it caused the Cypress tests to fail.
| function toolchainToName(toolchain, prefixLean) { | ||
| console.log(toolchain); | ||
| const nightly = toolchain.match(/^leanprover\/lean4\:nightly-(.*)$/); | ||
| if (nightly) return prefixLean ? `Lean ${nightly[1]}` : nightly[1]; |
There was a problem hiding this comment.
What it the point of having _Vers_ and _LeanVers_ when you could also name your project "Lean _Vers_"? Is there any use case for _LeanVers_ I missed?
There was a problem hiding this comment.
If you look at live.lean-lang.org right now, the default project uses _LeanVers_ — it's "Lean v4.31.0-rc0 with latest Mathlib", but if it doesn't recognize the formatting of the version it'll fall back to "Lean with latest Mathlib". Other projects use _Vers_ — "Stable Release (v4.30.0 with Mathlib, CSLib)" will fall back to "Stable Release (Lean with Mathlib, CSLib)" if the toolchain format isn't recognized. Can you suggest a good place to document this?
Also — I could definitely make do with just _Vers_ if we wanted to go simpler.
| // Secondary sort: sortOrder field | ||
| const ps = p.config.sortOrder | ||
| const qs = q.config.sortOrder | ||
| if (ps !== null && qs !== null && ps !== qs) { |
There was a problem hiding this comment.
| if (ps !== null && qs !== null && ps !== qs) { | |
| if (ps != null && qs != null && ps !== qs) { |
the potential future struggle with null !== undefined is not worth using !== imo
| return ps - qs | ||
| } | ||
| if (ps !== null && qs === null) return -1 | ||
| if (ps === null && qs !== null) return 1 |
There was a problem hiding this comment.
I've been thinking, if project with the highest number came first, this entire logic would be
if (ps != null || qs != null) return (qs ?? 0) - (ps ?? 0)wouldn't it? Would that justify sorting this way instead?
There was a problem hiding this comment.
Moreover, then one could simply say sortOrder: config.sortOrder ?? 0 as a number, couldn't we?
There was a problem hiding this comment.
yeah, I'll go with that approach
|
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: 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. |
2 participants
Makes a few changes to the project validation structure.
_Vers_will get replaced by the toolchain (e.g.v4.30.0) or byLeanif the toolchain format isn't recognized and_LeanVers_will get replaced by the toolchain plus "Lean" (e.g.Lean v4.30.0) or byLeanif the toolchain format isn't recognized