max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/interactive
History
Kyle Miller fdd5aec172
feat: better #eval command (#5627) 
This refactors and improves the `#eval` command, introducing some new
features.
* Now evaluated results can be represented using `ToExpr` and pretty
printing. This means **hoverable output**. If `ToExpr` fails, it then
tries `Repr` and then `ToString`. The `eval.pp` option controls whether
or not to try `ToExpr`.
* There is now **auto-derivation** of `Repr` instances, enabled with the
`pp.derive.repr` option (default to **true**). For example:
  ```lean
  inductive Baz
    | a | b

  #eval Baz.a
  -- Baz.a
  ```
It simply does `deriving instance Repr for Baz` when there's no way to
represent `Baz`. If core Lean gets `ToExpr` derive handlers, they could
be used here as well.
* The option `eval.type` controls whether or not to include the type in
the output. For now the default is false.
* Now things like `#eval do return 2` work. It tries using
`CommandElabM`, `TermElabM`, or `IO` when the monad is unknown.
* Now there is no longer `Lean.Eval` or `Lean.MetaEval`. These each used
to be responsible for both adapting monads and printing results. The
concerns have been split into two. (1) The `MonadEval` class is
responsible for adapting monads for evaluation (it is similar to
`MonadLift`, but instances are allowed to use default data when
initializing state) and (2) finding a way to represent results is
handled separately.
* Error messages about failed instance synthesis are now more precise.
Once it detects that a `MonadEval` class applies, then the error message
will be specific about missing `ToExpr`/`Repr`/`ToString` instances.
* Fixes a bug where `Repr`/`ToString` instances can't be found by
unfolding types "under the monad". For example, this works now:
  ```lean
  def Foo := List Nat
  def Foo.mk (l : List Nat) : Foo := l
  #eval show Lean.CoreM Foo from do return Foo.mk [1,2,3]
  ```
* Elaboration errors now abort evaluation. This eliminates some
not-so-relevant error messages.
* Now evaluating a value of type `m Unit` never prints a blank message.
* Fixes bugs where evaluating `MetaM` and `CoreM` wouldn't collect log
messages.

The `run_cmd`, `run_elab`, and `run_meta` commands are now frontends for
`#eval`.
2024-10-08 20:51:46 +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
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
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: have autoparams report parameter/field on failure (#5474) 2024-09-27 19:00:59 +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
autoBoundIssue.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +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 fix: version numbers in code actions (#2721) 2023-10-24 22:55:47 +11:00
codeaction.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
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
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 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
completionFallback.lean feat: completion fallback (#5299) 2024-09-12 16:09:20 +00:00
completionFallback.lean.expected.out feat: completion fallback (#5299) 2024-09-12 16:09:20 +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: more of BitVec.getElem_* (#5404) 2024-09-24 08:04:39 +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 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 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 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
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 feat: per-package server options (#2858) 2023-11-26 13:42:38 +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
highlight.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +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 feat: add option pp.mvars.delayed (#5643) 2024-10-08 17:48:52 +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: changing whitespace after module header may break subsequent commands (#5312) 2024-09-11 13:00:42 +00:00
incrementalCommand.lean.expected.out feat: better #eval command (#5627) 2024-10-08 20:51:46 +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
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
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 fix: auto-completion bugs and performance (#3460) 2024-02-26 09:43:19 +00: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 fix: auto-completion bugs and performance (#3460) 2024-02-26 09:43:19 +00: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 fix: auto-completion bugs and performance (#3460) 2024-02-26 09:43:19 +00:00
partialNamespace.lean
partialNamespace.lean.expected.out feat: per-package server options (#2858) 2023-11-26 13:42:38 +00:00
plainGoal.lean fix: report goals in induction with parse error 2023-11-20 09:15:27 +01:00
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 feat: rename request handler (#2462) 2023-11-21 13:10:52 +01:00
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: travelling auto-completion (#5257) 2024-09-10 07:26:44 +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