ocaml-gospel / gospel

A tool-agnostic formal specification language for OCaml.
https://ocaml-gospel.github.io/gospel
MIT License
126 stars 16 forks source link

Improve performance and clean up the preprocessor #353

Closed shym closed 11 months ago

shym commented 11 months ago

This PR reworks the preprocessor by:

In a bit more details, the performance gains are obtained by changing the interface of the preprocessor so that it outputs its result into a formatter rather than a string and propagating the change all the way down, so that:

Using the example mentioned in #336 (test run in CI, so the performance may vary depending on load...), we go from:

16
allocated_words: 440218559
real    0m1.814s

32
allocated_words: 1749282355
real    0m10.295s

48
allocated_words: 3768016163
real    0m16.260s

to:

16
allocated_words: 2152756
real    0m0.019s

32
allocated_words: 4253492
real    0m0.031s

48
allocated_words: 6354228
real    0m0.044s
shym commented 11 months ago

Testing on larger inputs seem to show that the preprocessor is handling about 14MB/s. (For comparison, the largest mli in the compiler code base is 76KB). So this is probably good enough for now to say: Closes #336.

shym commented 11 months ago

Closes #342

shym commented 11 months ago

Updated so that all print_X functions (not print itself, though, which is using) take ppf as their last argument. And rebased.