Working with files with huge verification times - FStarLang/FStar GitHub Wiki

  • Use hints (see Hints (or how to replay verification in milliseconds instead of minutes)). Hints are compatible with interactive-mode.

  • Use C-c C-l instead of C-c C-RET to advance to the current point in --lax mode.

  • Use #set-options "--lax" and #reset-options for the part of the file that verifies already. That is:

  • Pass --admit_except <id> with a query id (eg, '(FStar.Fin.pigeonhole, 1)') to re-run a single SMT query and admit the rest.

module TLS

#set-options "--lax"
// a bunch of definitions that verify already
#reset-options

let f = ...
  // the function that you're currently trying to get to verify
  • Use another module
module TLS.Wip

open TLS

let f = ...
  // work here on the function that you're trying to verify so that you can focus on this function only