We've been using this library for a few years at issuu, and we've run into several stack-overflow crashes on large inputs because of calls into non-tail-recursive list functions in either the Coq or OCaml standard library. We are currently maintaining our own fork with fixes to these issues, and we would like to merge those fixes upstream.
I recommend viewing the commits individually. The first commit has no semantic changes but simply updates the auto-generated code to Coq 8.4pl6, which is the version I have installed. This makes sure the subsequent changes to the Coq code produce a clean diff.
I added Extract Constant declarations to the Coq code to replace Coq standard library functions with custom tail-recursive ones. It would of course be better to implement the tail-recursive versions in Coq and prove them equivalent to the standard library versions, but I hope you'll agree that adding a bit more unverified code is better than keeping the code that is verified but crashes on large inputs.
mzp
commented
8 years ago
We've been using this library for a few years at issuu, and we've run into several stack-overflow crashes on large inputs because of calls into non-tail-recursive list functions in either the Coq or OCaml standard library. We are currently maintaining our own fork with fixes to these issues, and we would like to merge those fixes upstream. I recommend viewing the commits individually. The first commit has no semantic changes but simply updates the auto-generated code to Coq 8.4pl6, which is the version I have installed. This makes sure the subsequent changes to the Coq code produce a clean diff. I added
Extract Constantdeclarations to the Coq code to replace Coq standard library functions with custom tail-recursive ones. It would of course be better to implement the tail-recursive versions in Coq and prove them equivalent to the standard library versions, but I hope you'll agree that adding a bit more unverified code is better than keeping the code that is verified but crashes on large inputs.