Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
76 lines (65 sloc) 2.38 KB
# 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
#
# To use landmarks to profile ocaml code:
# - make sure landmarks is installed with opam (opam install landmarks)
# - enable the landmarks and landmarks.ppx packages
# - select the modules for auto-instrumentation
# - build the compiler
# - run the compiler with OCAML_LANDMARKS='on,output=landmarks.out'
#
# Uncomment the following to add the packages:
#
# true: \
# package(landmarks), \
# package(landmarks.ppx)
#
# Uncomment the following to profile specific modules:
#
# <src/ocaml-output/FStar_{Main,Dependencies,Universal,TypeChecker_Normalize,TypeChecker_Tc,TypeChecker_Util,SMTEncoding_Encode}.ml>: \
# ppx(`ocamlfind query landmarks.ppx`/ppx.exe --as-ppx --auto)
#
#
# NB: the fully inclusive landmarks ppx on ocaml-output/**/*.ml files can cause a stack overflow
# <src/ocaml-output/**/*.ml>: \
# ppx(`ocamlfind query landmarks.ppx`/ppx.exe --as-ppx --auto)
#
You can’t perform that action at this time.