Skip to content
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

refactor: Lean.Elab.Deriving.FromToJson #5292

Merged
merged 2 commits into from
Sep 10, 2024
Merged

refactor: Lean.Elab.Deriving.FromToJson #5292

merged 2 commits into from
Sep 10, 2024

Conversation

arthur-adjedj
Copy link
Contributor

Refactors the derive handlers for ToJson and FromJson in preparation for #3160.
This splits up the different parts of the handler according to how other similar handlers are implemented while keeping the original logic intact. This makes the changes necessary to adapt the file in #3160 much easier.

@arthur-adjedj
Copy link
Contributor Author

WIP

@github-actions github-actions bot added WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Sep 9, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 9, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5292
3bc1e0b
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 9, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5292
370d91c
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 9, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5292
4582307
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 9, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5292
ce82251
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Sep 9, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 10, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5292
cb9324e
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 10, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5292
24f4bab
@arthur-adjedj
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet. labels Sep 10, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@mhuisi
Copy link
Contributor

mhuisi commented Sep 10, 2024

!bench

@mhuisi
Copy link
Contributor

mhuisi commented Sep 10, 2024

Ah, we unfortunately don't have a benchmark for FromToJson (the .ilean roundtrip one uses custom handlers). Since this PR might affect language server performance, it might be good to add one to tests/bench/speedcenter.exec.velcom.yaml in a separate PR to confirm that this will not be an issue.

nomeata
nomeata reviewed Sep 10, 2024
View reviewed changes
Copy link
Collaborator

@nomeata nomeata left a comment

Choose a reason for hiding this comment

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

Looks plausible to me. How good is the test coverage, and how confident are you?

src/Lean/Elab/Deriving/FromToJson.lean Outdated
def mkFromJsonAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
let auxFunName := ctx.auxFunNames[i]!
let indval := ctx.typeInfos[i]!
let header ← mkFromJsonHeader indval --TODO fix header info
Copy link
Collaborator

Choose a reason for hiding this comment

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

Left-over TODO?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Looks like a leftover from #3160 indeed, I should remove it before merging IMO.

@nomeata nomeata changed the title chore: refactor Lean.Elab.Deriving.FromToJson.lean refactor: Lean.Elab.Deriving.FromToJson Sep 10, 2024
@nomeata
Copy link
Collaborator

nomeata commented Sep 10, 2024

Since this PR might affect language server performance,

Thanks for flagging! It wouldn’t affect performance if the generated code is going to be the same, and it’s just refactoring the meta-code, right?

@mhuisi
Copy link
Contributor

mhuisi commented Sep 10, 2024

Since this PR might affect language server performance,

Thanks for flagging! It wouldn’t affect performance if the generated code is going to be the same, and it’s just refactoring the meta-code, right?

Yes, and the benchmark would help confirm that the generated code is identical.

@arthur-adjedj
Copy link
Contributor Author

arthur-adjedj commented Sep 10, 2024 •
edited
Loading

  • How good is the test coverage ?
    There are a few tests that check the correctness of outputs from the handler, namely toFromJson.lean. These derive handlers are also heavily used in the language server, which, IIRC, is tested fairly enough in the interactive tests.
  • How confident are you ?
    I'm confident that the generated code is the same, the core logic behind the handler has stayed the same after all. Furthermore, the derive handler should behave very similarly in terms of performance.
    I'll dive into the code generated in the toFromJson.lean test, ensure it corresponds with nightly-with-mathlib and confirm that in a minute.

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 84463ab.
There were significant changes against commit c96fbdd:

  Benchmark         Metric                  Change
  ==========================================================
+ ilean roundtrip   branch-misses            -8.5% (-11.9 σ)
+ stdlib            attribute application    -1.1% (-29.5 σ)

@arthur-adjedj
Copy link
Contributor Author

Alright, here are the diffs for each ir code generated on each inductive/structure in toFromJson.lean. As far as I saw scrolling through, the only differences were in the hygienic naming, the code itself has stayed the same.

@nomeata
Copy link
Collaborator

nomeata commented Sep 10, 2024

Thanks for checking!

@nomeata nomeata added this pull request to the merge queue Sep 10, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 10, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5292
6890fe3
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 10, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5292
16176bf
Merged via the queue into leanprover:master with commit cb4a73a Sep 10, 2024
14 checks passed
@nomeata
Copy link
Collaborator

nomeata commented Sep 10, 2024

That said, a benchmark for the generated code would of course be great to have more assurance with subsequent changes. Would you be up to writing one?

@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@arthur-adjedj
Copy link
Contributor Author

That said, a benchmark for the generated code would of course be great to have more assurance with subsequent changes. Would you be up to writing one?

I'm not sure how I should go about writing such a benchmark, I have yet to write one... any indications are welcome :)
I'm also not certain of my available bandwidth to work on this in the near-future, but if it's not too time-consuming, I can probably work on that soon enough.

@nomeata
Copy link
Collaborator

nomeata commented Sep 10, 2024

I also wouldn't know. And not a requirement, just a suggestion :-)

tobiasgrosser pushed a commit to opencompl/lean4 that referenced this pull request Sep 16, 2024
@arthur-adjedj @tobiasgrosser
refactor: Lean.Elab.Deriving.FromToJson (leanprover#5292)
b7897ca 
Refactors the derive handlers for `ToJson` and `FromJson` in preparation
for leanprover#3160.
This splits up the different parts of the handler according to how other
similar handlers are implemented while keeping the original logic
intact. This makes the changes necessary to adapt the file in leanprover#3160 much
easier.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@nomeata nomeata nomeata approved these changes

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR 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.
5 participants
@arthur-adjedj @leanprover-community-bot @mhuisi @nomeata @leanprover-bot