diff --git a/autoload/coqtail.vim b/autoload/coqtail.vim
index e1c6d7d2..5eb2dbe9 100644
--- a/autoload/coqtail.vim
+++ b/autoload/coqtail.vim
@@ -185,10 +185,10 @@ function! s:cleanup() abort
   silent! autocmd! coqtail#Quit * <buffer>
   silent! autocmd! coqtail#Sync * <buffer>
 
-  " Close the channel
-  silent! call b:coqtail_chan.close()
-  let b:coqtail_chan = 0
-  let b:coqtail_started = 0
+  " " Close the channel
+  " silent! call b:coqtail_chan.close()
+  " let b:coqtail_chan = 0
+  " let b:coqtail_started = 0
 
   " Clean up auxiliary panels
   call coqtail#panels#cleanup()
@@ -277,43 +277,19 @@ endfunction
 
 " Initialize Python interface.
 function! coqtail#init() abort
-  if s:port == -1
-    let s:port = py3eval(printf(
-      \ 'CoqtailServer.start_server(bool(%d))',
-      \ !g:coqtail#compat#has_channel))
-    augroup coqtail#StopServer
-      autocmd! *
-      autocmd VimLeavePre *
-        \ call py3eval('CoqtailServer.stop_server()') | let s:port = -1
-    augroup END
-  endif
+  " Prepare auxiliary panels
+  call coqtail#panels#init()
 
-  if !s:initted()
-    " Since we are initializing, we are in the main buffer;
-    " the other buffers have not been initialized yet.
-    " Thus, we can safely refer to buffer-local b: variables
-    let b:coqtail_cmds_pending = 0
-
-    " Open channel with Coqtail server
-    let b:coqtail_chan = coqtail#channel#new()
-    call b:coqtail_chan.open('localhost:' . s:port)
-    if b:coqtail_chan.status() !=# 'open'
-      call coqtail#util#err(
-        \ printf('Failed to connect to Coqtail server at port %d.', s:port))
-      return 0
-    endif
+  " Shutdown the Coqtop interface when the last instance of this buffer is
+  " closed
+  augroup coqtail#Quit
+    autocmd! * <buffer>
+    autocmd QuitPre <buffer>
+      \ if len(win_findbuf(expand('<abuf>'))) == 1 | call coqtail#stop() | endif
+  augroup END
 
-    " Prepare auxiliary panels
-    call coqtail#panels#init()
-
-    " Shutdown the Coqtop interface when the last instance of this buffer is
-    " closed
-    augroup coqtail#Quit
-      autocmd! * <buffer>
-      autocmd QuitPre <buffer>
-        \ if len(win_findbuf(expand('<abuf>'))) == 1 | call coqtail#stop() | endif
-    augroup END
-  endif
+  " Prepare the LSP backend
+  call coqtail#lsp#init()
 
   return 1
 endfunction
@@ -392,7 +368,7 @@ endfunction
 
 " Stop the Coqtop interface and clean up auxiliary panels.
 function! coqtail#stop() abort
-  call s:call('stop', 'sync', 1, {})
+  " call s:call('stop', 'sync', 1, {})
   call s:cleanup()
 endfunction
 
@@ -600,7 +576,9 @@ function! coqtail#register() abort
     " Only define commands + mappings for main buffer for now;
     " these will be redefined for the goal and info buffers
     " when those are created (when :CoqStart is called)
-    call coqtail#define_commands()
-    call coqtail#define_mappings()
+    " call coqtail#define_commands()
+    " call coqtail#define_mappings()
+
+    call coqtail#init()
   endif
 endfunction
diff --git a/autoload/coqtail/lsp.vim b/autoload/coqtail/lsp.vim
new file mode 100644
index 00000000..be269f8a
--- /dev/null
+++ b/autoload/coqtail/lsp.vim
@@ -0,0 +1,206 @@
+" Author: Wolf Honore
+" LSP configuration.
+
+let s:lsp_server_name = 'coq-lsp'
+
+let s:goal_delay = 100
+let s:progress_delay = 100
+
+function! s:register_lsp() abort
+  call lsp#register_server({
+    \ 'name': s:lsp_server_name,
+    \ 'cmd': {server_info -> ['coq-lsp']},
+    \ 'root_uri': {server_info -> lsp#utils#path_to_uri(
+      \ lsp#utils#find_nearest_parent_file_directory(
+        \ lsp#utils#get_buffer_path(),
+        \ ['.git/', '_CoqProject', 'Makefile.coq', 'dune-project']
+      \)
+    \)},
+    \ 'allowlist': ['coq']
+  \})
+
+  " Listen for `$/coq/fileProgress`
+  call lsp#callbag#pipe(
+    \ lsp#stream(),
+    \ lsp#callbag#filter({msg ->
+      \ has_key(msg, 'response')
+      \ && !has_key(msg['response'], 'error')
+      \ && get(msg['response'], 'method', '') == '$/coq/fileProgress'
+    \}),
+    \ lsp#callbag#debounceTime(s:progress_delay),
+    \ lsp#callbag#map({msg -> msg.response.params.processing}),
+    \ lsp#callbag#subscribe({'next': function('s:on_file_progress')}),
+  \)
+
+  " Listen for CursorMoved, CursorMovedI
+  call lsp#callbag#pipe(
+    \ lsp#callbag#fromEvent(['CursorMoved', 'CursorMovedI']),
+    \ lsp#callbag#debounceTime(s:goal_delay),
+    \ lsp#callbag#subscribe({'next': {_ -> s:get_goals()}})
+  \)
+endfunction
+
+function s:parse_goals(goals)
+  if a:goals == v:null
+    return []
+  endif
+
+  " Translation of python/coqtail.py:pp_goals
+  let l:lines = []
+
+  let l:ngoals = len(a:goals.goals)
+  let l:nhidden = a:goals.stack != [] ? len(a:goals.stack[0][0] + a:goals.stack[0][1]) : 0
+  let l:nshelved = len(a:goals.shelf)
+  let l:nadmit = len(a:goals.given_up)
+
+  " Information about number of remaining goals
+  let l:lines = add(l:lines, printf('%d subgoal%s', l:ngoals, l:ngoals == 1 ? '' : 's'))
+  if l:nhidden > 0
+    let l:lines = add(l:lines, printf('(%d unfocused at this level)', l:nhidden))
+  endif
+  if l:nshelved > 0 || l:nadmit > 0
+    let l:line = []
+    if l:nshelved > 0
+      let l:line = add(l:line, printf('%d shelved', l:nshelved))
+    endif
+    if l:nadmit > 0
+      let l:line = add(l:line, printf('%d admitted', l:nadmit))
+    endif
+    let l:lines = add(l:lines, join(l:line, ' '))
+  endif
+
+  let l:lines = add(l:lines, '')
+
+  " When a subgoal is finished
+  if l:ngoals == 0
+    let l:next_goal = v:null
+    for [_, l:nexts] in a:goals.stack
+      if l:nexts != []
+        let l:next_goal = l:nexts[0]
+        break
+      endif
+    endfor
+
+    if l:next_goal != v:null
+      let l:bullet = a:goals.bullet
+      let l:next_info = 'Next goal'
+      if l:next_goal.info.name != v:null
+        let l:next_info .= printf(' [%s]', l:next_goal.info.name)
+      endif
+      if l:bullet != v:null
+        let l:bullet = substitute(l:bullet, '\.$', '', '')
+        let l:next_info .= printf(' (%s)', l:bullet)
+      endif
+      let l:next_info .= ':'
+
+      let l:lines += [l:next_info, '']
+      let l:lines += split(l:next_goal.ty, '\n')
+    else
+      let l:lines = add(l:lines, 'All goals completed.')
+    endif
+  endif
+
+  for l:idx in range(len(a:goals.goals))
+    let l:goal = a:goals.goals[l:idx]
+    if l:idx == 0
+      " Print the environment only for the current goal
+      for l:hyp in l:goal.hyps
+        let l:line = printf('%s : %s', join(l:hyp.names, ', '), l:hyp.ty)
+        if l:hyp.def != v:null
+          let l:line .= printf(' := %s', l:hyp.def)
+        endif
+        let l:lines = add(l:lines, l:line)
+      endfor
+    endif
+
+    let l:hbar = printf('%s (%d / %d)', repeat('=', 25), l:idx + 1, l:ngoals)
+    if l:goal.info.name != v:null
+      let l:hbar .= printf(' [%s]', l:goal)
+    endif
+    let l:lines += ['', l:hbar, '']
+
+    let l:lines += split(l:goal.ty, '\n')
+  endfor
+
+  return l:lines
+endfunction
+
+function s:parse_messages(msgs)
+  if a:msgs == v:null
+    return []
+  endif
+
+  let l:lines = []
+  for l:msg in a:msgs
+    let l:lines = add(l:lines, l:msg.text)
+  endfor
+
+  return l:lines
+endfunction
+
+function s:on_goals(response) abort
+  let l:goal = [s:parse_goals(a:response.response.result.goals), []]
+  let l:info = [s:parse_messages(a:response.response.result.messages), []]
+  if l:goal[0] != [] || l:info[0] != []
+    call coqtail#panels#open(1)
+    call coqtail#panels#refresh(bufnr('%'), {}, {'goal': l:goal, 'info': l:info}, 0)
+  else
+    call coqtail#panels#hide()
+  endif
+endfunction
+
+function! s:get_goals() abort
+  call lsp#send_request(s:lsp_server_name, {
+    \ 'method': 'proof/goals',
+    \ 'params': {
+      \ 'textDocument': lsp#get_text_document_identifier(),
+      \ 'position': lsp#get_position()
+    \},
+    \ 'on_notification': function('s:on_goals')
+  \})
+endfunction
+
+function s:match_from_pos(sline, scol, eline, ecol) abort
+  let l:match = []
+  for l:line in range(a:sline, a:eline)
+    let l:col = l:line == a:sline ? a:scol : 1
+    let l:span = l:line == a:eline ? a:ecol - l:col : len(getline(l:line)) - l:col
+    let l:match = add(l:match, [l:line, l:col, l:span])
+  endfor
+  return l:match
+endfunction
+
+function! s:on_file_progress(processing) abort
+  let l:hls = {
+    \ 'coqtail_checked': [],
+    \ 'coqtail_sent': [],
+    \ 'coqtail_error': [],
+    \ 'coqtail_omitted': []
+  \}
+
+  for l:info in a:processing
+    let [l:sline, l:scol] = lsp#utils#position#lsp_to_vim('%', l:info.range.start)
+    let [l:eline, l:ecol] = lsp#utils#position#lsp_to_vim('%', l:info.range.end)
+    if l:info.kind == 1
+      let l:hls.coqtail_sent += s:match_from_pos(l:sline, l:scol, l:eline, l:ecol)
+    elseif l:info.kind == 2
+      let l:hls.coqtail_error += s:match_from_pos(l:sline, l:scol, l:eline, l:ecol)
+    endif
+  endfor
+
+  call coqtail#panels#refresh(bufnr('%'), l:hls, {}, 0)
+endfunction
+
+function! s:register_commands() abort
+  command! -buffer CoqGoals call <sid>get_goals()
+endfunction
+
+function coqtail#lsp#init() abort
+  if executable('coq-lsp')
+    augroup coqtail_coq_lsp
+      autocmd! *
+      autocmd User lsp_setup call s:register_lsp()
+      autocmd User lsp_buffer_enabled call s:register_commands()
+    augroup END
+  endif
+endfunction
diff --git a/autoload/coqtail/panels.vim b/autoload/coqtail/panels.vim
index 5e5c9d08..190d8062 100644
--- a/autoload/coqtail/panels.vim
+++ b/autoload/coqtail/panels.vim
@@ -161,8 +161,8 @@ function! s:open(panel, force) abort
     endfor
   endif
 
-  call coqtail#define_commands()
-  call coqtail#define_mappings()
+  " call coqtail#define_commands()
+  " call coqtail#define_mappings()
 
   call coqtail#panels#switch(l:from)
   return l:opened
@@ -312,13 +312,15 @@ function! coqtail#panels#refresh(buf, highlights, panels, scroll) abort
     let l:cur_winid = win_getid()
 
     " Update highlighting
-    for l:winid in l:winids
-      call coqtail#compat#win_call(
-        \ l:winid,
-        \ function('s:updatehl'),
-        \ [l:winid, a:highlights],
-        \ 0)
-    endfor
+    if a:highlights != {}
+      for l:winid in l:winids
+        call coqtail#compat#win_call(
+          \ l:winid,
+          \ function('s:updatehl'),
+          \ [l:winid, a:highlights],
+          \ 0)
+      endfor
+    endif
 
     " Update panels
     for [l:panel, l:panel_data] in items(a:panels)