<commit_before>.. _utilities:

---------------------
 Utilities
---------------------

The distribution provides utilities to simplify some tedious works
beside proof development, tactics writing or documentation.


Using Coq as a library
----------------------

In previous versions, ``coqmktop`` was used to build custom
toplevels - for example for better debugging or custom static
linking. Nowadays, the preferred method is to use ``ocamlfind``.

The most basic custom toplevel is built using:

::

   % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \
                 -package coq.toplevel \
                  toplevel/coqtop\_bin.ml -o my\_toplevel.native


For example, to statically link |L_tac|, you can just do:

::

   % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \
                 -package coq.toplevel -package coq.ltac \
                 toplevel/coqtop\_bin.ml -o my\_toplevel.native

and similarly for other plugins.


Building a |Coq| project with coq_makefile
------------------------------------------
<commit_msg>[doc] Nits on utilities / toplevel building.<commit_after>.. _utilities:

---------------------
 Utilities
---------------------

The distribution provides utilities to simplify some tedious works
beside proof development, tactics writing or documentation.


Using Coq as a library
----------------------

In previous versions, ``coqmktop`` was used to build custom
toplevels - for example for better debugging or custom static
linking. Nowadays, the preferred method is to use ``ocamlfind``.

The most basic custom toplevel is built using:

::

   % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \
                 -package coq.toplevel \
                 topbin/coqtop_bin.ml -o my_toplevel.native


For example, to statically link |Ltac|, you can just do:

::

   % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \
                 -package coq.toplevel,coq.plugins.ltac \
                 topbin/coqtop_bin.ml -o my_toplevel.native

and similarly for other plugins.


Building a |Coq| project with coq_makefile
------------------------------------------

{'fraction_non_alphanumeric': 0.1619718309859155, 'fraction_numerical': 0.0, 'mean_word_length': 2.0269886363636362, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3734532', 'n_tokens_mistral': 610, 'n_tokens_neox': 586, 'n_words': 211}