fn generate_checking_file(genv: GlobalEnv<'_, '_>, def_id: DefId) -> Result<()>Expand description
Generates the file that checks that the proof has the type of the VC. The #print axioms is
used to reject proofs that (transitively) depend on sorryAx, see ProofReport::status. The file is
regenerated even when the VC is cached, so that it is always up to date.