infer_clone/scripts/toplevel_init

(* to be used with infertop, infer's custom toplevel *)

(* load dependencies *)
#use "topfind";;
#thread;;
#require "cmdliner";;
#require "core.top";;
#require "ctypes";;
#require "ctypes.stubs";;
#require "sawja";;
#require "atdgen";;
#require "xmlm";;
#require "ANSITerminal";;

open InferStdlib;;
open InferGenerated;;
open InferModules;;
[make] s/ocamlbuild/jbuilder/g Summary: Use jbuilder to build infer instead of ocamlbuild. This is mainly to get faster builds: ``` times in 10ms, ±differences measured in speedups, 4 cores \| \| ocb total \| jb \| ±total \| ocb user \| jb \| ±user \| ocb cpu \| jb \| ±cpu \| ocb sys \| jb \| ±sys \| \|-----------------------------------+-----------+------+--------+----------+------+-------+---------+-----+------+---------+------+------\| \| byte from scratch \| 6428 \| 2456 \| 2.62 \| 7743 \| 6662 \| 1.16 \| 138 \| 331 \| 2.40 \| 1184 \| 1477 \| 0.80 \| \| native from scratch \| 9841 \| 4289 \| 2.29 \| 9530 \| 8834 \| 1.08 \| 110 \| 245 \| 2.23 \| 1373 \| 1712 \| 0.80 \| \| byte after native \| 29578 \| 1602 \| 18.46 \| 4514 \| 4640 \| 0.97 \| 170 \| 325 \| 1.91 \| 543 \| 576 \| 0.94 \| \| change infer.ml byte \| 344 \| 282 \| 1.22 \| 292 \| 215 \| 1.36 \| 96 \| 99 \| 1.03 \| 040 \| 066 \| 0.61 \| \| change infer.ml native \| 837 \| 223 \| 3.75 \| 789 \| 174 \| 4.53 \| 98 \| 99 \| 1.01 \| 036 \| 47 \| 0.77 \| \| change Config.ml byte \| 451 \| 339 \| 1.33 \| 382 \| 336 \| 1.14 \| 97 \| 122 \| 1.26 \| 056 \| 80 \| 0.70 \| \| change Config.ml native \| 4024 \| 1760 \| 2.29 \| 4585 \| 4225 \| 1.09 \| 127 \| 276 \| 2.17 \| 559 \| 644 \| 0.87 \| \| change cFrontend_config.ml byte \| 348 \| 643 \| 0.54 \| 297 \| 330 \| 0.90 \| 96 \| 67 \| 0.70 \| 038 \| 102 \| 0.37 \| \| change cFrontend_config.ml native \| 1480 \| 584 \| 2.53 \| 1435 \| 906 \| 1.58 \| 106 \| 185 \| 1.75 \| 136 \| 178 \| 0.76 \| #+TBLFM: $4=$2/$3;f2::$7=$5/$6;f2::$10=$9/$8;f2::$13=$11/$12;f2 50 cores \| \| ocb total \| jb \| ±total \| ocb user \| jb \| ±user \| ocb cpu \| jb \| ±cpu \| ocb sys \| jb \| ±sys \| \|---------------------+-----------+------+--------+----------+------+-------+---------+----+------+---------+------+------\| \| byte from scratch \| 9114 \| 2061 \| 4.42 \| 9334 \| 5133 \| 1.82 \| \| \| 0/0 \| 2566 \| 1726 \| 1.49 \| \| native from scratch \| 13481 \| 3967 \| 3.40 \| 12291 \| 7608 \| 1.62 \| \| \| 0/0 \| 3003 \| 2100 \| 1.43 \| \| byte after native \| 3467 \| 1476 \| 2.35 \| 5067 \| 3912 \| 1.30 \| \| \| 0/0 \| 971 \| 801 \| 1.21 \| #+TBLFM: $4=$2/$3;f2::$7=$5/$6;f2::$10=$9/$8;f2::$13=$11/$12;f2 ``` Menu: 1. Write a jbuild file, autogenerated from jbuild.in because we need to fill in some information at build-time (really, at configure time, but TODO), such as whether or not clang is enabled. 2. Nuke lots of stuff from infer/src/Makefile that is now in the jbuild file 3. The jbuild file lives in infer/src/ so it can see all the sources. If we put it somewhere else, eg, infer/, then `jbuilder` scans too many files (all irrelevant) and takes 2.5s to start instead of .8s. Adding irrelevant directories to jbuild-ignore does not help. 4. jbuilder does not support subdirectories, so resort to listing all the source files in the generated jbuild (only source directories need to be manually listed in jbuild.in though). Still, the generated .merlin is wrong and makes merlin find source files in _build, so manually tune it to get good merlin support. We also lose some of merlin for unit tests as it cannot see their build artefacts anymore. 5. checkCopyright gets its own jbuild because it's standalone. Also, remove some deprecation warnings in checkCopyright due to the new version of Core from a while ago. 6. Drop less-used Makefile features (they had regressed anyway) such as building individual modules. Also, building mod_dep.pdf now takes all the source files available so they better build (before, it would only take the source files from the config, eg with or without clang) (that's pretty minor). 7. The toplevel is now built as a custom toplevel because that was easier. It should soon be even easier: https://github.com/janestreet/jbuilder/issues/210 8. Move BUILTINS.mli to BUILTINS.ml because jbuilder is not happy about interface files without implementations. In particular, I did not try to migrate too much of the Makefile logic to jbuilder, more can be done in the future. Reviewed By: jberdine Differential Revision: D5573661 fbshipit-source-id: 4ca6d8f 7 years ago			`(* to be used with infertop, infer's custom toplevel *)`

Add basic support for starting ocaml repl with infer code Summary: Make it possible to run infer code from within `ocaml`/`utop`. Integration is really basic, but we can extend it if we find it useful. Reviewed By: jberdine Differential Revision: D3736029 fbshipit-source-id: 4cebb7c 8 years ago			`(* load dependencies *)`
			`#use "topfind";;`
Add tuareg and core as dependencies Reviewed By: jvillard, jberdine Differential Revision: D4066732 fbshipit-source-id: eccb89e 8 years ago			`#thread;;`
[config] migrate help to use man pages Summary: Glorious, glorious man pages. This changes a bunch of things that were hard to break up from the diff, so the resulting diff is big. Use `Cmdliner.Manpage` to format man pages (and also format a bit ourselves since it is so stubborn). As a bonus, introduce the following subcommands: ``` infer run ... # same as default mode with -- before infer capture ... # -a capture infer compile ... # -a compile infer analyze ... # InferAnalyze infer report ... # InferPrint infer diff ... # this one is not new infer clang ... # InferClang, not that you should use it ``` The man pages can still be improved a lot. Notable missing sections: `ENVIRONMENT`, stuff about .inferconfig, some example usage, `DESCRIPTION`, ... Reviewed By: jberdine Differential Revision: D4921083 fbshipit-source-id: 9602230 8 years ago			`#require "cmdliner";;`
[build] move to ctypes stubs Summary: This removes the dependency of libffi, and gives better guarantees at compile-time. A bit overkill to retrieve the width of the terminal but what do you know... Reviewed By: jberdine Differential Revision: D4700003 fbshipit-source-id: 036989b 8 years ago			`#require "core.top";;`
[utils] Add CTypes binding of fts and implement remove_directory_tree Summary: This diff adds a dependency on ctypes.foreign and uses the example binding of fts to implement remove_directory_tree. Reviewed By: yunxing Differential Revision: D4115569 fbshipit-source-id: 3509955 8 years ago			`#require "ctypes";;`
[build] move to ctypes stubs Summary: This removes the dependency of libffi, and gives better guarantees at compile-time. A bit overkill to retrieve the width of the terminal but what do you know... Reviewed By: jberdine Differential Revision: D4700003 fbshipit-source-id: 036989b 8 years ago			`#require "ctypes.stubs";;`
Add basic support for starting ocaml repl with infer code Summary: Make it possible to run infer code from within `ocaml`/`utop`. Integration is really basic, but we can extend it if we find it useful. Reviewed By: jberdine Differential Revision: D3736029 fbshipit-source-id: 4cebb7c 8 years ago			`#require "sawja";;`
			`#require "atdgen";;`
[mvn] new integration Summary: This replaces the previous integration written in Python, which consisted in 1) run the mvn command and parse its output to locate "directories containing source files", 2) run on files named "*.java" in these directories. This meant we had to run javac twice on each source file, and more importantly this mechanism of finding source files was very fragile. In fact, I could not make it work on several mvn projects I tried. The new integration is based on parsing "pom.xml" to add an "infer-capture" profile which instructs mvn to run `/path/to/infer` instead of `javac`. We also add this profile to each maven submodule. Users can specify an "infer-capture" profile themselves if the default one doesn't work; in that case we don't inject our own "infer-capture" profile. Reviewed By: jeremydubreil Differential Revision: D4409613 fbshipit-source-id: d664274 8 years ago			`#require "xmlm";;`
[CTL] Initial version of a step-by-step debugger for CTL formulas Summary: This debugger stops the execution of CTL during the evaluation of formulas, then shows useful info about the current state: - Which formula is being evaluated - In which part of the AST is such formula being evaluated - Line number of the source file - Whether a CTL-Transition will take place or not - Node-ID that can be related to the dotty file containing the evaluation graph (the one in infer-out/lint_dotty/) The AST is shown with coloured nodes, where each colour has the following meaning: - [Default terminal colour], Bold: The node is being evaluated - Green, Bold: The formula returned true on the current node - Red, Bold: The formula returned false on the current node Reviewed By: ddino Differential Revision: D4834451 fbshipit-source-id: c9aa970 8 years ago			`#require "ANSITerminal";;`
Add basic support for starting ocaml repl with infer code Summary: Make it possible to run infer code from within `ocaml`/`utop`. Integration is really basic, but we can extend it if we find it useful. Reviewed By: jberdine Differential Revision: D3736029 fbshipit-source-id: 4cebb7c 8 years ago
[jbuilder] turn I{Std,List} and atd-generated files into libraries Summary: This simplifies the jbuild files: no need to list these files explicitly anymore, nor to exclude them explicitly from the main `InferModules` library (due to their different compilation flags). Isolate common parts into jbuild.common do `cat`-based code inclusion into jbuild files to factorize code. Reviewed By: jberdine Differential Revision: D5678328 fbshipit-source-id: 6d7d925 7 years ago			`open InferStdlib;;`
			`open InferGenerated;;`
[make] s/ocamlbuild/jbuilder/g Summary: Use jbuilder to build infer instead of ocamlbuild. This is mainly to get faster builds: ``` times in 10ms, ±differences measured in speedups, 4 cores \| \| ocb total \| jb \| ±total \| ocb user \| jb \| ±user \| ocb cpu \| jb \| ±cpu \| ocb sys \| jb \| ±sys \| \|-----------------------------------+-----------+------+--------+----------+------+-------+---------+-----+------+---------+------+------\| \| byte from scratch \| 6428 \| 2456 \| 2.62 \| 7743 \| 6662 \| 1.16 \| 138 \| 331 \| 2.40 \| 1184 \| 1477 \| 0.80 \| \| native from scratch \| 9841 \| 4289 \| 2.29 \| 9530 \| 8834 \| 1.08 \| 110 \| 245 \| 2.23 \| 1373 \| 1712 \| 0.80 \| \| byte after native \| 29578 \| 1602 \| 18.46 \| 4514 \| 4640 \| 0.97 \| 170 \| 325 \| 1.91 \| 543 \| 576 \| 0.94 \| \| change infer.ml byte \| 344 \| 282 \| 1.22 \| 292 \| 215 \| 1.36 \| 96 \| 99 \| 1.03 \| 040 \| 066 \| 0.61 \| \| change infer.ml native \| 837 \| 223 \| 3.75 \| 789 \| 174 \| 4.53 \| 98 \| 99 \| 1.01 \| 036 \| 47 \| 0.77 \| \| change Config.ml byte \| 451 \| 339 \| 1.33 \| 382 \| 336 \| 1.14 \| 97 \| 122 \| 1.26 \| 056 \| 80 \| 0.70 \| \| change Config.ml native \| 4024 \| 1760 \| 2.29 \| 4585 \| 4225 \| 1.09 \| 127 \| 276 \| 2.17 \| 559 \| 644 \| 0.87 \| \| change cFrontend_config.ml byte \| 348 \| 643 \| 0.54 \| 297 \| 330 \| 0.90 \| 96 \| 67 \| 0.70 \| 038 \| 102 \| 0.37 \| \| change cFrontend_config.ml native \| 1480 \| 584 \| 2.53 \| 1435 \| 906 \| 1.58 \| 106 \| 185 \| 1.75 \| 136 \| 178 \| 0.76 \| #+TBLFM: $4=$2/$3;f2::$7=$5/$6;f2::$10=$9/$8;f2::$13=$11/$12;f2 50 cores \| \| ocb total \| jb \| ±total \| ocb user \| jb \| ±user \| ocb cpu \| jb \| ±cpu \| ocb sys \| jb \| ±sys \| \|---------------------+-----------+------+--------+----------+------+-------+---------+----+------+---------+------+------\| \| byte from scratch \| 9114 \| 2061 \| 4.42 \| 9334 \| 5133 \| 1.82 \| \| \| 0/0 \| 2566 \| 1726 \| 1.49 \| \| native from scratch \| 13481 \| 3967 \| 3.40 \| 12291 \| 7608 \| 1.62 \| \| \| 0/0 \| 3003 \| 2100 \| 1.43 \| \| byte after native \| 3467 \| 1476 \| 2.35 \| 5067 \| 3912 \| 1.30 \| \| \| 0/0 \| 971 \| 801 \| 1.21 \| #+TBLFM: $4=$2/$3;f2::$7=$5/$6;f2::$10=$9/$8;f2::$13=$11/$12;f2 ``` Menu: 1. Write a jbuild file, autogenerated from jbuild.in because we need to fill in some information at build-time (really, at configure time, but TODO), such as whether or not clang is enabled. 2. Nuke lots of stuff from infer/src/Makefile that is now in the jbuild file 3. The jbuild file lives in infer/src/ so it can see all the sources. If we put it somewhere else, eg, infer/, then `jbuilder` scans too many files (all irrelevant) and takes 2.5s to start instead of .8s. Adding irrelevant directories to jbuild-ignore does not help. 4. jbuilder does not support subdirectories, so resort to listing all the source files in the generated jbuild (only source directories need to be manually listed in jbuild.in though). Still, the generated .merlin is wrong and makes merlin find source files in _build, so manually tune it to get good merlin support. We also lose some of merlin for unit tests as it cannot see their build artefacts anymore. 5. checkCopyright gets its own jbuild because it's standalone. Also, remove some deprecation warnings in checkCopyright due to the new version of Core from a while ago. 6. Drop less-used Makefile features (they had regressed anyway) such as building individual modules. Also, building mod_dep.pdf now takes all the source files available so they better build (before, it would only take the source files from the config, eg with or without clang) (that's pretty minor). 7. The toplevel is now built as a custom toplevel because that was easier. It should soon be even easier: https://github.com/janestreet/jbuilder/issues/210 8. Move BUILTINS.mli to BUILTINS.ml because jbuilder is not happy about interface files without implementations. In particular, I did not try to migrate too much of the Makefile logic to jbuilder, more can be done in the future. Reviewed By: jberdine Differential Revision: D5573661 fbshipit-source-id: 4ca6d8f 7 years ago			`open InferModules;;`