Tracking performance issues in the build of miTLS

[msprotz]

(before this disappears in the archives of slack)

summary of a performance discussion we had with @fournet yesterday...

• generation of .krml files is quadratic because we don't cache the results of F* extraction internally; we used to do it but no longer do (see Unnecessary casts inserted in KreMLin AST when using --cmi FStarLang/FStar#1596); we suspect that introducing .extracted files would be a big performance win, since parsers, which are notoriously inline_for_extraction-heavy, wouldn't require a quadratic amount of work
  action item: feature work in F* to add support for these files- interactive mode seems to have issues of its own: loading, say, Negotiation.fsti in emacs takes much longer than verifying it in batch mode; could there be too many protocol messages exchanged that slow things down? (I see a ton of messages about loading dependencies) who would be an emacs expert to look into this?
  action item: investigate emacs-mode- loading .checked files takes a while (for Negotiation.fsti on my super high-end machine: that's 20s in batch mode for loading things up, followed by 3s of actual verification time)
• Tom Kelly from Cambridge Labs identified an inefficiency where a new z3 process is created for each .checked file being loaded, but with his patch I don't see a noticeable performance improvement on batch-mode Negotiation.fsti -- maybe Cédric will see an improvement, since his machine seemed to be exhibiting over 1minute of just loading checked files? unclear
  action item: review and approve Z3 background process refresh optim FStarLang/FStar#1781 -- it can't hurt
• we seem to be loading parsing data for the entire dependency graph of each file for the purposes of cycle detection (hence, the warning about name resolution in HACL which, frankly, we should just fix); loading parsed files is costly; can we have a --unsafe_no_cycle flag to be used only in situations where a Makefile runs fstar --dep (which does cycle detection), so that we can skip cycle detection for individual files?
  action item: add a new flag to skip cycle detection; maybe this would remove the memory overhead of only loading .checked files once?- the noextract keyword still runs internal extraction code, it just replaces the body of the definition with failwith
  action item: an expert (Tahina) could comment on whether skipping extraction altogether of such definitions (assuming there's enough type information in the context to do so) would translate into big performance improvements for the extraction of parsers