Stream: coq-lsp

Topic: Caching


view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 01:21):

Caching seems to work OK, when it works. Unfortunately there are 2 problems as of now:

view this post on Zulip Rudi Grinberg (Jul 04 2022 at 01:27):

What data are you caching?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 03:49):

As of now I'm caching the document processing action, that is to say, the action coq_state * coq_ast -> coq_state * result

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 03:49):

the actual type is this one

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 03:50):

https://github.com/coq/coq/blob/d6724a90188d6f151362a02bde9c385191e02013/vernac/vernacstate.ml#L92

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 03:50):

I've fixed AST equality and now the system seems to work pretty well

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 03:50):

!

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 03:50):

but no writing to disk yet

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 03:50):

Coq AST is quite something :/

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 03:51):

see https://github.com/ejgallego/coq-lsp/blob/main/controller/memo.ml#L44

view this post on Zulip Enrico Tassi (Jul 04 2022 at 05:57):

Do you realize that .vio files are just the marshaling of the coq state just before every proof?


Last updated: Feb 06 2023 at 07:03 UTC