The `--__no_positivity` option does not seem to work for interleaved modules in interactive mode

[mushrm88]

Due to #2840, for certain type definitions, I need to disable the positivity checker. I use the --__no_positivity flag for this. If I only have an .fst file, the option seems to work properly and I can edit the .fst file interactively. However, if I have both an .fst and an .fsti file, where the interface file has a type definition wrapped with the no positivity flag, then the interactive mode will error out when editing the .fst file even if I add the flag before the error.

Passing the flag to the command line works.

[mtzguido]

This is due to the fact that pragmas in the interface file are not interleaved into the implementation, hence the option gets lost. This issue has a bit of history, see https://github.com/FStarLang/FStar/issues/959#issuecomment-445906441, #1142, #1770.

Removing the pragmas was supposed to help, since them not being visible in the fst can cause mysterious failures, but breaks this example, and I don't think there's an easy way around it... Maybe we can revisit that choice, or start implementing one of the more robust variants of interfaces.

For this particular option we could instead turn it into an attribute, which should unblock this problem. I will try it.

[mtzguido]

For the record I couldn't repro the problem in emacs, but can repro in the command line with this module: A.fsti

module A

#push-options "--__no_positivity"
noeq
type t = | Mk of (t -> unit)
#pop-options

val x : int

A.fst:

module A

let x = 1

And, for the dangers of keeping interface pragmas, see this: B.fsti:

module B

#push-options "--lax"
val f : squash False
#pop-options

B.fst:

module B

let f = ()

One would expect the lax-checking of the signature of f to be meaningless, but if it leaks into the implementation file (say by reverting ac81813ec8bd8419bfa35b376cd1bdc6d68ff572 ), then we accept a proof of false.