On Inria's gitlab: https://gitlab.inria.fr/agueneau/coq-bigO/
Requires the Procrastination library: https://gitlab.inria.fr/agueneau/coq-procrastination
The following archive bundles the library and quick setup scripts. To use it:
make init. This will download and compile the dependencies (in particular, Coq and required libraries). Note that everything is done locally, and does not pollute the global environment. Expect this step to take some time.
. env.sh. This will populate the current shell environnement.
maketo build the bigO library and examples (located in subdirectory
The 3 first steps should only be run once. Afterwards,
. env.sh should
be run every time one wants to use the contents of the archive.