"foo() -> !" means something different in fns than in proto! #3295
Labels
A-concurrency
Area: Concurrency
A-frontend
Area: Compiler frontend (errors, parsing and HIR)
A-grammar
Area: The grammar of Rust
A-syntaxext
Area: Syntax extensions
Comments
|
non-critical for 0.6, de-milestoning |
|
Nominating for milestone 2, backwards-compatible |
|
are we keeping proto!? I thought the pipes compiler was going away entirely. |
|
Are we? I thought we hadn't decided, but I'd be happy to hear that we did decide so I can close this :-) |
|
I hope it stays! |
|
related: #3658 |
|
just a bug, removing milestone/nomination. |
|
seems like a compatibility issue to me? the syntax of the proto! macro would be changing, although i suppose maybe that doesn't count as language syntax. |
bors
added a commit
that referenced
this issue
Aug 1, 2013
The pipes compiler produced data types that encoded efficient and safe bounded message passing protocols between two endpoints. It was also capable of producing unbounded protocols. It was useful research but was arguably done before its proper time. I am removing it for the following reasons: * In practice we used it only for producing the `oneshot` protcol and the unbounded `stream` protocol and all communication in Rust use those. * The interface between the proto! macro and the standard library has a large surface area and was difficult to maintain through language and library changes. * It is now written in an old dialect of Rust and generates code which would likely be considered non-idiomatic. * Both the compiler and the runtime are difficult to understand, and likewise the relationship between the generated code and the library is hard to understand. Debugging is difficult. * The new scheduler implements `stream` and `oneshot` by hand in a way that will be significantly easier to maintain. This shouldn't be taken as an indication that 'channel protocols' for Rust are not worth pursuing again in the future. Concerned parties may include: @graydon, @pcwalton, @eholk, @bblum The most likely candidates for closing are #7666, #3018, #3020, #7021, #7667, #7303, #3658, #3295.
RalfJung
pushed a commit
to RalfJung/rust
that referenced
this issue
Feb 17, 2024
add tests for imported_main
jaisnan
pushed a commit
to jaisnan/rust-dev
that referenced
this issue
Jul 29, 2024
Using the `__CPROVER_object_upto` function to pass modifies clauses to asserts clauses in goto for rust slices. Resolves rust-lang#2908 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Matias Scharager <mscharag@amazon.com> Co-authored-by: Celina G. Val <celinval@amazon.com> Co-authored-by: Felipe R. Monteiro <felisous@amazon.com>
jaisnan
pushed a commit
to jaisnan/rust-dev
that referenced
this issue
Jul 29, 2024
- Add Arbitrary for array - Add Arbitrary for tuples - Add missing changes from modifies slices (rust-lang#3295) Note that for adding `any_array` I had to cleanup the unnecessary usage of constant parameters from `kani::any_raw`.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
In functions,
-> !indicates the function returns bottom, i.e., doesn't return. In pipe protocol definitions,-> !means "terminate the session", which is analogous to returning unit (the 1 type), not bottom (the 0 type).It seems more conceptually in-line to write session-end transitions with no arrow, like
... { continue(T) -> state2, close(U) } ...The text was updated successfully, but these errors were encountered: