search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Make 241 fatal by default #1652

Closed msprotz closed 5 years ago

msprotz commented 5 years ago

It's only after my laptop had been whizzing for an unusually long amount of time that I looked at my terminal to see what was up with my F* build.

FStar.Tactics.Logic.fst(0,0-0,0): (Warning 241) Stale, because inconsistent cache version cache file FStar.Tactics.Logic.fst.checked; will recheck FStar.Tactics.Logic.fst and all subsequent files

only then did I realize that I should've run git clean -fdx.

I'm suggesting on Slack a new CI job to catch these incrementality breakages, but in the meanwhile, is there any good reason for not making 241 fatal? To me, it's almost always the sign that something is wrong with your setup and that you need to git clean -fdx the universe.

Thanks,

Jonathan

msprotz commented 5 years ago

(Note that this would entail not issuing 241 when the stale cache file is the one we're about to regenerate.)

aseemr commented 5 years ago

We can make this one and the warning "A.fst.checked was not written because some of its dependences were also not checked" as errors only when --cache_checked_modules is on. In general making these errors by default could become painful during development. On the other hand, we don't usually have --cache_checked_modules on in our emacs setting(?).

msprotz commented 5 years ago

Yes, good point -- I should've mentioned that this only makes sense when --cache_checked_modules is on.

aseemr commented 5 years ago

In our last discussion about this, we decided not to make it an error and keep the behavior as is. Closing the issue, please reopen if we should discuss it more.