F# build on clean repo

gistfile1.txt

[hritcu@resurrected FStar]$ git status                                                                                 (git)-[master] 
On branch master
Your branch is up to date with 'origin/master'.

nothing to commit, working tree clean
[hritcu@resurrected FStar]$ ls bin                                                                                     (git)-[master] 
fstar-any.sh  fstar-compiler-lib  fstarlib  fstar-tactics-lib  tests-mono.sh
[hritcu@resurrected FStar]$ make -C src                                                                                (git)-[master] 
make: Entering directory '/home/hritcu/Temp/FStar/src'
mono VS/.nuget/NuGet.exe restore VS/FStar.sln
Installing 'FsLexYacc.Runtime 6.1.0'.
Installing 'PPrintForFSharp 0.0.2'.
Installing 'FSharp.Compatibility.OCaml 0.1.10'.
Installing 'FsLexYacc 6.1.0'.
Successfully installed 'PPrintForFSharp 0.0.2'.
Successfully installed 'FSharp.Compatibility.OCaml 0.1.10'.
Successfully installed 'FsLexYacc.Runtime 6.1.0'.
Successfully installed 'FsLexYacc 6.1.0'.
make -C VS install-packages
make[1]: Entering directory '/home/hritcu/Temp/FStar/src/VS'
[ -d packages ] || make update-nuget
mono .nuget/NuGet.exe restore FStar.sln
All packages listed in packages.config are already installed.
find packages -name '*.exe' -exec chmod +x '{}' ';'
make[1]: Leaving directory '/home/hritcu/Temp/FStar/src/VS'
/usr/bin/msbuild /verbosity:minimal /p:Configuration=Release VS/FStar.sln
Microsoft (R) Build Engine version 15.2.0.0 ( Thu May 11 17:28:41 UTC 2017)
Copyright (C) Microsoft Corporation. All rights reserved.

/home/hritcu/Temp/FStar/src/basic/boot/NotFStar.Util.fs(49,5): warning FS3190: Lowercase literal 'max_int' is being shadowed by a new pattern with the same name. Only uppercase and module-prefixed literals can be used as named patterns. [/home/hritcu/Temp/FStar/src/basic/basic.fsproj]
  basic -> /home/hritcu/Temp/FStar/bin/basic.dll
  Restoring NuGet packages...
  To prevent NuGet from downloading packages during build, open the Visual Studio Options dialog, click on the Package Manager node and uncheck 'Allow NuGet to download missing packages'.
  prettyprint -> /home/hritcu/Temp/FStar/bin/prettyprint.dll
  compiling to dfas (can take a while...)
  337 states
  writing output
  building tables
  computing first function...time: 00:00:00.0763897
  building kernels...time: 00:00:00.0983478
  building kernel table...time: 00:00:00.0073673
  computing lookahead relations............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................time: 00:00:00.5191532
  building lookahead table...time: 00:00:00.2468278
  building action table...state 429: shift/reduce error on SEMICOLON
  state 429: shift/reduce error on SEMICOLON_SEMICOLON
  state 464: shift/reduce error on BAR
  state 467: shift/reduce error on LBRACE
  state 468: shift/reduce error on BAR
  state 479: shift/reduce error on BAR
  state 554: shift/reduce error on COLON_EQUALS
  state 591: shift/reduce error on LBRACE
  time: 00:00:00.7768619
  building goto table...time: 00:00:00.2682482
  returning tables.
  8 shift/reduce conflicts
  761 states
  143 nonterminals
  140 terminals
  410 productions
  #rows in action table: 761
  parser -> /home/hritcu/Temp/FStar/bin/parser.dll
  syntax -> /home/hritcu/Temp/FStar/bin/syntax.dll
  tosyntax -> /home/hritcu/Temp/FStar/bin/tosyntax.dll
/home/hritcu/Temp/FStar/src/typechecker/FStar.TypeChecker.DMFF.fs(572,9): warning FS0025: Incomplete pattern matches on this expression. For example, the value 'Tm_ascribed (_, (_,Some (_)), _)' may indicate a case not covered by the pattern(s). [/home/hritcu/Temp/FStar/src/typechecker/typechecker.fsproj]
  typechecker -> /home/hritcu/Temp/FStar/bin/typechecker.dll
  format -> /home/hritcu/Temp/FStar/bin/format.dll
  reflection -> /home/hritcu/Temp/FStar/bin/reflection.dll
  extraction -> /home/hritcu/Temp/FStar/bin/extraction.dll
  fsdoc -> /home/hritcu/Temp/FStar/bin/fsdoc.dll
  smtencoding -> /home/hritcu/Temp/FStar/bin/smtencoding.dll
  tactics -> /home/hritcu/Temp/FStar/src/tactics/bin/Release/tactics.dll
  Consider app.config remapping of assembly "FSharp.Core, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" from Version "4.4.0.0" [/usr/lib/mono/gac/FSharp.Core/4.4.1.0__b03f5f7f11d50a3a/FSharp.Core.dll] to Version "4.4.1.0" [/usr/lib/mono/gac/FSharp.Core/4.4.1.0__b03f5f7f11d50a3a/FSharp.Core.dll] to solve conflict and get rid of warning.
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(1980,5): warning MSB3276: Found conflicts between different versions of the same dependent assembly. Please set the "AutoGenerateBindingRedirects" property to true in the project file. For more information, see http://go.microsoft.com/fwlink/?LinkId=294190. [/home/hritcu/Temp/FStar/src/fstar/fstar.fsproj]
  fstar -> /home/hritcu/Temp/FStar/bin/fstar.exe
  tests -> /home/hritcu/Temp/FStar/bin/tests.exe
dos2unix parser/parse.fsi
dos2unix: converting file parser/parse.fsi to Unix format...
chmod a+x ../bin/tests.exe
chmod a+x ../bin/fstar.exe
make: Leaving directory '/home/hritcu/Temp/FStar/src'
[hritcu@resurrected FStar]$ ./bin/fstar.exe --version                                                                  (git)-[master] 
F* 
platform=
compiler=
date=
commit=
[hritcu@resurrected FStar]$ ./bin/fstar.exe                                                                            (git)-[master] 
fstar.exe [options] file[s]
  --admit_smt_queries [true|false]  Admit SMT queries, unsafe! (default 'false')
  --admit_except [symbol|(symbol, id)]  Admit all queries, except those with label (<symbol>, <id>)) (e.g. --admit_except '(FStar.Fin.pigeonhole, 1)' or --admit_except FStar.Fin.pigeonhole)
  --cache_checked_modules  Write a '.checked' file for each module after verification and read from it if present, instead of re-verifying
  --codegen [OCaml|FSharp|Kremlin|tactics]  Generate code for execution
  --codegen-lib namespace  External runtime library (i.e. M.N.x extracts to M.N.X instead of M_N.x)
  --debug module_name  Print lots of debugging information while checking module
  --debug_level [Low|Medium|High|Extreme|...]  Control the verbosity of debugging info
  --dep [make|graph|full]  Output the transitive closure of the full dependency graph in three formats:
	 'graph': a format suitable the 'dot' tool from 'GraphViz'
	 'full': a format suitable for 'make', including dependences for producing .ml files
	 'make': (deprecated) a format suitable for 'make', including only dependences among source files
  --detail_errors  Emit a detailed error report by asking the SMT solver many queries; will take longer;
         implies n_cores=1
  --detail_hint_replay  Emit a detailed report for proof whose unsat core fails to replay;
         implies n_cores=1
  --doc  Extract Markdown documentation files for the input modules, as well as an index. Output is written to --odir directory.
  --dump_module module_name
  --eager_inference  Solve all type-inference constraints eagerly; more efficient but at the cost of generality
  --extract_module module_name  Only extract the specified modules (instead of the possibly-partial dependency graph)
  --extract_namespace namespace name  Only extract modules in the specified namespace
  --expose_interfaces  Explicitly break the abstraction imposed by the interface of any implementation file that appears on the command line (use with care!)
  --fstar_home dir  Set the FSTAR_HOME variable to <dir>
  --gen_native_tactics [path]  Compile all user tactics used in the module in <path>
  --hide_uvar_nums  Don't print unification variable numbers
  --hint_file path  Read/write hints to <path> (instead of module-specific hints files)
  --hint_info  Print information regarding hints (deprecated; use --query_stats instead)
  --in  Legacy interactive mode; reads input from stdin
  --ide  JSON-based interactive mode for IDEs
  --include path  A directory in which to search for files included on the command line
  --indent  Parses and outputs the files on the command line
  --initial_fuel non-negative integer  Number of unrolling of recursive functions to try initially (default 2)
  --initial_ifuel non-negative integer  Number of unrolling of inductive datatypes to try at first (default 1)
  --lax  Run the lax-type checker only (admit all verification conditions)
  --load module  Load compiled module
  --log_types  Print types computed for data/val/let-bindings
  --log_queries  Log the Z3 queries in several queries-*.smt2 files, as we go
  --max_fuel non-negative integer  Number of unrolling of recursive functions to try at most (default 8)
  --max_ifuel non-negative integer  Number of unrolling of inductive datatypes to try at most (default 2)
  --min_fuel non-negative integer  Minimum number of unrolling of recursive functions to try (default 1)
  --MLish  Trigger various specializations for compiling the F* compiler itself (not meant for user code)
  --n_cores positive_integer  Maximum number of cores to use for the solver (implies detail_errors = false) (default 1)
  --no_default_includes  Ignore the default module search paths
  --no_extract module name  Do not extract code from this module
  --no_location_info  Suppress location information in the generated OCaml output (only relevant with --codegen OCaml)
  --odir dir  Place output in directory <dir>
  --prims file
  --print_bound_var_types  Print the types of bound variables
  --print_effect_args  Print inferred predicate transformers for all computation types
  --print_full_names  Print full names of variables
  --print_implicits  Print implicit arguments
  --print_universes  Print universes
  --print_z3_statistics  Print Z3 statistics for each SMT query (deprecated; use --query_stats instead)
  --prn  Print full names (deprecated; use --print_full_names instead)
  --query_stats  Print SMT query statistics
  --record_hints  Record a database of hints for efficient proof replay
  --reuse_hint_for toplevel_name  Optimistically, attempt using the recorded hint for <toplevel_name> (a top-level name in the current module) when trying to verify some other term 'g'
  --silent   
  --smt path  Path to the Z3 SMT solver (we could eventually support other solvers)
  --smtencoding.elim_box [true|false]  Toggle a peephole optimization that eliminates redundant uses of boxing/unboxing in the SMT encoding (default 'false')
  --smtencoding.nl_arith_repr [native|wrapped|boxwrap]  Control the representation of non-linear arithmetic functions in the SMT encoding:
		i.e., if 'boxwrap' use 'Prims.op_Multiply, Prims.op_Division, Prims.op_Modulus'; 
		if 'native' use '*, div, mod';
		if 'wrapped' use '_mul, _div, _mod : Int*Int -> Int'; 
		(default 'boxwrap')
  --smtencoding.l_arith_repr [native|boxwrap]  Toggle the representation of linear arithmetic functions in the SMT encoding:
		i.e., if 'boxwrap', use 'Prims.op_Addition, Prims.op_Subtraction, Prims.op_Minus'; 
		if 'native', use '+, -, -'; 
		(default 'boxwrap')
  --split_cases positive_integer  Partition VC of a match into groups of <positive_integer> cases
  --tactic_raw_binders  Do not use the lexical scope of tactics to improve binder names
  --tactic_trace  Print a depth-indexed trace of tactic execution (Warning: very verbose)
  --tactic_trace_d positive_integer  Trace tactics up to a certain binding depth
  --timing  Print the time it takes to verify each top-level definition
  --trace_error  Don't print an error message; show an exception trace instead
  --ugly  Emit output formatted for debugging
  --unthrottle_inductives  Let the SMT solver unfold inductive types to arbitrary depths (may affect verifier performance)
  --unsafe_tactic_exec  Allow tactics to run external processes. WARNING: checking an untrusted F* file while using this option can have disastrous effects.
  --use_eq_at_higher_order  Use equality constraints when comparing higher-order types (Temporary)
  --use_hints  Use a previously recorded hints database for proof replay
  --use_hint_hashes  Admit queries if their hash matches the hash recorded in the hints database
  --use_native_tactics path  Use compiled tactics from <path>
  --no_tactics  Do not run the tactic engine before discharging a VC
  --using_facts_from One or more space-separated occurrences of '[+|-]( * | namespace | fact id)'  
		Prunes the context to include only the facts from the given namespace or fact id. 
			Facts can be include or excluded using the [+|-] qualifier. 
			For example --using_facts_from '* -FStar.Reflection +FStar.List -FStar.List.Tot' will 
				remove all facts from FStar.List.Tot.*, 
				retain all remaining facts from FStar.List.*, 
				remove all facts from FStar.Reflection.*, 
				and retain all the rest.
		Note, the '+' is optional: --using_facts_from 'FStar.List' is equivalent to --using_facts_from '+FStar.List'. 
		Multiple uses of this option accumulate, e.g., --using_facts_from A --using_facts_from B is interpreted as --using_facts_from A^B.
  --__temp_no_proj module_name  Don't generate projectors for this module
  --version  Display version number
  --warn_default_effects  Warn when (a -> b) is desugared to (a -> Tot b)
  --z3cliopt option  Z3 command line options
  --z3refresh  Restart Z3 after each query; useful for ensuring proof robustness
  --z3rlimit positive_integer  Set the Z3 per-query resource limit (default 5 units, taking roughtly 5s)
  --z3rlimit_factor positive_integer  Set the Z3 per-query resource limit multiplier. This is useful when, say, regenerating hints and you want to be more lax. (default 1)
  --z3seed positive_integer  Set the Z3 random seed (default 0)
  --use_two_phase_tc [true|false]  Use the two phase typechecker (default 'false')
  --__no_positivity  Don't check positivity of inductive types
  --__ml_no_eta_expand_coertions  Do not eta-expand coertions in generated OCaml
  --warn_error   The [-warn_error] option follows the OCaml syntax, namely:
		- [r] is a range of warnings (either a number [n], or a range [n..n])
		- [-r] silences range [r]
		- [+r] enables range [r]
		- [@r] makes range [r] fatal.
  --help  Display this information
[hritcu@resurrected FStar]$ ls bin                                                                                     (git)-[master] 
basic.dll              fsdoc.dll                       fstar-any.sh        parser.XML       syntax.pdb        tosyntax.pdb
basic.pdb              fsdoc.dll.config                fstar-compiler-lib  prettyprint.dll  syntax.XML        tosyntax.XML
basic.XML              fsdoc.pdb                       fstar.exe           prettyprint.pdb  tactics.dll       typechecker.dll
extraction.dll         fsdoc.XML                       fstar.exe.config    prettyprint.XML  tactics.pdb       typechecker.pdb
extraction.dll.config  FSharp.Compatibility.OCaml.dll  fstarlib            reflection.dll   tests.exe         typechecker.XML
extraction.pdb         FSharp.Core.dll                 fstar.pdb           reflection.pdb   tests.exe.config
extraction.XML         FSharp.Core.xml                 fstar-tactics-lib   smtencoding.dll  tests-mono.sh
format.dll             FSharp.PPrint.dll               fstar.XML           smtencoding.pdb  tests.pdb
format.pdb             FsLexYacc.Runtime.dll           parser.dll          smtencoding.XML  tests.XML
format.XML             FsLexYacc.Runtime.xml           parser.pdb          syntax.dll       tosyntax.dll