Caching seems to work OK, when it works. Unfortunately there are 2 problems as of now:
Marshalleither: a) requires
Closuresor 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
Marshal.to_channel, however some functional value has leaked it seems :S
What 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
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 :/
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