The Coq mailing list

[Jacek Chrząszcz <chrzaszcz AT mimuw.edu.pl>]

There are -inputstate and -outputstate options to coqtop, they could
be useful...

Bests

Jacek

2015-03-24 0:36 GMT+01:00 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