Skip to content

feat: boxed simple ground literal extraction#12727

Merged
hargoniX merged 1 commit intomasterfrom
hbv/boxed_ground_literals
Feb 27, 2026
Merged

feat: boxed simple ground literal extraction#12727
hargoniX merged 1 commit intomasterfrom
hbv/boxed_ground_literals

Conversation

@hargoniX
Copy link
Copy Markdown
Contributor

This PR implements simple ground literal extraction for boxed scalar values.

@hargoniX hargoniX requested a review from leodemoura as a code owner February 27, 2026 14:56
@hargoniX hargoniX added changelog-compiler Compiler, runtime, and FFI release-ci Enable all CI checks for a PR, like is done for releases labels Feb 27, 2026
@hargoniX
Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 27, 2026

Benchmark results for f88a5b9 against 9843794 are in! @hargoniX

  • build//instructions: -837.8M (-0.01%)

Large changes (1🟥)

  • 🟥 compiled/liasolver//instructions: +24.6M (+0.60%)

Small changes (5✅, 1🟥)

  • 🟥 build/module/Lean.Compiler.LCNF.SimpleGroundExpr//instructions: +333.0M (+5.05%) (reduced significance based on *//lines)
  • compiled/binarytrees.st//instructions: -7.9M (-0.01%)
  • compiled/hashmap//instructions: -1.4M (-0.04%)
  • compiled/qsort//instructions: -1.2M (-0.01%)
  • size/compile/.out//bytes: -7MiB (-0.36%)
  • size/libleanshared.so//bytes: -291kiB (-0.20%)

@hargoniX
Copy link
Copy Markdown
Contributor Author

release CI is broken because of general CI issues, the interesting part here was fsanitize saying yes.

@hargoniX hargoniX removed the release-ci Enable all CI checks for a PR, like is done for releases label Feb 27, 2026
@hargoniX hargoniX changed the title feat: boxed ground literal extraction feat: boxed simple ground literal extraction Feb 27, 2026
@hargoniX hargoniX enabled auto-merge February 27, 2026 16:10
@hargoniX hargoniX added this pull request to the merge queue Feb 27, 2026
Merged via the queue into master with commit 81a5eb5 Feb 27, 2026
37 of 53 checks passed
@hargoniX hargoniX deleted the hbv/boxed_ground_literals branch February 27, 2026 16:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-compiler Compiler, runtime, and FFI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants