Hi Jonathan, thank you again for the tutorial - it is a very valuable resource and filled a lot of knowledge gaps. I have one more question regarding strings: Is it correct that there is currently no way to print a buffer of chars? The `server` example calls printf directly from C, and looking through the libraries, I couldn't find any fwrite or printf functions to use from Low* itself. (I'm aware of print_bytes, but that's not really useful for printing chars). I'd be happy to take a stab at implementing fwrite if that would be useful for the project. Best regards,
-- Pierre Beaucamp On Wed, May 2, 2018, at 11:08 AM, Jonathan Protzenko wrote: > Yes, this is something that has poor usability. Prims.string and > FStar.String.concat are supported as transition mechanisms to help > porting F* programs to Low* but I agree that it's confusing for > beginners to have them work "by default".> > https://fstarlang.github.io/lowstar/html/LowStar.html#c-string-literals > has a note that explains it, my plan is to make it a warning that's > fatal by default, and that can be disabled if you need these > mechanisms> > ~ jonathan > > *From:* Pierre Beaucamp <m...@pierrebeaucamp.com> *Sent:* Tuesday, > May 1, 2018 4:38 PM *To:* Jonathan Protzenko; Pierre Beaucamp via > fstar-club *Subject:* Re: [fstar-club] Trying to use List.Tot.map > with Kremlin> > > Thanks for the quick answer Jonathan. > > I already assumed that this is caused by limited inter-polarity > between F* strings and their representation in Low*. What threw me > off is that this code works: > > let main () = > C.print_string (C.string_of_literal (String.concat ", " > ["hello"; "world"])); > C.exit_success > > Either way, I'm excited for the Low* tutorial - thank you for writing > it. This is a very interesting language with unfortunately very > little documentation for new-comers (I'm pretty much trying to learn > F* and Low* at the same time, and I guess this is where a lot of the > confusion is coming from). > > Thank you and best regards, > > -- > Pierre Beaucamp > > On Tue, May 1, 2018, at 7:09 PM, Jonathan Protzenko wrote: > > Hello Pierre, > > > > These are all excellent questions -- I am currently writing a > > tutorial for Low* are these served as good inspiration for the > > introduction. If CI goes through, a work-in-progress version of the > > tutorial should be uploaded in the next few hours at > > > https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffstarlang.github.io%2Flowstar%2F&data=02%7C01%7Cprotz%40microsoft.com%7Cdb40113318a44ce8c0be08d5afbc9c55%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608146970557404&sdata=aLvfTn4cd9Wrvck8prnVvnQfEA9I3BPpp1%2BE0PkjGpw%3D&reserved=0 > > -- please read it and let me know whether after browsing it, your > > questions have been answered. > > > > In case the CI doesn't perform the upload, or the tutorial is > > unclear, the essence of your issue is that your code is not Low*. > > > > * the F* string and list types are F* values, i.e. concat has > > type string -> string -> string; the only way to give you > > these semantics without requiring the user to track > > allocations and lifetimes is to use a garbage-collector, > > which C does not have > > * the same goes for lists: compiling them to C with the current > > F* value semantics would lead to a zillion uncollected list > > cell allocations. > > > > What the C.String module provides is a bare-bones model of C string > > literals, i.e. `const char *s = "my string literal";`, meaning that > > you should provide an actual literal, e.g. `C.String.( print > > !$"hello, world \n" );`. This is very limited, and does not allow > > you to do arbitrary string manipulation. > > > > A proof-of-concept example exists that does that, in the test/ > > subdirectory of KreMLin, and is called Server.fst. It models > > blitting > > C.String.t's into a mutable buffer of C chars, tracking how much > > space remains in your buffer, whether the buffer is live, etc. > > and rules out buffer overflows. > > > > Naturally, it's a little involved for a hello world, but I guess > > that's the reality of tracking temporal (liveness) and spatial > > safety (bounds) in C. > > > > Let me know if that helps. > > > > Cheers, > > > > Jonathan > > > > > > ~ jonathan > > > > ________________________________ > > From: fstar-club <fstar-club-boun...@lists.gforge.inria.fr> on > > behalf of Pierre Beaucamp via fstar-club <fstar- > > c...@lists.gforge.inria.fr> Sent: Tuesday, May 1, 2018 9:48 AM To: > > fstar-club@lists.gforge.inria.fr Subject: [fstar-club] Trying to > > use List.Tot.map with Kremlin > > > > Hi everyone, > > > > I'm just playing a bit around with F-Star and Kremlin and I seem to > > be stuck at a simple problem. I don't know if I'm missing something > > obvious or if this might be a bug. My code looks like this: > > > > let main () = > > C.print_string (C.string_of_literal (String.concat ", " > > (List.Tot.map string_of_int [1; 2; 3]))); > > C.exit_success > > > > I expect this code to print `1, 2, 3` but instead I get the > > following runtime error: > > > > KreMLin abort at ./Main.c:9 This function was not > > extracted: Failure("Cannot extract string_of_literal > > applied to a non-literal") > > > > I tried some variations of the above program to see if I can reverse- > > engineer what is going on, but as soon as I introduce > > `List.Tot.map`, the code breaks. I know that there is also > > `C.Loops.map`, but I don't know if I really need to use buffers to > > make it work. > > > > Also, I'm generally interested in learning more about Kremlin / > > Low* / F*. If there are any recommended resources or other helpful > > links, feel free to share them with me. > > > > Thank you and best regards, > > > > -- > > Pierre Beaucamp > > _______________________________________________ > > fstar-club mailing list fstar-club@lists.gforge.inria.fr > > > https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gforge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-club&data=02%7C01%7Cprotz%40microsoft.com%7C445acbbb8a104079b70808d5af83d2b8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636607903120375441&sdata=WkxhslLqaMBwupJazX4IDfRaWwsqX6IIiuWZT8YrwFc%3D&reserved=0> >
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
