FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Warning 337 does not produce a line number in the language server

Open briangmilnes opened this issue 4 months ago • 0 comments

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 //Forge: 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 //Forge: VALIDATE _build/fstar/fst/checked/MultipleDecreases.fst.checked //* Warning 337 at src/MultipleDecreases.fst(3,8-3,14): // - This definitions has multiple decreases clauses.

briangmilnes avatar Oct 02 '24 21:10 briangmilnes