how to access command-line input arguments?

[alex4482]

Is there a way to access input arguments at the start of the main function?
like starting the exe like this: " ./Main.exe arg1 arg2 "
and using those parameters in the code

[nikswamy]

There's an OCaml library in ocaml/fstar-lib/FStar_GetOpt.ml that provides some utilities to manipulate command-line arguments.

There's an F* interface to this OCaml library, used by the F* compiler itself, in src/basic/FStar.Getopt.fsti

One way to proceed would be to define for your project an interface like so:

FStar.Getopt.fsti:

module FStar.Getopt

val cmdline (_:unit) : list string

You can call that in your main function to get the command line args, parse them as you like etc.
Then, when you extract the code to OCaml and link it against fstar-lib, it should link with FStar_Getopt.ml.

All of this reminds me that we should include such an interface in the F* standard library itself so that you don't have to define your own interface like this.