Opt in to new type inference method

[Baltoli]

@Scott-Guest has implemented a new type inference algorithm that does not rely on Z3; using it should reduce CI flakiness during parsing by not requiring a lot of files to be opened and processes to be spawned.

At the moment, the new mode is opt-in and can be enabled by passing:

--type-inference-mode simplesub

as a flag to kompile.

[dkcumming]

@Scott-Guest @Baltoli Just trying to understand, so the new type inference algo is in K >= v6.1.42 and we should go ahead and make the change now? Or it is still in development? I ask because this is part of K Development project also I see.

[Baltoli]

It's merged to K now, yes. The new algorithm is ready for use in downstream semantics but requires a fallback to Z3 in a few limited cases - you should make the change now so that we can see that it's working properly in the wild. It's in the K development project so that we can keep an eye on how it's being rolled out.

[dkcumming]

Okay sound good, we will get on it.

[dkcumming]

CI seems the same. We only have miniature proofs at this point, so it isn't really getting a full work out.
Old Type Inference Algo
New Type Inference Algo