Code

[WIP] 🐕‍🦺 Cooltt Server v2.0#289

Code

Open

TOTBWF wants to merge 39 commits intomainRedPRL/cooltt:mainfrom cooltt-server-v2RedPRL/cooltt:cooltt-server-v2Copy head branch name to clipboard

+1,116-53

Commits

Commits on Aug 26, 2021

• Add socket communication code for a cooltt display server

  TOTBWF

  committed
  1bab8ff

• Add syntax for "Probe Holes"

  TOTBWF

  committed
  856f19b

• Use a 'ref' to hold the cooltt server handle

  TOTBWF

  committed
  bc5b903

• Add 'probe_goal' family of tactics

  TOTBWF

  committed
  331d422

• Add server communication inside elaborator

  TOTBWF

  committed
  2eb241f

• Server initialization + command line args

  TOTBWF

  committed
  bba9713

• Fix issue with emacs mode + extra args

  TOTBWF

  committed
  e42d970

• Update protocol to perform more heavy lifting on the cooltt side

  TOTBWF

  committed
  115b838

Commits on Aug 27, 2021

• Update zsh completion

  favonia

  committed
  f2b3c71

Commits on Sep 2, 2021

• Merge remote-tracking branch 'origin/main' into cooltt-server

  TOTBWF

  committed
  d79782d

• Replace ProbeHole with Visualize

  TOTBWF

  committed
  5a8aeb1

• Update syntax highlighting

  TOTBWF

  committed
  c30a940

• Add ability to pass in server hostname, rework options handling a bit

  TOTBWF

  committed
  10e4fff

Commits on Sep 22, 2021

• Update message format to track changes to coolttviz

  TOTBWF

  committed
  a568129

Commits on Sep 23, 2021

• Fix Test Suite

  TOTBWF

  committed
  36717bd

Commits on Nov 24, 2021

• Remove old server code

  TOTBWF

  committed
  3d8480a

• Add a message queue for emitting metadata from the refiner

  TOTBWF

  committed
  2777db2

• Thread through a null job queue into the refiner

  TOTBWF

  committed
  2beea3a

Commits on Nov 25, 2021

• Start implementing LSP server

  TOTBWF

  committed
  b03d146

• Fix some issues with the core lsp impl

  TOTBWF

  committed
  af99c13

• Add 'Executor.ml' for running server actions

  TOTBWF

  committed
  3435bfa

• Add emacs config for lsp integration

  TOTBWF

  committed
  0b24b1c

• Pull 'elaborate_typed_term' into the elaborator

  TOTBWF

  committed
  10e5aaf

• Remove job queue in favor of metadata list

  TOTBWF

  committed
  c5f6839

• Update main.ml with server command

  TOTBWF

  committed
  1306aac

• Add type hovers

  TOTBWF

  committed
  a72fd57

• Tweak printing for subtypes with trivial cofibrations

  TOTBWF

  committed
  f018ff6

Commits on Nov 28, 2021

• [WIP] Start working on holes/commands

  TOTBWF

  committed
  f2b74ff

Commits on Nov 29, 2021

• Add segment trees

  favonia

  committed
  26c8989

• Remove stupid parentheses

  favonia

  committed
  ea21988

• Refactor and clean up code

  favonia

  committed
  a9e2309

• Add a README

  favonia

  committed
  425b0f0

Commits on Nov 30, 2021

• Add visualize code action

  TOTBWF

  committed
  6ad5196

• Wire up code actions

  TOTBWF

  committed
  75cb430

• Fix minor bug in SegmentTree

  TOTBWF

  committed
  45042be

• Add some extra stuff to the segment tree API

  TOTBWF

  committed
  16ddd81

• Add pp_range

  TOTBWF

  committed
  75e8550

• Rework how metadata is stored

  TOTBWF

  committed
  34fcefa

• Remove IntervalTree

  TOTBWF

  committed
  0b0db06