Best practices for troubleshooting F* proofs

[klinvill]

Tacking onto #2546, are there any best practices for troubleshooting F* proofs (especially with what z3 is doing)? For that question, I generated the queries that are sent to z3 (--log_queries) but it resulted in smt2 files with ~150,000 lines. Is there a better way to troubleshoot and see what's happening under the hood without needing to parse through these large files?

[nikswamy]

Looking through F*'s SMT output requires a lot of knowledge about the internals of F*. I would hope that a typical user doesn't have to wade through that encoding .... but it can be useful to profile Z3 to see why proofs are going slow.

Here's one resource:
https://github.com/FStarLang/FStar/wiki/Profiling-Z3-queries

This sliding admit style here is also useful way to debug proofs incrementally, while staying within F* rather than going to Z3:
https://github.com/FStarLang/FStar/wiki/Sliding-admit-verification-style