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.

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

Warning for shadowing format needs to be more like warning for emacs #3492

Open
briangmilnes opened this issue Sep 22, 2024 · 1 comment
Open

Comments

@briangmilnes
Copy link
Contributor

  • Warning 274:
  • Implicitly opening namespace 'test.fstar.final.' shadows module 'testmain'
    in file "/home/milnes/Tuff/FinalFlog/test/src/fstar/fst/TestMain.fst".
  • Rename
    "/home/milnes/Tuff/FinalFlog/test/src/fstar/fst/TestMain.fst"
    to avoid conflicts.

is not like Warning N: at
and the emacs regexps that match compilation errors don't like multiple lines.
I've tried and can't get this to match.

It's simplest just to make the error file single line in the system.
I have the warnings/errors matching and a very nice way to configure fstar-mode for
working with Forge and opam vs local (everest) install vs a system compile (with all
the right includes working). I'll doc it on the wiki soon.

@briangmilnes
Copy link
Contributor Author

And it's printing the wrong case too:

  • Implicitly opening namespace 'test.fstar.final.' shadows module 'testmain'

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant