Hello,
I’m new to this community site.
I hope I’m posting this in the right place, so would you be kind to warn me if I’m not?
I have written a function using Program Fixpoint that is consuming too
much memory to check. This happens while checking the function itself, even before
the proof obligations. When I ask Coq to check the function, the Coq process consumes
all my computer’s memory and the OOM Killer kills Coq’s process before it finishes.
What are the possibles reasons that may be causing this issue?
This is happening in the middle of big project of mine and I couldn’t reproduce it in
a small scenario.
I’d first ensure your swap space is setup correctly; otherwise you might get OOM much too soon.
How big is this function, and how many constructors are there in the datatypes you match on? I’m assuming those numbers are relatively large, but would be good to know.
Then, I’d check if using “Unset Program Cases.” before the function makes a difference; it should reduce the size of the output function. With the default settings, the size of Program’s output can be much bigger (I forget the details, but iirc it becomes quadratic). That flag disables features that are sometimes useful, but they’re also expensition
If that fails, I’d also try disabling parta of the funcrion to see if coq is just using lots of ram, or if it’s actually allocating memory in an infinite loop
I’d also try to split this function into smaller ones, limit matches on multiple expressions at once, etc.
I believe that my swap space configuration is good, because Coq’s process eats all my 16 GB of ram when I check this function.
The “Unset Program Cases” solved the problem. It still is a bit slow to check, but at least the process finishes without eating all my ram.
I’m working on the certification of algorithm W and I think this issue may be caused by the monad that I’m using in my definitions. This monad uses a few pattern matchings in its bind operator, in particular in its type. So a function with a lot of binds has a lot of implicit (possible nested) pattern matchings. Could this be the cause?
Since I already talked about my project, maybe I should link it here.
The issue was in this branch , while checking the W function on file Infer.v. Now with “Unset Program Cases” the function checks.
Coq doesn’t inline definition bodies when typechecking, except as needed to compare types; so I’d expect that the pattern matches inside the methods of your monad shouldn’t matter. However, the matches in HoareState and in Infer's argument could be a problem; I’d honestly try moving them in separate definitions, written without Program or by disabling Program Cases. Right now, your bind is still defined with Program, and the type of bind might slow down typechecking quite a bit.
To debug which, you can get the effects of Unset Program Case for a specific match, replacing match foo with with match foo return _ with.
1 Like
FWIW, this was incorrect; termination checking can inline definitions, as needed to check how recursive calls are used. For instance, if f is recursive and passes f itself as an argument to g, then g will be inlined.