Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Some assorted fixes #2839

Merged
merged 20 commits into from
Mar 7, 2023
Merged

Some assorted fixes #2839

merged 20 commits into from
Mar 7, 2023

Conversation

mtzguido
Copy link
Member

  • Fix a couple typing errors in the compiler not caught by lax-checking (a value of type ident accepted to be term, and similarly for lbname and lident).
  • Add a new qualifier to ident and lident to prevent this error, as they are hidden by an interface. Should do for more types too?
  • Show warning immediately when --debug, do not collect them.
  • Antiquotations now work in binders and patterns
  • Improving an error for loading plugins. I will soon send a PR for building plugins when --codegen is passed, instead of trying to do so at --load time (which can be a race in a build system, and HACL* has some logic to avoid it).

mtzguido added 20 commits March 7, 2023 07:13
@mtzguido
tosyntax: cid.range -> range_of_id cid
a0c7353 
The .range field is actually for terms, so this is a type error, but not
caught as we are only lax-checking and F* is dropping a guard requiring
`ident == term`.

cc @W95Psp
@mtzguido
ident: mark ident and lident as new to prevent some errors
45ac3bd 
See previous commit.
@mtzguido
syntax/util: remove duplicated range_of_lbname
5b15a85
@mtzguido
extraction: fixing another type error, ident vs lbname
84f7ed4
@mtzguido
.gitattributes: tidy for new dune build
bdd8099
@mtzguido
errors: show warnings and errors immediately when debugging is on
34638d2
@mtzguido
tosyntax: antiquotations in binder and pattern types
699e81a
@mtzguido
tactics: a more helpful error when loading fails
faafb5f 
No need to `failwith`, and we can also add a way to ignore the error
and continue without loading the plugin file.
@mtzguido
examples: param: update
ab5d7c2
@mtzguido
errors: add an interface
f3d9d22
@mtzguido
Compiler.List: nit
ab14f4e
@mtzguido
Makefile: tweak shortcuts
35395fe
@mtzguido
tactics: check for internal qualifiers when splicing
6e891d0 
We cannot allow tactics to just set any qualifier. While some of them
will cause the typechecker to fail, in others it will just silently
accept them since it trusts the parser to not generate odd combinations,
such as `Effect` on a top-level value definition.

So, just raise an error if any internal qualifier appears in the
generated sigelt.
@mtzguido
expose InternalAssumption
cedd874
@mtzguido
reflection: fix embedding for some qualifiers
d5df326 
They are not curried, their payloads are pairs
@mtzguido
tc: inductive: consider noeq to also clash with eqtype annotation
2d38009 
Fixes #2809
@mtzguido
bug-reports: mark #2809 fixed
2fee8de
@mtzguido
update error messages
8395de3
@mtzguido
tactics: wire ghost_uvar_env to the normalizer
dccc12f 
Otherwise this will not run for interpreted tactics, only for native
ones.
@mtzguido
snap
33992de
@mtzguido
Copy link
Member Author

mtzguido commented Mar 7, 2023

Added:

  • An interface for the errors module
  • Forbid using internal qualifiers when splicing (for this I also reordered the qual list in the Syntax module to respect a comment, and hence bumped the checked file version number)
  • Fix some embeddings
  • Fix 2089

@mtzguido mtzguido merged commit 9594e8f into master Mar 7, 2023
@mtzguido mtzguido deleted the guido_misc branch March 7, 2023 16:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@mtzguido