Skip to content

Latest commit

 

History

History
96 lines (64 loc) · 3.02 KB

todo.org

File metadata and controls

96 lines (64 loc) · 3.02 KB

This TODO file is a draft, for now we organize it in terms of Coq todos, and coq-lsp todos. We also include some other interesting info.

Coq LSP Todos

  • profit from command refinement
  • lsp server process and coq-lsp-checker client for every document
  • dune integration, auto-build, dap
  • documentation links
  • jump to definition
  • integration with tracing
  • warnings suggestions / fix
  • flags for coq process
  • Implement onsave => compile vo file? [see on-disk cache issues below]

On-disk cache:

This is a complex topic due to sharing; for now, we have some basic support for an on-disk cache, but quite a bit of engineering effort may be needed for coq-lsp to be able to use it effectively.

As a reference, a 18 MiB hash table can become 2.5 GiB if serialized naively without sharing.

Using `Marshall` for our Memo hash table does indeed work fine w.r.t. space, however the newly loaded hash table seems to be degenerate in some sense as the following happens:

  • once the cache is loaded, for some reason `Hashtbl.find_opt` takes ages, spending all its time in `compare`
  • moreover, for some reason the state is different, and we get a cache miss.

So a first step we would like to understand why we get a cache miss, likely due to some CEphemeron’s?

We get a cache miss even in the root state, so a first interesting try would be `-boot -noinit` and see if we have a miss.

Or even better, we could develop a state diff tool.

Coq DB and libobject

A big task is to rework libobject so we have more principled access.

There is a start of discussion in coq/coq#16261

Coq / Platform

Other misc todos:

  • parsing state: this is the most critical part to do in Coq, as of today, parsing at different points in Coq requires a very costly state reconstruction, which greatly increases latency.
  • common initialization code:

    A initial attempt was done in https://github.com/coq/coq/pulls/13418 following EJGA suggestions, but we want to merge with the other 3 copies that predate it, here, in SerAPI, and in jsCoq.

    Some more flexibility is needed.

  • Remove derive, improve API for multiple proof terms.

    See issue: coq/coq#10363

  • proof handling refactoring:

    See issue: coq/coq#10041

    This was greatly advanced but still work to do, and many possibilities

  • Improve typeclass hook onto pretyper ? That seems messy, not sure it is worth it.
  • refine the type of vernac interpretation. We want to make the general state more explicit, in particular for parsing-only commands, tactics, commands that alter the module structure.

    A nice idea here would be to give the vernac more structure

  • provide API for Coq SMT / CoqHammer and other tools to register processes with the document manager, there was a discussion in a Coq Hackathon about this.
  • OCaml multicore

Related and interesting libraries

  • lev + lev_fiber: prime candidate for us using it
  • let-def/lwd
  • what about Lwt? Does it work OK on Win?