Hello Marius,
Some responses to your questions are below.
Sent from Outlook<http://aka.ms/weboutlook>
From: fstar-club on behalf of Marius
Melzer via fstar-club
Sent: Tuesday, September 1, 2020 3:00 PM
To: 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 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-clubdata=02%7C01%7Cnswamy%40microsoft.com%7C633dbc379e324b9270cd08d84f05c374%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637346233897233895sdata=NUEuPNwoMPCngt8ZcijJfklweC7nPd5Nf24jYZpsaOg%3Dreserved=0
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
