diff --git a/_tags b/_tags index 4b7598cbed9..095d61f3b4f 100644 --- a/_tags +++ b/_tags @@ -10,7 +10,8 @@ true: \ annot, bin_annot, thread, -traverse, \ package(batteries), \ package(zarith), \ - package(ppx_deriving.std), package(ppx_deriving_yojson) + package(ppx_deriving.std), \ + package(ppx_deriving_yojson) # ADL: the new unicode lexer "src/parser/ml/FStar_Parser_LexFStar.ml": syntax(camlp4o) @@ -47,3 +48,29 @@ true: \ <**/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: +# +# : \ +# 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 +# : \ +# ppx(`ocamlfind query landmarks.ppx`/ppx.exe --as-ppx --auto) +#