Skip to content

fix: use a custom environment extension for LCNF decls #8468

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
zwarich merged 1 commit into from
May 25, 2025
Merged

fix: use a custom environment extension for LCNF decls #8468

zwarich merged 1 commit into from
May 25, 2025

Conversation

@zwarich
Copy link
Contributor

@zwarich zwarich commented May 24, 2025

This PR switches the LCNF baseExt/monoExt environment extensions to use a custom environment extension that uses a PersistentHashMap. The optimizer relies upon the ability to update a decl multiple times, which does not work with SimplePersistentEnvExtension.

@zwarich zwarich requested a review from Kha May 24, 2025 21:14
@zwarich zwarich requested a review from leodemoura as a code owner May 24, 2025 21:14
@zwarich zwarich added the changelog-compiler Compiler, runtime, and FFI label May 24, 2025
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label May 24, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented May 24, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a54872f5f64c9e8e0b89276384a2793b008b0078 --onto d5060e9e66aee1eee60bbeeea8ae9b9c94e29a47. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-24 21:38:45)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a54872f5f64c9e8e0b89276384a2793b008b0078 --onto 2a1354b3cc1eb05e1b67c656d2172ada8f54a937. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-25 15:14:09)

Kha
Kha reviewed May 25, 2025
View reviewed changes
src/Lean/Compiler/LCNF/PhaseExt.lean Outdated
addImportedFn := fun _ => pure {},
addEntryFn := fun s decl => s.insert decl.name decl
exportEntriesFn := sortedDecls
saveEntriesFn := sortedDecls
Copy link
Member

@Kha Kha May 25, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Already the default value

@zwarich zwarich force-pushed the lcnf-env-extension branch from a80df23 to 4dc3d6b Compare May 25, 2025 14:49
@zwarich zwarich added this pull request to the merge queue May 25, 2025
Merged via the queue into leanprover:master with commit be51365 May 25, 2025
14 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Kha Kha Kha approved these changes

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees

No one assigned

Labels

changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@zwarich @leanprover-community-bot @Kha