eval_expr creates auxiliary definitions in the VM. These auxiliary
definitions are gone after the VM finishes.
We store vm_obj's in the attribute_manager.
Before this commit, Lean was crashing in the following scenario:
1- A new caching_user_attribute is defined, and the user data structure
contains closures.
2- The closures are created using eval_expr.
3- When reusing the cached values, the system crashes when trying
to apply a closure created using eval_expr. The closure points to
an auxiliary definition that has already been deleted.
The new test exposes the problem. This is not a hypothetical scenario,
the new test is based on the Lean - Mathematica integration being
developed by @rlewis1988.
The fix consists in making sure we do not cache anything if
the VM environment has been updated by eval_expr.
I believe this is acceptable behavior. eval_expr is a very low level
tactic, and I don't see a good motivation for invoking it when
constructing the cache.
BTW, the test can be relaxed if the vm_attr does not contain closures.
However, it doesn't seem to pay off.
Another potential fix would be to propagate the definitions created
by eval_expr to the main environment. However, I think this is not
acceptable.
We will be flooding the main environment with useless temporary definitions
created by `eval_expr`.
This commit also stores the environment at caching time, and make
sure the cache is only reused if the current environment is a descendant
of the the one at caching time. This is fixing a different potential
bug.
This will minimize the size of the m_builtin_cases_vector.
It also indirectly prevents the crash decribed at 144d9096e2.
However, the fix used there is more robust.
We generate internal ids for builtin cases_on recursors.
These ids were being saved in the .olean files.
This was fine before commit 41e8a1712e because we had a separate
mapping for builtin cases_on recursors. Now, all ids are stored in the
same mapping. Thus, minor changes in the set of VM builtin operations
make lean crash when importing .olean files because they will change the
internal id for the builtin cases_on.
The problem can be reproduced in the following way:
0- Go to build/release
1- make clean-olean
2- make
Everything is fine after step 2
3- Comment the following line at tactic_state.cpp
DECLARE_VM_BUILTIN(name({"tactic", "open_namespaces"}), tactic_open_namespaces);
4- make
5- Lean will crash when executing the following command
../../bin/lean ../../library/init/meta/tactic.lean
I believe this bug is reponsible by the crash that @jroesch reported on Slack.
This commit fixes the problem by storing the name of the builtin
cases_on recursor in the .olean file.
@gebner, I have been experiencing crashes that are hard to reproduce.
I think one of the problems was that get_vm_name was returning a `name const &`.
I think this may produce a memory access violation in the following
scenario:
1- Thread 1 invokes get_vm_name, and gets a reference R. This is a
reference to a memory cell in the vector m_idx2name.
2- Thread 2 invokes get_vm_index, and it triggers a vector resize
operation. After the resize, reference R is invalid.
3- Thread 1 crashes trying to access R.
