Code

Interactive goals & diagnostics#596

Code

Merged

leodemoura merged 51 commits intoleanprover:masterleanprover/lean4:masterfrom Vtec234:rpc-widgetsVtec234/lean4:rpc-widgetsCopy head branch name to clipboardAug 24, 2021

+1,333-373

Commits

Commits on Aug 23, 2021

• feat: MonadPrettyFormat

  Vtec234

  committed
  fe24a67

  Copy full SHA for fe24a67

• feat: pretty-printer with tags

  Vtec234

  committed
  e752c44

  Copy full SHA for e752c44

• feat: expressions with bundled environments for RPC

  Vtec234

  committed
  12484f5

  Copy full SHA for 12484f5

• feat: misc server additions

  Vtec234

  committed
  77d0c43

  Copy full SHA for 77d0c43

• feat: interactive goals

  Vtec234

  committed
  6df487a

  Copy full SHA for 6df487a

• feat: BEq Json

  Vtec234

  committed
  bee2443

  Copy full SHA for bee2443

• chore: move RpcSession

  Vtec234

  committed
  d601841

  Copy full SHA for d601841

• perf: speed up String.intercalate

  Vtec234

  committed
  ae24e93

  Copy full SHA for ae24e93

• perf: tail-recursive Json.compress

  Vtec234

  committed
  6aa18d4

  Copy full SHA for 6aa18d4

• feat: interactive diagnostics take 1

  Vtec234

  committed
  c83d61b

  Copy full SHA for c83d61b

• feat: flatten tagged text

  Show description for a6adffa
  Vtec234

  committed
  a6adffa

  Copy full SHA for a6adffa

• chore: cleanup

  Vtec234

  committed
  8db393e

  Copy full SHA for 8db393e

• chore: drop superfluous "server"

  Show description for a3650b4
  

  Vtec234

  and

  gebner

  committed
  a3650b4

  Copy full SHA for a3650b4

• feat: batch RPC release

  Vtec234

  committed
  811aeb1

  Copy full SHA for 811aeb1

• fix: text ordering

  Vtec234

  committed
  9aa592a

  Copy full SHA for 9aa592a

• feat: SubExpr support for iterating holes

  

  dselsam

  authored and

  Vtec234

  committed
  6c656b9

  Copy full SHA for 6c656b9

• feat: build info trees in delab

  

  dselsam

  authored and

  Vtec234

  committed
  2286078

  Copy full SHA for 2286078

• fix: delab structure field annotations

  Vtec234

  committed
  0203211

  Copy full SHA for 0203211

• fix: no non-expr embeds in diagnostics

  Vtec234

  committed
  2cec299

  Copy full SHA for 2cec299

• refactor: simplify delaborator monad stacks

  Vtec234

  committed
  9c97f01

  Copy full SHA for 9c97f01

• chore: Repr Syntax and minor cleanup

  Vtec234

  committed
  d3ea0d0

  Copy full SHA for d3ea0d0

• fix: tail-recursion in Format pretty-printer

  Vtec234

  committed
  40c3b9e

  Copy full SHA for 40c3b9e

• chore: log errors at identifier

  Vtec234

  committed
  944b944

  Copy full SHA for 944b944

• chore: use new deriving handler

  Vtec234

  committed
  bb44123

  Copy full SHA for bb44123

• feat: emit MessageData from Infos

  Vtec234

  committed
  9a99a47

  Copy full SHA for 9a99a47

• feat: begin integrating Elab.Info in widgets

  Vtec234

  committed
  ddeafe5

  Copy full SHA for ddeafe5

• feat: more widget Info integration

  Vtec234

  committed
  fdcd054

  Copy full SHA for fdcd054

• feat: initial TraceExplorer

  Show description for ef8f4f5
  Vtec234

  committed
  ef8f4f5

  Copy full SHA for ef8f4f5

• feat: keep-alive semantics for RPC sessions

  Vtec234

  committed
  2796ac3

  Copy full SHA for 2796ac3

• fix: syntax not updating in header snapshots

  Vtec234

  committed
  2ec7dc8

  Copy full SHA for 2ec7dc8

• perf: cache diagnostics in server

  Show description for bee3ab1
  Vtec234

  committed
  bee3ab1

  Copy full SHA for bee3ab1

• refactor: consistent naming of widget modules

  Vtec234

  committed
  cb89e6e

  Copy full SHA for cb89e6e

• chore: forgot import

  Vtec234

  committed
  690e8ed

  Copy full SHA for 690e8ed

• feat: better interactive goals

  Vtec234

  committed
  89c0f06

  Copy full SHA for 89c0f06

• chore: fix tests

  Vtec234

  committed
  642e55e

  Copy full SHA for 642e55e

• chore: support goals embedded in messages

  Vtec234

  committed
  3605e4c

  Copy full SHA for 3605e4c

• feat: unify goal handlers

  Vtec234

  committed
  495c1a2

  Copy full SHA for 495c1a2

• fix: clear messages earlier

  Vtec234

  committed
  f86a239

  Copy full SHA for f86a239

• fix: optional type for plain goal request

  Vtec234

  committed
  6b80ffe

  Copy full SHA for 6b80ffe

• chore: address some comments

  Vtec234

  committed
  375f736

  Copy full SHA for 375f736

• fix: missing instance

  Vtec234

  committed
  3fce562

  Copy full SHA for 3fce562

• chore: remove ExprWithCtx

  Vtec234

  committed
  810c78e

  Copy full SHA for 810c78e

• chore: use array for hypothesis names

  Vtec234

  committed
  d96d636

  Copy full SHA for d96d636

• chore: make rpc/connect a request

  Vtec234

  committed
  8d00852

  Copy full SHA for 8d00852

• feat: support multiple RPC sessions

  Show description for f3b8b1d
  Vtec234

  committed
  f3b8b1d

  Copy full SHA for f3b8b1d

• chore: no backticks in Name JSON

  Vtec234

  committed
  0a80286

  Copy full SHA for 0a80286

• feat: send expression range in interactive term goal

  Vtec234

  committed
  da9e941

  Copy full SHA for da9e941

• chore: bump server version

  Vtec234

  committed
  d23480a

  Copy full SHA for d23480a

• doc: diagnostic diff in snapshots

  Vtec234

  committed
  465492c

  Copy full SHA for 465492c

• feat: allow future additions to CodeWithInfos tags

  Vtec234

  committed
  b7e926e

  Copy full SHA for b7e926e

Commits on Aug 24, 2021

• doc: add review comments

  Vtec234

  committed
  0284555

  Copy full SHA for 0284555