refactor: derive LEAN_GITHASH from src/ content instead of commit SHA#13754
Draft
Kha wants to merge 1 commit into
Draft
refactor: derive LEAN_GITHASH from src/ content instead of commit SHA#13754Kha wants to merge 1 commit into
LEAN_GITHASH from src/ content instead of commit SHA#13754Kha wants to merge 1 commit into
Conversation
… SHA This PR changes the build-embedded `LEAN_GITHASH` so it reflects the actual on-disk contents of the source tree being compiled (tracked + untracked, dirty-aware) rather than the `HEAD` commit SHA. Dev builds with uncommitted edits now embed a hash distinct from a clean build at the same commit, so `.olean` cache invalidation and `lean --githash` correctly distinguish them. Replaces `get_git_head_revision` (and the `STAGE=0+USE_LAKE` `git ls-tree` fallback with its `jj` shim) with a single `ComputeSourceHash.cmake` script invoked from a build-time `update_githash` custom target. The script lists files via `git ls-files` (falling back to `jj file list` for pure-jj workspaces), hashes each via CMake's `file(SHA256)`, and combines into a final `string(SHA256)`. Pairs with `cmake -E copy_if_different` so an unchanged hash does not trigger downstream recompilation.
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR changes the build-embedded
LEAN_GITHASHso it reflects the actual on-disk contents of the source tree being compiled (tracked + untracked, dirty-aware) rather than theHEADcommit SHA. Dev builds with uncommitted edits now embed a hash distinct from a clean build at the same commit, so.oleancache invalidation andlean --githashcorrectly distinguish them.HACK: This should either be limited to dev builds or use some new slot to preserve the githash, e.g.
--buildhash.Replaces
get_git_head_revision(and theSTAGE=0+USE_LAKEgit ls-treefallback with itsjjshim) with a singleComputeSourceHash.cmakescript invoked from a build-timeupdate_githashcustom target. The script lists files viagit ls-files(falling back tojj file listfor pure-jj workspaces), hashes each via CMake'sfile(SHA256), and combines into a finalstring(SHA256). Pairs withcmake -E copy_if_differentso an unchanged hash does not trigger downstream recompilation.