Hello Marius, Some responses to your questions are below.
Sent from Outlook<http://aka.ms/weboutlook> ________________________________ From: fstar-club <fstar-club-boun...@lists.gforge.inria.fr> on behalf of Marius Melzer via fstar-club <fstar-club@lists.gforge.inria.fr> Sent: Tuesday, September 1, 2020 3:00 PM To: fstar-club@lists.gforge.inria.fr <fstar-club@lists.gforge.inria.fr> Subject: [fstar-club] Execute F* using ocaml/opam package Hi, I'm just starting off with Fstar and I have a little bit setup problems. I installed fstar via opam and now I'm trying to get my project to compile&run via the ocaml code generation. 1) I exported to ocaml via: fstar.exe --codegen OCaml project.fst (this generated a lot of "Pattern uses these theory symbols or terms that should not be in an smt pattern: ..." warnings, is that ok to ignore? What do they mean exactly?). This anyways generates a bunch of ocaml files. The warning relates to the use of quantifiers encoded to the SMT solver. You can read more about it here: https://github.com/FStarLang/FStar/wiki/Quantifiers-and-patterns and http://fstar-lang.org/tutorial/tutorial.html#sec-smt-lemmas--bridging-the-gap-between-intrinsic-and-extrinsic-proofs It is safe to ignore this warning, at least as far as code extraction is concerned. However, the improper use of quantifier patterns can impact proof automation and stability. 2) I now want to compile the ocaml code and must as I read include the ml support library. The library is part of the installed opam package, at least this exists: ~/.opam/4.07.1/lib/fstarlib/, but an "ocamlfind ocamlopt -package fstarlib *.ml" only gets me ocamlfind: Package `fstarlib' not found - why doesn't this work and how can I get to a runnable executable here? Take a look at examples/hello/Makefile. It provides a template that you can follow for an F* project extracted to OCaml. In particular, it does (simplifying it a bit): fstar.exe --odir out --codegen OCaml --extract 'Hello' Hello.fst OCAMLPATH="../../bin" ocamlfind opt -package fstarlib -linkpkg -g out/Hello.ml -o hello.exe ./hello.exe It looks like your invocation of ocamlfind may be missing an OCAMLPATH setting? Hope that helps, Nik I realize that this might rather be an ocaml question and if this is the wrong place to ask it, please let me know then I will try to find another mailing list to ask about it. Thanks in advance, Marius _______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gforge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-club&data=02%7C01%7Cnswamy%40microsoft.com%7C633dbc379e324b9270cd08d84f05c374%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637346233897233895&sdata=NUEuPNwoMPCngt8ZcijJfklweC7nPd5Nf24jYZpsaOg%3D&reserved=0
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club