Skip to content

Perform `fast_done` first in `naive_solver`.

Robbert Krebbers requested to merge ci/robbert/naive_solver into master

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

Edited by Robbert Krebbers

Merge request reports