feat: elidible subterms #3201
feat: elidible subterms #3201
Conversation
github-actions
bot
added
the
toolchain-available
|
Neat! Just based on the PR description, for lists and arrays, did you consider putting the ellipsis in the middle, in case the user cares more about what's at the end? |
|
One of the reasons why we are implementing this setting is because complete delaboration takes a significant amount of time for some users with especially large terms - it's not just for readability. Putting it somewhere in the middle would require us to traverse the full term, erasing this benefit of the option. I'm also not sure if it's easy to implement just for lists with the existing delaboration architecture (whether a term should be omitted is controlled by the function steering the delaboration, not individual delaborators - the adjusted list delaborator in this PR is merely propagating the omitted term for readability). |
|
That makes sense, thanks for the explanation! |
leanprover-community-mathlib4-bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
There was a problem hiding this comment.
The implementation looks sensible. It's a bit sad that we have to add OmissionInfo to Elab.Info. I think this is because delab-info is starting to diverge further from elab-info (you'll never get OmissionInfo from the elaborator, right?). At one point I believe we discussed splitting out a separate Delab.Info. It may be worth considering again.
|
Added |
I had the same thought when implementing this. However, it seems that all other
Do you remember where or why this was discussed? |
There was a problem hiding this comment.
This is a nice feature to have, and overall it looks like a good implementation.
There are two things I'd like to see before merging:
- Adjusting the name. I think something like
pp.omitDeepTermswith the opposite truth value would be clearer. Pretty printing deep terms is the natural default, and omitting deep terms seems like a special setting. As a counterpoint, one could argue thatpp.deepTermsfollows the convention ofpp.proofs, but as a countercounterpoint these are dissimilar because a term being a proof is an intrinsic property, but depth depends on where the expression appears. - Adding a test file. It'd be nice to see that the feature can be turned on and off, and that it can handle long lists. (Probably best to set the maxDepth low.) For test files, Sebastian suggested to me that we are using module comments to say what things are meant to be testing. (
lean/run/rawStrings.leanis one example)
| | `([$xs,*]) => `([$x, $xs,*]) | ||
| | `(⋯) => `([$x, $tail]) -- Unexpands to `[x, y, z, ⋯]` for `⋯ : List α` | ||
| | _ => throw () | ||
| | _ => throw () |
There was a problem hiding this comment.
For long lists, I guess this unexpander has been yielding quadratic complexity. Maybe eventually we should have a delaborator instead, so it can allocate the array all at once. That could also implement Joachim's suggestion to show the first and last elements of a long list. That's not for this PR though.
| @@ -251,7 +281,7 @@ partial def delab : Delab := do | |||
| else | |||
| return ← annotateTermInfo (← ``(_)) | |||
There was a problem hiding this comment.
If we wanted to adjust pp.proofs to use this new syntax, I suppose this if/else could be replaced with something like
let pf ← omission
if ← getPPOption getPPProofsWithType then
let stx ← withType delab
return ← `(($pf : $stx)) >>= annotateCurPos
else
return pfThat's untested -- I'm just wanting to record how big of a change this would be. I don't think pp.proofs should be touched in this PR.
mhuisi
force-pushed
the
mhuisi/elidible-subterms
branch
from
0ef6a90 to
fc3a3e9
Compare
There was a problem hiding this comment.
The heuristic is a good idea for handling some potential annoyances when omitting terms. Maybe in the future we might have some additional pretty printing options to control it, but I believe it's better to add them later if they're requested.
Once we have docstrings on the API functions and we decide whether or not to rename pp.maxTermDepth, then I think it'll be ready.
There was a problem hiding this comment.
Looks good to me!
(The rationale for pp.deepTerms is that, even though we think pp.omitDeepTerms is a clearer name, it's important to follow Sebastian's design for the pp options and be consistent with the analogous pp.proofs. Furthermore, this option will likely soon become a closer analogue since it too should use similar logic and use the omission syntax.)
By having the `pp.proofs` feature use `⋯` when omitting proofs, when users copy/paste terms from the InfoView the elaborator can give an error message explaining why the term cannot be elaborated. Also adds `pp.proofs.threshold` option to allow users to pretty print shallow proof terms. By default, only atomic proof terms are pretty printed. This adjustment was suggested in PR #3201, which added `⋯` and the related `pp.deepTerms` option.
By having the `pp.proofs` feature use `⋯` when omitting proofs, when users copy/paste terms from the InfoView the elaborator can give an error message explaining why the term cannot be elaborated. Also adds `pp.proofs.threshold` option to allow users to pretty print shallow proof terms. By default, only atomic proof terms are pretty printed. This adjustment was suggested in PR leanprover#3201, which added `⋯` and the related `pp.deepTerms` option.
This PR adds two new delaboration settings:
pp.deepTerms : Bool(default:true) andpp.deepTerms.threshold : Nat(default:20).Setting
pp.deepTermstofalsewill make the delaborator terminate early afterpp.deepTerms.thresholdlayers of recursion and replace the omitted subterm with the symbol⋯if the subterm is deeper thanpp.deepTerms.threshold / 4(i.e. it is not shallow). To display the omitted subterm in the InfoView,⋯can be clicked to open a popup with the delaborated subterm.InfoView with pp.deepTerms set to false (click to show image)
Implementation
⋯from regular terms, a new constructorLean.Elab.Info.ofOmissionInfois added toLean.Elab.Infothat takes a value of a new typeLean.Elab.OmissionInfo.ofOmissionInfois needed inLean.Widget.makePopupfor theLean.Widget.InteractiveDiagnostics.infoToInteractiveRPC procedure that is used to display popups when clicking on terms in the InfoView. It ensures that the expansion of an omitted subterm is delaborated usingexplicit := false, which is typically set totruein popups for regular terms.Infowidget utility functions are adjusted to supportofOmissionInfo.⋯so that long lists[x₁, ..., xₖ, ..., xₙ]are shortened to[x₁, ..., xₖ, ⋯].