_tags

# Warnings:
# 8	Partial match: missing cases in pattern-matching.
# 11	Redundant case in a pattern matching (unused match case).
# 20    This argument will not be used by the function.
# 21	Non-returning statement.
# 26	Suspicious unused variable: unused variable that is bound with let or as, and doesn’t start with an underscore (_) character.
# 28	Wildcard pattern given as argument to a constant constructor.

true: \
  annot, bin_annot, thread, -traverse, \
  package(batteries), \
  package(zarith), \
  package(ppx_deriving.std), package(ppx_deriving_yojson)

# ADL: the new unicode lexer
"src/parser/ml/FStar_Parser_LexFStar.ml": syntax(camlp4o)

# ADL: Please do not enable compiler-libs unless absolutely necessary
<src/*/ml/*> or <src/ocaml-output/*.ml>: \
  package(compiler-libs), \
  package(compiler-libs.common), \
  package(menhirLib), \
  package(dynlink), \
  package(pprint), \
  package(ulex), \
  package(stdint), \
  package(yojson), \
  package(ocaml-migrate-parsetree), \
  package(process)

# This ensures that main.native bundles its dependencies, which dynlinked tactics might need.
"src/fstar/ml/main.native": \
  linkall

# Turn off warnings for extracted files
<src/ocaml-output/**/*.ml> or <ulib/**/extracted/*.ml> or <ulib/tactics_ml/fstarlib_leftovers/*.ml>: \
  warn(-8-11-20-21-26-28)

<ulib/ml/FStar_{U,}Int*.ml>  or "ulib/ml/fstarlib.cma": \
  package(stdint)

"ulib/ml/fstarlib.cma": \
  linkpkg

<ulib/tactics_ml/**/*.ml>: \
  package(fstar-compiler-lib)

<**/FStar_Monotonic_Seq.ml>: \
  principal