Interleave: do not interleave pragmas in IDE mode, just like batch#3909
Draft
mtzguido wants to merge 5 commits intoFStarLang:masterfrom
Draft
Interleave: do not interleave pragmas in IDE mode, just like batch#3909mtzguido wants to merge 5 commits intoFStarLang:masterfrom
mtzguido wants to merge 5 commits intoFStarLang:masterfrom
Conversation
We've long ignored the pragmas in an fsti when checking an fst (FStarLang#1142). This helps in preventing tons of confusion when checking an fst file, as otherwise the rlimit/fuel/ifuel can change under the user's feet as they check a file. However, in the IDE mode, when the pragma was near the top of the fsti (more specifically in the first chunk that would be interleaved) in the fst, this was still being interleaved. This is since when try to find the relevant decls to interleave from the fsti before the top-level `module Foo` decl, and that returns the empty set, so they remaing in the `remaining_iface_vals` which are still returned, but were unfiltered. This lead to a long headache just now while noticing a file failing in the IDE, but that had succeeded repeatedly in batch mode. Fix this by just filtering out all the pragmas before any kind of interleaving, which should be more robust.
Member
Author
|
This needed more tweaks, and does in fact cause a difference in batch mode, which we just hadn't noticed. Checking the fallout here: |
10 tasks
This avoids having a pragma in the interface. Also tidy up fuel usage/pragmas in these files.
Member
Author
|
I removed an unrelated patch about pow2 (now in #3910) and re-ran here https://github.com/mtzguido/FStar/actions/runs/16332110688 |
Merged
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
We've long ignored the pragmas in an fsti when checking an fst (#1142). This helps in preventing tons of confusion when checking an fst file, as otherwise the rlimit/fuel/ifuel can change under the user's feet as they check a file.
However, in the IDE mode, when the pragma was near the top of the fsti (more specifically in the first chunk that would be interleaved) in the fst, this was still being interleaved. This is since when try to find the relevant decls to interleave from the fsti before the top-level
module Foodecl, and that returns the empty set, so they remaing in theremaining_iface_valswhich are still returned, but were unfiltered.This lead to a long headache just now while noticing a file failing in the IDE, but that had succeeded repeatedly in batch mode.
Fix this by just filtering out all the pragmas before any kind of interleaving, which should be more robust.