In the interactive mode, flycheck queries are run with lax=true in the environment, which causes SMT queries to be dropped. This in turn will "confuse" the Pulse checker whenever we are doing flychecking, and report spurious errors such as FStarLang/Pulse#122.
This is a bigger problem with confusion between --admit_smt_queries true, --lax, and the env.lax and env.admit fields. I'm wrapping up a PR about that.
Meanwhile, just make all entries into a splice_t tactic run with admit=false and lax=false.
Another thing we should do is simply not flycheck syntax extension blobs. Emacs' fstar-mode does this already, but apparently not the VS code extension. We have an internal environment flag flychecking:bool for this purpose, but it's not set from VS code queries apparently.
In the interactive mode, flycheck queries are run with
lax=truein the environment, which causes SMT queries to be dropped. This in turn will "confuse" the Pulse checker whenever we are doing flychecking, and report spurious errors such as FStarLang/Pulse#122.This is a bigger problem with confusion between
--admit_smt_queries true,--lax, and theenv.laxandenv.admitfields. I'm wrapping up a PR about that.Meanwhile, just make all entries into a
splice_ttactic run with admit=false and lax=false.Another thing we should do is simply not flycheck syntax extension blobs. Emacs' fstar-mode does this already, but apparently not the VS code extension. We have an internal environment flag
flychecking:boolfor this purpose, but it's not set from VS code queries apparently.