Introducing FStar.Prelude, removing special casing for Prims/Pervasives internally #3732
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mtzguido
force-pushed
the
prelude
branch
2 times, most recently
from
2376690 to
2fe9c73
Compare
…ther special handling
…ded are not considered for autocomplete
mtzguido
force-pushed
the
prelude
branch
2 times, most recently
from
7b86ba2 to
aba3abb
Compare
…for this type Needed to mark norm as noextract, which makes sense!
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR changes the behavior of F* to automatically open the module
FStar.Preludein every file, instead of Prims and Pervasives. (We also open theFStarnamespace, that is retained.)The main improvement is that there is no special list of core modules that do not incur default dependencies, and instead we can mark a module with the
[@@"no_prelude"]attribute to indicate it should not open the prelude. This in turn allows to edit these base modules much more easily. The last two patches here move some of the bulk of Pervasives into separate modules, which makes it easier to read them. These modules are included in the prelude too, so then most users do not "notice".In particular this allowed me to easily break a dependency problem with the norm_steps in the compiler referring to Pervasives.norm_step (of the parent compiler) which was definitely wrong.
Note this also means there's nothing special about Prims anymore either.