Re: [fstar-club] bug report (wrong cast from I32)

2020-03-17 Thread paul zimmermann via fstar-club
inconvenience. > > Regards, > Catalin > > > On Wed, Jul 3, 2019 at 8:04 AM paul zimmermann via fstar-club > wrote: > > > >Dear Jonathan, > > > > > From: Jonathan Protzenko > > > Date: Wed, 3 Jul 2019 05:30:37 + > > >

Re: [fstar-club] bug report (wrong cast from I32)

2019-07-03 Thread paul zimmermann via fstar-club
Dear Jonathan, > From: Jonathan Protzenko > Date: Wed, 3 Jul 2019 05:30:37 + > > Hello Paul and Félix, > > Thanks for the bug report -- I've filed > https://github.com/FStarLang/FStar/issues/1803 > > Out of curiosity, what was your initial interest in F*? Are you interested in >

[fstar-club] bug report (wrong cast from I32)

2019-07-02 Thread paul zimmermann via fstar-club
Hi, with Félix Breton (in cc) we get the following behaviour: module Bug open FStar.HyperStack.IO module I32 = FStar.Int32 let main () = if (I32.((-1l) <^ 0l)) then print_string "correct\n" else print_string "wrong\n"; 0 This prints "wrong", and was compiled

[fstar-club] INSTALL.md

2019-07-02 Thread paul zimmermann via fstar-club
Hi, on https://github.com/FStarLang/FStar/blob/master/INSTALL.md#building-f-from-sources, paragraph "Instructions for all OSes", Step 4, in the line $ opam install ocamlbuild ocamlfind ..., the 'pprint' package is listed twice. Maybe this is wanted? Best regards, Paul Zimmermann