Repository navigation
Conversation
…munity#144) Move the two private declarations extending core API out of `ImportGraph/Shake/EnvExtension.lean` into their own public modules, following the existing `ImportGraph/Lean/` layout: - `List.prependWithoutDuplicating` moves to `ImportGraph/Lean/List.lean` (root `List` namespace, so dot notation works on any list). - `Lean.PHashSet.union` moves to `ImportGraph/Lean/PersistentHashSet.lean` as `Lean.PersistentHashSet.union` (`PHashSet` is an abbrev of `PersistentHashSet`, so dot notation keeps working). Both were dead code as `private` declarations; they are now public API. The new files are intentionally not imported by the umbrella `ImportGraph.lean`. Regression tests added under `ImportGraphTest/Lean/` and registered in `ImportGraphTest.lean`. Fixes leanprover-community#144
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
1 participant
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.
Fixes #144.
ImportGraph/Shake/EnvExtension.leancontained twoprivatedeclarations extending core API, which were dead code (only self-references) precisely because they were private:List.prependWithoutDuplicating— essentially(as ++ bs).deleteDuplicatesRev, keeping later-occurring elementsLean.PHashSet.union— inserts the elements of the first set into the second unless presentThis PR moves them to their own public modules under the existing
ImportGraph/Lean/layout, as suggested in the issue:ImportGraph/Lean/List.leanprovidesList.prependWithoutDuplicating(rootListnamespace, so dot notation works on any list)ImportGraph/Lean/PersistentHashSet.leanprovidesLean.PersistentHashSet.union(PHashSetis an abbrev forPersistentHashSet, so dot notation onPHashSetvalues keeps working)Neither file is imported by the umbrella
ImportGraph.lean, per the issue description; users opt in with an explicit import.Regression tests for both functions were added as
ImportGraphTest/Lean/List.leanandImportGraphTest/Lean/PersistentHashSet.lean(following the repo's#guard_msgs in #evalstyle) and registered inImportGraphTest.lean.Verified locally against the pinned toolchain (
leanprover/lean4:v4.35.0):lake buildandlake exe graphpass, andlake build ImportGraphTestpasses for every target except the pre-existingImportGraphTest.AnotherFileWithTransitiveImports, which exceeds my local sandbox's 3 GiB memory cgroup (OOM-kill, exit 137) identically on unmodifiedmain, so it is unrelated to this change. Nosorry/admitanywhere.