[pull] master from FStarLang:master #343
Open
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
![pull[bot]](https://avatars.githubusercontent.com/in/12910?s=60&v=4){kind=small}
Error message tweaks
If lib/fstar/ulib already exists, we will ulib into it, instead of overwriting it. Just remove it beforehand. We should own $(PREFIX)/lib/fstar.
Makefile/package fixes
Some fixes in support of Pulse errors
Result of `make bump-stage0`
Bump version number
Some refactoring, and tidying up libraries during build
Normalizer: making delta attributes compose
test.mk: Make sure to be silent on error output tests
Tactics: return proper errors when guards fail for typing reflection
Tc: unconditionally restore options before encoding a module
Add missing apt-get update
Simplify `reveal ?u =?= reveal t` to `?u =?= hide (reveal t)`.
Parser: allow operators in restricted opens
This makes jump-to-definition work for spliced definitions, including typeclass methods and Pulse functions.
Tc: proper ranges for spliced definitions
Prims.ml: remove mentions of lex_t/LexNil/LexCons
This can be very slow, since if we are loading 100 checked files we will incur in 100 restarts of Z3 including fact filtering.
Tc: no need to refresh the solver when loading from cache
Tc: tweak error range for wrong universe instatiation
INSTALL.md: fix location of get_fstar_z3.sh
… you to lax check a block and then full check it easily)
…d_changes Revert a block and recheck it, if the push kind changes (i.e., allows…
Useful to debug parsing failures, since it's not obvious what the tokens involved even were.
The MINUS token is distinguished and not included in the binary operators, handle it specially.
Parser: fix parsing of (-)
Used from Pulse
Parser: mark lidentOrOperator as public
Tactics.NamedView: guaranteeing that pack does not change top-level ctor
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.
See Commits and Changes for more details.
Created by
pull[bot]
Can you help keep this open source service alive? 💖 Please sponsor : )