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.
The fix was incorrect because it could produce an invalid local context.
Actually, the regression tests/lean/run/1258.lean was producing an
assertion violation.
Global variables must be simple types. Reason: the finalization of
global objects in different compilation units is not specified by the
standard. The only exception is the global at src/shared/init.cpp.
It is used to automatically initialize the lean shared library.
Before this commit, attribute_manager used a std::unique_ptr in a global
variable. The test shared_test was crashing in one of my machines
because a different finalization order was being used.
@avigad I decided to fallback into first-order unification to address
the (a ∉ []) issue.
@dselsam Have you experienced similar problems in the ICML project?
The new comment at type_context.cpp explains the problem and hack to
workaround it. The issue is yet another instance where using "first-order
unification" produces imprecision, but generates the solution we want.
