Kyle Miller 6c1f8a8a63 fix: ensure autoparam errors have correct positions (#4926) ... Autoparam tactic scripts have no source positions, which until recently made it so that any errors or messages would be logged at the current ref, which was the application or structure instance being elaborated. However, with the new incrementality features the ref is now carefully managed to avoid leakage of outside data. This inhibits the elaborator's ref from being used for the tactic's ref, causing messages to be placed at the beginning of the file rather than on the syntax that triggered the autoparam. To fix this, now the elaborators insert the ref's source position everywhere into the autoparam tactic script. If in the future messages for synthetic tactics appear at the tops of files in other contexts, we should consider an approach where `Lean.Elab.Term.withReuseContext` uses something like `replaceRef` to set the ref while disabling incrementality when the tactic does not contain source position information. Closes #4880		2024-08-06 22:27:51 +00:00
..
533.lean
533.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
863.lean
863.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
1031.lean
1031.lean.expected.out
1265.lean
1265.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
1403.lean
1403.lean.expected.out	feat: do not instantiate metavariables in kabstract/rw for disallowed occurrences (#2539)	2024-01-03 00:01:40 +00:00
1525.lean
1525.lean.expected.out
1659.lean
1659.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +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	fix: ensure autoparam errors have correct positions (#4926)	2024-08-06 22:27:51 +00:00
amb.lean
amb.lean.expected.out
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
autoBoundIssue.lean.expected.out
catHover.lean
catHover.lean.expected.out
codeaction.lean
codeaction.lean.expected.out
compHeader.lean
compHeader.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion.lean
completion.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion2.lean
completion2.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion3.lean
completion3.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion4.lean
completion4.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion5.lean
completion5.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion6.lean
completion6.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completion7.lean
completion7.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionAtPrint.lean
completionAtPrint.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionCheck.lean	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionCheck.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionDocString.lean
completionDocString.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionEOF.lean
completionEOF.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionFromExpectedType.lean	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionFromExpectedType.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionIStr.lean
completionIStr.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionOpenNamespaces.lean	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionOpenNamespaces.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionOption.lean
completionOption.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionPrefixIssue.lean
completionPrefixIssue.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionPrivateTypes.lean	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionPrivateTypes.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
completionPrv.lean
completionPrv.lean.expected.out	feat: BitVec.ofBoolListLE and theorems (#3721)	2024-03-21 04:48:29 +00:00
compNamespace.lean
compNamespace.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
definition.lean
definition.lean.expected.out
Diff.lean
Diff.lean.expected.out
discrsIssue.lean
discrsIssue.lean.expected.out
dotIdCompletion.lean
dotIdCompletion.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00: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: incremental elaboration of definition headers, bodies, and tactics (#3940)	2024-05-22 13:23:30 +00:00
expectedTypeAsGoal.lean
expectedTypeAsGoal.lean.expected.out
fieldCompletion.lean
fieldCompletion.lean.expected.out	chore: set literal notation (#3348)	2024-02-19 23:22:36 +00:00
foldingRange.lean
foldingRange.lean.expected.out
goalEOF.lean
goalEOF.lean.expected.out
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
goTo2.lean
goTo2.lean.expected.out
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
highlight.lean.expected.out
hover.lean	feat: hover / go-to-def for attribute cmd (#3896)	2024-04-13 07:13:25 +00:00
hover.lean.expected.out	feat: add missing theorems for + 1 and - 1 normal form (#4242)	2024-06-17 05:35:32 +00:00
hoverAt.lean
hoverAt.lean.expected.out
hoverBinderUndescore.lean
hoverBinderUndescore.lean.expected.out
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
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	feat: incremental next and tactic if (#4459)	2024-06-18 12:36:59 +00:00
incrementalCombinator.lean.expected.out	feat: incremental next and tactic if (#4459)	2024-06-18 12:36:59 +00:00
incrementalCommand.lean	feat: trailing whitespace changes should not invalidate imports (#4580)	2024-07-24 13:08:01 +00:00
incrementalCommand.lean.expected.out	feat: trailing whitespace changes should not invalidate imports (#4580)	2024-07-24 13:08:01 +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	feat: PProd syntax (part 3) (#4756)	2024-07-16 21:06:04 +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	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
inWordCompletion.lean	feat: BitVec.ofNatLt and updates to use it (#3430)	2024-02-21 18:02:56 +00:00
inWordCompletion.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00: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
jumpMutual.lean
jumpMutual.lean.expected.out
keywordCompletion.lean
keywordCompletion.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
lean3HoverIssue.lean
lean3HoverIssue.lean.expected.out
macroGoalIssue.lean
macroGoalIssue.lean.expected.out
match.lean
match.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
matchPatternHover.lean
matchPatternHover.lean.expected.out
matchStxCompletion.lean
matchStxCompletion.lean.expected.out	fix: auto-completion bugs and performance (#3460)	2024-02-26 09:43:19 +00:00
partialNamespace.lean
partialNamespace.lean.expected.out
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
rename.lean
rename.lean.expected.out
run.lean	feat: generalized Parsec (#4774)	2024-08-06 15:17:23 +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
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
userWidget.lean.expected.out