--eager_inference flag should be disabled

FStarLang / FStar

A Proof-oriented Programming Language

https://fstar-lang.org

Apache License 2.0

2.7k stars 234 forks source link

--eager_inference flag should be disabled #444

Closed catalin-hritcu closed 5 years ago

catalin-hritcu commented 8 years ago

According to Nik's comment on https://github.com/FStarLang/FStar/issues/424#issuecomment-150864813 --eager_inference flag should be disabled. "It's extremely non-standard and was there to support a transition from the old inference algorithm to the current one."

s-zanella commented 8 years ago

Is the --eager_inference flag hard to maintain? It was useful at debugging in the past, so why not just keep it.

nikswamy commented 8 years ago

It will be yet another configuration of the type-checker to test. I don't think our regression suite uses it at all. So, I worry that counting on it going forward will lead to unpredictability.

If you really want to keep it, I don't mind. Let's document it as "experimental" or "brittle" or something like that.