Request: very basic file I/O about libraries HOT 5 CLOSED

FWIW, I'd be a bit nervous about undertaking this at at moment when everyone seems to agree that extern is currently somewhat broken (e.g., dafny-lang/dafny#2397, dafny-lang/dafny#469, dafny-lang/dafny#313, dafny-lang/dafny#2291), but we haven't yet converged on a new approach. You may be bolder than I am, however :)

from libraries.

Not sure where to ask this, but I guess here it's on point.
I see that the file I/O implementations were merged in but with Go "out of scope" because of bugs in fundamental aspects of translation of Dafny to Go.
Those bugs seem pretty related to a bunch of others that I have reported myself.

My team is considering moving forward with a Go translation of Dafny code, and for now I've been finding my own workarounds for those bugs. But this "out of scope" makes it sound like maybe this isn't a good idea after all. Would it be possible to get some clarity on what is the status of Go support? For example, any timeline regarding when would a Go file I/O implementation be added?

Please let me know if this question makes more sense elsewhere.

from libraries.

Hi @hmijail, thanks for reaching out. We intend to support the Go compiler at the same level as the others. We don't have a concrete timeline for adding a Golang file I/O implementation, but for now you can track this work here: #79

I would say that of the two blocking issues I linked in #60 (comment), only the former (dafny-lang/dafny#2989) is a fundamental issue in the Go compiler, and fixing this kind of bug is indeed a priority for us. It's one we intend to fix as we work on improving the interoperability between compiled Dafny code and code written in target languages.

The latter issue (dafny-lang/dafny#2045) is easily worked around if you're only compiling to Go. That workaround was insufficient for this PR only because we needed a single Dafny {:extern} declaration that works "the same" across all languages, and Golang is an odd one out. Again, we expect to improve or eliminate this edge case as we improve Dafny interoperability.

from libraries.

@parno:

FWIW, I'd be a bit nervous about undertaking this at at moment when everyone seems to agree that extern is currently somewhat broken (e.g., dafny-lang/dafny#2397, dafny-lang/dafny#469, dafny-lang/dafny#313, dafny-lang/dafny#2291), but we haven't yet converged on a new approach. You may be bolder than I am, however :)

Absolutely a fair point. We're relying on the fact that the implementation of the file I/O is well encapsulated, so if and when we have something that works better than {:extern} currently does, we can move to it without breaking any consumers.

from libraries.

The latter issue (dafny-lang/dafny#2045) is easily dafny-lang/dafny#2045 (comment) if you're only compiling to Go.

That's not a problem I have found myself yet, but I'll keep it in mind just in case :). Though we do hope to keep multiple target languages, so it's not ideal.

from libraries.