Caching seems to work OK, when it works. Unfortunately there are 2 problems as of now:
Marshall
either: a) requires Closures
or b) when using Closures
, the read back doesn't work with a funny error message (looks like a bug in OCaml?) Would be great if we didn't require to use Closures
in Marshal.to_channel
, however some functional value has leaked it seems :SWhat data are you caching?
As of now I'm caching the document processing action, that is to say, the action coq_state * coq_ast -> coq_state * result
the actual type is this one
https://github.com/coq/coq/blob/d6724a90188d6f151362a02bde9c385191e02013/vernac/vernacstate.ml#L92
I've fixed AST equality and now the system seems to work pretty well
!
but no writing to disk yet
Coq AST is quite something :/
see https://github.com/ejgallego/coq-lsp/blob/main/controller/memo.ml#L44
Do you realize that .vio files are just the marshaling of the coq state just before every proof?
Last updated: Mar 28 2024 at 23:01 UTC