Zoncolan and SPARTA both use abstract interpretation at their core, but as far as the code/implementation goes they are mostly unrelated. Zoncolan is built on top of the Hack type checker (https://hacklang.org/), which means that it's largely written in OCaml.
You can run Pyre without using watchman if your editor-of-choice supports LSP -- the two modes are basically complementary. You can also run `pyre check` in non-incremental mode, though that may be slower depending on the size of your codebase.
So you're saying the LSP portion checks the file(s) you're currently editing, whereas the watchman (also incremental) check or the non-incremental check do the whole project?
Edit: for the active file / LSP part, I mean it shows errors mainly for the active file.
Exactly - the LSP portion of pyre works for files you have open in an editor, but might miss changes due to a rebase or files you edit on the terminal. The watchman integration is there to make sure that pyre's aware of changes outside your editor.
Edit: pyre will show type errors for all files in your repository, not just the ones you have open.
Ah, that's nice. So you can change the type of a function in one file that you are editing, and pyre will show you all the other places that are now using the wrong types.
Good question [I am the 'Pieter' on that blog post]. There will be a talk at PyCon that covers parts of this. It comes down to two reasons:
1) Performance. We needed something that would consistently work quickly on Instagram's server codebase (currently at several million lines).
2) We are building deeper semantic static analysis tools on top of Pyre. We've built some of these tools for Hack/PHP already, so following the Hack type checker's architecture is the best way for us to achieve this.
> 1) Performance. We needed something that would consistently work quickly on Instagram's server codebase (currently at several million lines).
That's not really an answer to why you didn't work on mypy, at least to an outsider to the decision making process. Are you saying that you discovered it's just not possible to scale mypy (or at least not without extensive work / more work than building your own solution?)
I think (2) is the overriding concern: we're getting really great results with the static analysis tools we've built internally on top of the Hack type checker. Building a similar tool on top of mypy would've required fairly invasive changes; we decided to use the Hack type checker infra instead.
Full disclosure: I worked on the Hack type checker briefly, a long time ago :)
