Perform `fast_done` first in `naive_solver`.
This avoids naive_solver
tearing whole goals apart, even if the goal appears exactly as a hypothesis.
In Iris/C I ran into this problem after the recent set_solver
changes (4ff965b2). Since set_unfold
unfolds more stuff than it used to do, naive_solver
essentially had to solve P → P
. However, since it was tearing the entire goal apart, and trying to reestablish it while there were other assumptions in the context that influenced instantiation of existentials, it was not able to solve P
again. By performing fast_done
eagerly, it will not simply solve P → P
immediately without tearing the entire goal apart.
It appears that the impact on e.g. LambdaRust is in the noise range: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=master&var-commit1=4ad3f8b08c1ff4481d0fab41f878b215257a6462&var-config1=coq-8.9.0&var-branch2=ci%2Frobbert%2Fnaive_solver&var-commit2=11c5f900bf7b1f9fdaf4ba8cfc36d601bb5abdbf&var-config2=coq-8.9.0&var-group=().*&var-metric=instructions