See #1405
Memory consumption is still high, but I didn't manage to cross the 2Gb
limit anymore with this commit even after hundreds of modifications.
@gebner I'm not seeing a big difference betwee Lean without memory_pool,
with bounded memory_pool and unbounded memory_pool. We may even consider
removing it in the future after a more careful benchmarking.
In the benchmark (https://gist.github.com/leodemoura/b27fb4203a13a67274b388a602149303),
I'm getting the following numbers:
- No memory_pool: runtimes between 3.532s - 3.556s
- With memory_pool bounded by 8192: runtimes between 3.32s - 3.44s
- With memory_pool (with no limit): runtimes between 3.32s - 3.44s
On the other hand, the small object allocator makes a big difference.
I used your list_rev.lean example.
- with: 2.62s
- without: 3.75s
closes#1134
see #1362
This feature is implemented using a "hearbeat" thread local counter.
We reset the counter whenever we start a new task.
The counter is incremented when:
1- An object is allocated using small_object_allocator (e.g., VM object)
2- An object is allocated using memory_pool (e.g., expr, level, rb_tree nodes, list cons-cells, etc)
3- check_system(...) invocations
We check if the threshold was reached at check_system.
The option --timeout=num can be used to set the limit (in thousands).
The default is unbounded in batch mode.
In server mode, the default is 100000. We can compile the standard library with --timeout=12000
I did not perform many experiments to check how precise this counter is.
I added a new Emacs configuration setting to change the server default.
Here is the wall clock time for different values of --timeout for the
command used on issue #1134
time ../../bin/lean -j 0 --timeout=20000 loop.lean
loop.lean:1:0: error: (deterministic) timeout detected at 'expression equality test' (potential solution: increase timeout threshold)
real 0m1.070s
user 0m1.032s
sys 0m0.036s
time ../../bin/lean -j 0 --timeout=40000 loop.lean
loop.lean:1:0: error: (deterministic) timeout detected at 'expression equality test' (potential solution: increase timeout threshold)
real 0m1.777s
user 0m1.676s
sys 0m0.044s
time ../../bin/lean -j 0 --timeout=50000 loop.lean
loop.lean:1:0: error: (deterministic) timeout detected at 'expression equality test' (potential solution: increase timeout threshold)
real 0m1.985s
user 0m1.920s
sys 0m0.056s
time ../../bin/lean -j 0 --timeout=100000 loop.lean
loop.lean:1:0: error: (deterministic) timeout detected at 'expression equality test' (potential solution: increase timeout threshold)
real 0m3.587s
user 0m3.564s
sys 0m0.020s
