Dwight Guth

@arximboldi any update on this?

Sure, I'm in no rush to get these merged as I already have a working version in our fork of the repository that will suffice for the time being. I...

@arximboldi I originally thought I could modify the PR to take advantage of the template parameter introduced in #190 in order to only expose a reference to these objects if...

btw, as I commented on the other PR, it seems that your SSH key issue is not completely resolved yet.

Unfortunately it's unlikely that I'll have a chance to flesh this out the rest of the way anytime soon because the main thing that is left is to make this...

Documentation is still very much a work in progress. There is some slightly outdated "documentation by example" found here: https://github.com/kframework/k/tree/master/k-distribution/tutorial And some up-to-date but incomplete documentation here: https://github.com/kframework/k/blob/master/pending-documentation.md But nothing...

Pretty sure this never actually made it off the java backend. So there's a lot of maintenance to do here before you could reasonably use it with modern K. It's...

To summarize, basically all three floating types are represented internally by 64-bit floats. What we need is: 1. configuration settings for the mantissa and exponent size of each of the...

I believe the Java backend has the hook `#BOOL:checksat_`, but note that it was never tested with K4 and I can't guarantee it will work. SMT functionality was built into...

I think the simplest thing to do is just emit the error message and not the stack trace. Is anyone really gaining any information from those stack traces?