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 337 does not produce a line number in the language server #3516

Open
briangmilnes opened this issue Oct 2, 2024 · 0 comments
Open

Comments

@briangmilnes
Copy link
Contributor

If you foolishly add a decreases to an interface you get a 337 but in the language server
it does not give you a line number. Perhaps a sweep of all warnings in the compiler
for this difference should be quickly performed also.
FSTI:
module MultipleDecreases
val length #a (l:list a) : Tot nat (decreases l)
module MultipleDecreases

let rec length #a (l:list a)
: Tot nat (decreases l)
= match l with
| [] -> 0
| _ :: tl -> length tl

// In the language server no line is produced
//(Warning 337) - This definitions has multiple decreases clauses.
//- The decreases clause on the declaration is ignored, please remove it.
// In the compiler the error has a line
//qqmake -k validate
//Forge: VALIDATE _build/fstar/fst/checked directory
//F
orge: VALIDATE make -k _build/fstar/fst/checked/MultipleDecreases.fsti.checked //_build/fstar/fst/checked/MultipleDecreases.fst.checked PROJECT=multipledecreases
//Forge: VALIDATE _build/fstar/fst/checked/MultipleDecreases.fsti.checked
//F
orge: VALIDATE _build/fstar/fst/checked/MultipleDecreases.fst.checked
//* Warning 337 at src/MultipleDecreases.fst(3,8-3,14):
// - This definitions has multiple decreases clauses.

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