Running F* Programs Interactively with the OCaml Interactive Toplevel

We can extract F* programs and build them as executables, but what about extracting an F* program to OCaml, and then playing with it in the interactive toplevel? This can be done by loading the F* OCaml libraries into the toplevel, followed by the .ml file generated during extraction.

Extracting a program beyond the scope of this article. We assume that you have an output directory called "out" where the intermediate products of standard extraction are created, and the extracted OCaml is in a file called "myprogram.ml" in that directory. The key things to do are:

1. Start the ocaml toplevel with the F* binaries path in view so it can find the necessary libraries,
2. #use "topfind";; and then #require "fstarlib";; to load those libraries, and
3. #use "out/myprogram.ml";; to load your code.
4. When finished: #quit;; to exit the toplevel. In Cygwin, trying to Ctrl-C or Ctrl-D may freeze the Cygwin terminal window.

You can then interact with your code. You can't use built-in OCaml types for primitive values, like ints. For example, calling an F* function that takes an int has to be done like: fn (Prims.parse_int "2") rather than fn 2.

The ocaml toplevel is rather unforgiving in that it has little terminal support. Two possible options are to run "rlwrap ocaml" or to use "utop" as the toplevel. The author has not yet attempted these options.

A full execution is below:

$ OCAMLPATH=$FSTAR_HOME/bin ocaml

        OCaml version 4.05.0

# #use "topfind";;
- : unit = ()
Findlib has been successfully loaded. Additional directives:
  #require "package";;      to load a package
  #list;;                   to list the available packages
  #camlp4o;;                to load camlp4 (standard syntax)
  #camlp4r;;                to load camlp4 (revised syntax)
  #predicates "p,q,...";;   to set these predicates
  Topfind.reset();;         to force that packages will be reloaded
  #thread;;                 to enable threads

- : unit = ()
# #require "fstarlib";;
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ocaml: added to search path
C:/cygwin64/home/kkane/.opam/4.05.0+mingw64c/lib/ocaml\unix.cma: loaded
C:/cygwin64/home/kkane/.opam/4.05.0+mingw64c/lib/ocaml\nums.cma: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\num-top: added to search path
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\num-top\num_top.cma: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\num: added to search path
C:/cygwin64/home/kkane/.opam/4.05.0+mingw64c/lib/ocaml\bigarray.cma: loaded
C:/cygwin64/home/kkane/.opam/4.05.0+mingw64c/lib/ocaml\str.cma: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\bytes: added to search path
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\batteries: added to search path
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\batteries\batteries.cma: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\batteries\batteriesConfig.cmo: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\batteries\batteriesHelp.cmo: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\batteries\batteriesPrint.cmo: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\stdint: added to search path
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\stdint\stdint.cma: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\zarith: added to search path
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\zarith\zarith.cma: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\result: added to search path
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\result\result.cma: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving: added to search path
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving\ppx_deriving_runtime.cma: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving\./ppx_deriving: activated
ppx_deriving: C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving\./ppx_deriving_show.cma: option added
ppx_deriving: C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving\./ppx_deriving_eq.cma: option added
ppx_deriving: C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving\./ppx_deriving_ord.cma: option added
ppx_deriving: C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving\./ppx_deriving_enum.cma: option added
ppx_deriving: C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving\./ppx_deriving_iter.cma: option added
ppx_deriving: C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving\./ppx_deriving_map.cma: option added
ppx_deriving: C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving\./ppx_deriving_fold.cma: option added
ppx_deriving: C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving\./ppx_deriving_create.cma: option added
ppx_deriving: C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving\./ppx_deriving_make.cma: option added
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\easy-format: added to search path
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\easy-format\easy_format.cma: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\biniou: added to search path
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\biniou\biniou.cma: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\yojson: added to search path
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\yojson\yojson.cma: loaded
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving_yojson: added to search path
C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving_yojson\ppx_deriving_yojson_runtime.cma: loaded
ppx_deriving: C:\cygwin64\home\kkane\.opam\4.05.0+mingw64c\lib\ppx_deriving_yojson\./ppx_deriving_yojson.cma: option added
D:\sd\everest\FStar\bin\fstarlib: added to search path
D:/sd/everest/FStar/bin\fstarlib\fstarlib.cma: loaded
# #use "out/myprogram.ml";;
Hello myprogram
val main : Prims.unit = ()
val slicetest : Prims.nat -> Prims.nat FStar_Seq_Base.seq = <fun>
#