max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/interactive
History
Marc Huisinga 22d1d04059
fix: incremental goal state requests select incomplete snapshot (#6887) 
This PR fixes a bug where the goal state selection would sometimes
select incomplete incremental snapshots on whitespace, leading to an
incorrect "no goals" response. Fixes #6594, a regression that was
originally introduced in 4.11.0 by #4727.

The fundamental cause of #6594 was that the snapshot selection would
always select the first snapshot with a range that contains the cursor
position. For tactics, whitespace had to be included in this range.
However, in the test case of #6594, this meant that the snapshot
selection would also sometimes pick a snapshot before the cursor that
still contains the cursor in its whitespace, but which also does not
necessarily contain all the information needed to produce a correct goal
state. Specifically, at the `InfoTree`-level, when the cursor is in
whitespace, we distinguish competing goal states by their level of
indentation. The snapshot selection did not have access to this
information, so it necessarily had to do the wrong thing in some cases.

This PR fixes the issue by adjusting the snapshot selection for goals to
explicitly account for whitespace and indentation, and refactoring the
language processor architecture to thread enough information through to
the snapshot selection so that it can decide which snapshots to use
without having to force too many tasks, which would destroy
incrementality in goal state requests.

Specifically, this PR makes the following adjustments:
- Refactor `SnapshotTask` to contain both a `Syntax` and a `Range`.
Before, `SnapshotTask`s had a single range that was used both for
displaying file progress information and for selecting snapshots in
server requests. For most snapshots, this range did not include
whitespace, though for tactics it did. Now, the `reportingRange` field
of `SnapshotTask` is intended exclusively for reporting file progress
information, and the `Syntax` is used for selecting snapshots in server
requests. Importantly, the `Syntax` contains the full range information
of the snapshot, i.e. its regular range and its range including
whitespace.
- Adjust all call-sites of `SnapshotTask` to produce a reasonable
`Syntax`.
- Adjust the goal snapshot selection to account for whitespace and
indentation, as the `InfoTree` goal selection does.
- Fix a bug in the snapshot tree tracing that would cause it to render
the `Info` of a snapshot at the wrong location when `trace.Elab.info`
was also set.

This PR is based on #6329.
2025-02-14 11:53:24 +00:00
..
533.lean
533.lean.expected.out feat: allow structure in mutual blocks (#6125) 2024-11-22 09:20:07 +00:00
863.lean
863.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
1031.lean
1031.lean.expected.out
1265.lean
1265.lean.expected.out fix: auto-completion performance regression (#6794) 2025-01-27 21:15:09 +00:00
1403.lean
1403.lean.expected.out feat: update omega/solve_by_elim to use new tactic syntax, use new tactic syntax (#5932) 2024-11-03 16:23:37 +00:00
1525.lean
1525.lean.expected.out
1659.lean
1659.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
2058.lean feat: localize universe metavariable errors at let bindings and fun binders (#5402) 2024-09-24 05:30:42 +00:00
2058.lean.expected.out feat: localize universe metavariable errors at let bindings and fun binders (#5402) 2024-09-24 05:30:42 +00:00
2881.lean fix: some goal state issues (#5677) 2024-10-17 12:09:54 +00:00
2881.lean.expected.out fix: some goal state issues (#5677) 2024-10-17 12:09:54 +00:00
4078.lean fix: hovers on binders with metavariables (#4192) 2024-05-21 10:34:58 +00:00
4078.lean.expected.out fix: hovers on binders with metavariables (#4192) 2024-05-21 10:34:58 +00:00
4880.lean fix: ensure autoparam errors have correct positions (#4926) 2024-08-06 22:27:51 +00:00
4880.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
5659.lean fix: proper "excess binders" error locations for rintro and intro (#6565) 2025-01-08 08:36:45 +00:00
5659.lean.expected.out fix: proper "excess binders" error locations for rintro and intro (#6565) 2025-01-08 08:36:45 +00:00
6594.lean fix: incremental goal state requests select incomplete snapshot (#6887) 2025-02-14 11:53:24 +00:00
6594.lean.expected.out fix: incremental goal state requests select incomplete snapshot (#6887) 2025-02-14 11:53:24 +00:00
amb.lean
amb.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
anonHyp.lean
anonHyp.lean.expected.out feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat (#3629) 2024-03-09 15:31:51 +00:00
autoBoundIssue.lean feat: upstream definition of Vector from Batteries (#6197) 2024-11-24 23:01:32 +00:00
autoBoundIssue.lean.expected.out feat: upstream definition of Vector from Batteries (#6197) 2024-11-24 23:01:32 +00:00
builtinCodeactions.lean fix: line break in simp? output (#6048) 2024-11-13 15:49:11 +00:00
builtinCodeactions.lean.expected.out fix: line break in simp? output (#6048) 2024-11-13 15:49:11 +00:00
catHover.lean chore: fix spelling mistakes in tests (#5439) 2024-09-24 03:22:53 +00:00
catHover.lean.expected.out chore: fix spelling mistakes in tests (#5439) 2024-09-24 03:22:53 +00:00
codeaction.lean
codeaction.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
compHeader.lean
compHeader.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completion.lean
completion.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completion2.lean
completion2.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completion3.lean
completion3.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completion4.lean
completion4.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completion5.lean
completion5.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completion6.lean
completion6.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completion7.lean
completion7.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completionAtPrint.lean feat: Environment.addConstAsync (#6691) 2025-01-19 02:00:16 +00:00
completionAtPrint.lean.expected.out feat: Environment.addConstAsync (#6691) 2025-01-19 02:00:16 +00:00
completionBracketedDot.lean fix: travelling auto-completion (#5257) 2024-09-10 07:26:44 +00:00
completionBracketedDot.lean.expected.out fix: travelling auto-completion (#5257) 2024-09-10 07:26:44 +00:00
completionCheck.lean fix: auto-completion bugs and performance (#3460) 2024-02-26 09:43:19 +00:00
completionCheck.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completionDanglingDot.lean fix: don't issue atomic id completions when there is a dangling dot (#5837) 2024-11-19 12:23:41 +00:00
completionDanglingDot.lean.expected.out fix: don't issue atomic id completions when there is a dangling dot (#5837) 2024-11-19 12:23:41 +00:00
completionDeprecation.lean feat: denote deprecations in completion items (#5707) 2024-10-14 13:05:16 +00:00
completionDeprecation.lean.expected.out fix: auto-completion performance regression (#6794) 2025-01-27 21:15:09 +00:00
completionEOF.lean
completionEOF.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completionFallback.lean feat: completion fallback (#5299) 2024-09-12 16:09:20 +00:00
completionFallback.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completionFromExpectedType.lean fix: auto-completion bugs and performance (#3460) 2024-02-26 09:43:19 +00:00
completionFromExpectedType.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completionIStr.lean
completionIStr.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completionOpenNamespaces.lean fix: auto-completion bugs and performance (#3460) 2024-02-26 09:43:19 +00:00
completionOpenNamespaces.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completionOption.lean
completionOption.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completionPrefixIssue.lean
completionPrefixIssue.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completionPrivateTypes.lean fix: auto-completion bugs and performance (#3460) 2024-02-26 09:43:19 +00:00
completionPrivateTypes.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
completionPrv.lean
completionPrv.lean.expected.out fix: auto-completion performance regression (#6794) 2025-01-27 21:15:09 +00:00
completionStructureInstance.lean fix: use sensible notion of indentation in structure instance field completion (#6279) 2024-12-02 09:37:12 +00:00
completionStructureInstance.lean.expected.out fix: use sensible notion of indentation in structure instance field completion (#6279) 2024-12-02 09:37:12 +00:00
completionTactics.lean fix: use sensible notion of indentation in structure instance field completion (#6279) 2024-12-02 09:37:12 +00:00
completionTactics.lean.expected.out fix: use sensible notion of indentation in structure instance field completion (#6279) 2024-12-02 09:37:12 +00:00
compNamespace.lean
compNamespace.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
definition.lean
definition.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
Diff.lean
Diff.lean.expected.out
discrsIssue.lean
discrsIssue.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
dotIdCompletion.lean
dotIdCompletion.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
editAfterError.lean feat: incremental elaboration of definition headers, bodies, and tactics (#3940) 2024-05-22 13:23:30 +00:00
editAfterError.lean.expected.out feat: incremental elaboration of definition headers, bodies, and tactics (#3940) 2024-05-22 13:23:30 +00:00
editCompletion.lean feat: incremental elaboration of definition headers, bodies, and tactics (#3940) 2024-05-22 13:23:30 +00:00
editCompletion.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
expectedTypeAsGoal.lean
expectedTypeAsGoal.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
explicitAppInstHole.lean fix: refine how named arguments suppress explicit arguments (#5283) 2024-09-27 20:14:29 +00:00
explicitAppInstHole.lean.expected.out feat: add option pp.mvars.delayed (#5643) 2024-10-08 17:48:52 +00:00
foldingRange.lean
foldingRange.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
ghostGoals.lean fix: ghost goals in autoparam tactic block (#6408) 2024-12-17 20:57:39 +00:00
ghostGoals.lean.expected.out fix: ghost goals in autoparam tactic block (#6408) 2024-12-17 20:57:39 +00:00
goalEOF.lean
goalEOF.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
goalIssue.lean
goalIssue.lean.expected.out feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat (#3629) 2024-03-09 15:31:51 +00:00
goTo.lean
goTo.lean.expected.out fix: include references in attributes in call hierarchy (#5650) 2024-10-18 15:38:32 +00:00
goTo2.lean
goTo2.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
haveInfo.lean feat: incremental have (#4308) 2024-06-04 09:12:27 +00:00
haveInfo.lean.expected.out feat: incremental have (#4308) 2024-06-04 09:12:27 +00:00
highlight.lean fix: avoid new term info around def bodies (#6031) 2024-11-11 14:54:59 +00:00
highlight.lean.expected.out fix: avoid new term info around def bodies (#6031) 2024-11-11 14:54:59 +00:00
hover.lean feat: hover / go-to-def for attribute cmd (#3896) 2024-04-13 07:13:25 +00:00
hover.lean.expected.out doc: add recommended spellings for many term notations (#6886) 2025-02-03 13:46:39 +00:00
hoverAt.lean
hoverAt.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
hoverBinderUndescore.lean
hoverBinderUndescore.lean.expected.out feat: add option pp.mvars.delayed (#5643) 2024-10-08 17:48:52 +00:00
hoverDot.lean
hoverDot.lean.expected.out feat: add missing theorems for + 1 and - 1 normal form (#4242) 2024-06-17 05:35:32 +00:00
hoverException.lean
hoverException.lean.expected.out feat: @[builtin_doc] attribute (part 2) (#3918) 2024-09-13 08:05:10 +00:00
hoverTacticExt.lean feat: more infrastructure for tactic documentation (#4490) 2024-06-21 12:49:30 +00:00
hoverTacticExt.lean.expected.out feat: more infrastructure for tactic documentation (#4490) 2024-06-21 12:49:30 +00:00
incrementalCombinator.lean fix: disable incrementality in case .. | .. (#5090) 2024-08-19 09:17:03 +00:00
incrementalCombinator.lean.expected.out fix: disable incrementality in case .. | .. (#5090) 2024-08-19 09:17:03 +00:00
incrementalCommand.lean fix: reparsing may need to backtrack two commands (#6236) 2024-11-27 13:06:57 +00:00
incrementalCommand.lean.expected.out fix: reparsing may need to backtrack two commands (#6236) 2024-11-27 13:06:57 +00:00
incrementalInduction.lean feat: incremental elaboration of definition headers, bodies, and tactics (#3940) 2024-05-22 13:23:30 +00:00
incrementalInduction.lean.expected.out feat: incremental elaboration of definition headers, bodies, and tactics (#3940) 2024-05-22 13:23:30 +00:00
incrementalMutual.lean fix: calculate error suppression per snapshot (#4657) 2024-07-08 09:54:43 +00:00
incrementalMutual.lean.expected.out fix: calculate error suppression per snapshot (#4657) 2024-07-08 09:54:43 +00:00
incrementalTactic.lean fix: calculate error suppression per snapshot (#4657) 2024-07-08 09:54:43 +00:00
incrementalTactic.lean.expected.out fix: proper "excess binders" error locations for rintro and intro (#6565) 2025-01-08 08:36:45 +00:00
infoIssues.lean
infoIssues.lean.expected.out feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat (#3629) 2024-03-09 15:31:51 +00:00
internalNamesIssue.lean
internalNamesIssue.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
inWordCompletion.lean feat: BitVec.ofNatLt and updates to use it (#3430) 2024-02-21 18:02:56 +00:00
inWordCompletion.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
issue4527.lean fix: cdot parser error message range (#4528) 2024-06-21 15:06:07 +00:00
issue4527.lean.expected.out fix: cdot parser error message range (#4528) 2024-06-21 15:06:07 +00:00
issue5021.lean fix: hover text over _ in ?_ (#5118) 2024-08-21 20:47:19 +00:00
issue5021.lean.expected.out feat: add option pp.mvars.delayed (#5643) 2024-10-08 17:48:52 +00:00
issue5597.lean fix: declareSimpLikeTactic macro to use mkSynthetic (#5838) 2024-10-30 14:27:56 +00:00
issue5597.lean.expected.out fix: declareSimpLikeTactic macro to use mkSynthetic (#5838) 2024-10-30 14:27:56 +00:00
jumpMutual.lean
jumpMutual.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
keywordCompletion.lean
keywordCompletion.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
lean3HoverIssue.lean
lean3HoverIssue.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
macroGoalIssue.lean
macroGoalIssue.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
match.lean
match.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
matchPatternHover.lean
matchPatternHover.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
matchStxCompletion.lean
matchStxCompletion.lean.expected.out feat: structure auto-completion & partial InfoTrees 2024-11-19 09:26:58 +01:00
partialNamespace.lean
partialNamespace.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
plainGoal.lean
plainGoal.lean.expected.out fix: discrepancy theorem vs example (#4493) 2024-06-24 01:18:41 +00:00
plainTermGoal.lean
plainTermGoal.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
rename.lean
rename.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
run.lean chore: move Lean.Data.Parsec to Std.Internal.Parsec (#5115) 2024-08-21 15:26:17 +00:00
stdOutput.lean
stdOutput.lean.expected.out
terminationBySuggestion.lean feat: termination_by structural (#4542) 2024-07-01 16:51:30 +00:00
terminationBySuggestion.lean.expected.out feat: termination_by structural (#4542) 2024-07-01 16:51:30 +00:00
test_single.sh
travellingCompletions.lean fix: travelling auto-completion (#5257) 2024-09-10 07:26:44 +00:00
travellingCompletions.lean.expected.out fix: auto-completion performance regression (#6794) 2025-01-27 21:15:09 +00:00
unterminatedDocComment.lean feat: incremental elaboration of definition headers, bodies, and tactics (#3940) 2024-05-22 13:23:30 +00:00
unterminatedDocComment.lean.expected.out feat: incremental elaboration of definition headers, bodies, and tactics (#3940) 2024-05-22 13:23:30 +00:00
userWidget.lean feat: bundle of widget improvements (#2964) 2023-12-21 06:24:33 +00:00
userWidget.lean.expected.out feat: bundle of widget improvements (#2964) 2023-12-21 06:24:33 +00:00