verus-lang / verus-analyzer

A Verus compiler front-end for IDEs (derived from rust-analyzer)
Apache License 2.0
8 stars 4 forks source link

Automatically import vstd and builtin #9

Open chanheec opened 1 year ago

chanheec commented 1 year ago

This PR is to automatically import Verus' vstd(verified std) and builtin without the user's guide.

Currently Verus uses "pervasive" which will be replaced by "vstd", and we have the user to generated a symlink to the pervasive in the project's "src" directory. This was because "pervasive" was a module rather than a crate. As vstd becomes a separate crate, this PR changes verus-analyzer to index vstd crate when it index std crate in the startup.

achreto commented 2 months ago

Would it make sense to apply those commits to #27 ? I did a rebase to the most recent rust-analyzer there (or well as of June 25) -- or are those commits already in there?

chanheec commented 2 months ago

These changes are incomplete, so I don't think we want to merge these into the latest rebase now. (These commits are not in the current main branch.)