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. 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? 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://lists.gforge.inria.fr/mailman/listinfo/fstar-club
