Publish definition of verus! macro on crates.io
#1758
Closed
dschoepe
started this conversation in
Feature requests
Replies: 1 comment
-
|
I think we can mark this as complete at this point (modulo a bit more work to ensure regular updates). |
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Uh oh!
There was an error while loading. Please reload this page.
-
To allow verus-verified code to be used outside of verification contexts, it would be very useful to publish enough parts of
vstd,builtin, andbuiltin_macroson crates.io to enable regularcargo builds of verified crates, even if this does not run verification. An explicit dependency on the github repository would prevent crates using theverus!macro from existing on crates.io.While publishing verus in its entirety on
crates.iois challenging, it's hopefully a simpler problem to publish just the definition of theverus!macro.Beta Was this translation helpful? Give feedback.
All reactions