Use `eauto` as default for `set_solver`.

The set_solver tactic roughly calls set_unfold and then performs naive_solver. @jihgfee noticed that set_solver (without tactic argument) calls naive_solver idtac by default. This is somewhat strange since naive_solver (without tactic argument) defaults to naive_solver eauto.

Also @jihgfee found an example where set_solver by idtac (the current default) is much slower than set_solver by eauto.

So I am wondering what's the reason why set_solver uses idtac? Is that just some arbitrary legacy choice, or does it actually improve performance?

@jung Could you run timing with this MR on the reverse dependencies so we can figure this out?

Currently we only have timing measurement infrastructure for Iris changes, not std++ changes... I'll need to think about whether I can hack something together here.

In case that's too tricky:

I could make the default solver of set_solver overridable. Such a change is backwards compatible, so we can merge it here. Then I can make an Iris MR to change the override, and you can run timing with that.

I think the best way to do this is to have an Iris branch that has its opam file updated to point to the new std++. Then we can time that Iris branch against master.

So either we release an std++ version with this 'by hand', or we just merge this to get an opam release.

I set up a magic branch ci-release... can you try pushing this branch there? That should trigger an opam package to be generated.

Never mind, I'll try the ci-release thing.

Timing results will appear at:

• examples
• lambda-rust
• iron

Looks pretty good, I would say.

Thank you @jung for setting this up.

The results indeed look good.

@jihgfee Could you minimize the example that takes 0 sec with the eauto version and a minute with the idtac version? We could add that one to the test suite.

@jihgfee ping, is it possible to have a minimized example?

added 8 commits

• 44b93de4...c25b43ed - 6 commits from branch master
• b37cd70f - Use `eauto` as default for `set_solver`.
• 9091657c - CHANGELOG.

Compare with previous version

Going to merge this one. If we can get a mininized example where the idtac version is slower later, that would be nice, but not needed.

enabled an automatic merge when the pipeline for 9091657c succeeds

merged

mentioned in commit 3a32d06d

mentioned in merge request !457 (merged)

mentioned in issue #179 (closed)