The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

How hard would it be to write a Coq wrapper that performed memoization?  More precisely, I want a daemon that I can feed multiple file names over a period of time, and if a given file shares the first 90% of its lines with a previously given file, only the last 10% of the lines in the second file should need to be run.

I've thought about writing a python wrapper around `coqtop -emacs` and using `BackTo` to implement this, but I am curious if (a) such a tool already exists, or (b), it would be easy to write an alternative ocaml coq toplevel that did this memorization?

(The main use case for this would be my bug-minimizer, and it would also be useful on a group of files that spend a lot of time on initial imports, and all import the same libraries.)

Thanks,

Jason