search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Tutorial module Ex01a doesn't compile #1717

Closed brianberns closed 5 years ago

brianberns commented 5 years ago

https://www.fstar-lang.org/tutorial/

Expected behavior: Tutorial module compiles cleanly

Observed behavior:

Ex01a(63,0-63,48): (Warning 272) Top-level let-bindings must be total; this term may have effects
Ex01a(63,0-63,48): (Warning 272) Top-level let-bindings must be total; this term may have effects
Ex01a(53,21-53,28): (Error 12) Expected type "Prims.unit"; but "Ex01a.write f" has type "s: Prims.string -> FStar.All.ML Prims.unit"
Ex01a(53,21-53,28): (Error 12) Expected type "Prims.unit"; but "Ex01a.write f" has type "s: Prims.string -> FStar.All.ML Prims.unit"
Verified module: Ex01a (1352 milliseconds)
2 errors were reported (see above)
catalin-hritcu commented 5 years ago

@brianberns What exactly are you doing to get these errors? I just tried and everything works fine from the web interface:screenshot attached Also all this code is under CI, so it works for us!

brianberns commented 5 years ago

I just tried it again and got the same output as you, so I'll close this issue. Thanks.