Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Text

Original von: Coq^©

HISTORY:
-------

* July 2007 (Pierre Corbineau & Lionel Elie Mamane).
  Inclusion of a build system with 3 explicit phases:
  - Makefile.stage1: ocamldep, sed, camlp4 without Coq grammar extension
  - Makefile.stage2: camlp4 with grammar.cma or q_constr.cmo
  - Makefile.stage3: coqdep (.vo)

* March 2010 (Pierre Letouzey).
  Revised build system. In particular, no more stage1,2,3 :
  - Stage3 was removed some time ago when coqdep was split into
    coqdep_boot and full coqdep.
  - Stage1,2 were replaced by brutal inclusion of all .d at the start
    of Makefile.build, without trying to guess what could be done at
    what time. Some initial inclusions hence _fail_, but "make" tries
    again later and succeed.
  - Btw, .ml4 are explicitly turned into .ml files, which stay after build.
    By default, they are in binary ast format, see READABLE_ML4 option.

* February 2014 (Pierre Letouzey).
  Another revision of the build system. We avoid relying on the awkward
  include-which-fails-but-works-finally-after-a-retry feature of gnu make.
  This was working, but was quite hard to understand. Instead, we reuse
  the idea of two explicit phases, but in a lighter way than in 2007.
  The main Makefile calls Makefile.build twice :
  - first for building grammar.cma (and q_constr.cmo), with a
    restricted set of .ml4 (see variable BUILDGRAMMAR).
  - then on the true target asked by the user.

* June 2016 (Pierre Letouzey)
  The files in grammar/ are now self-contained, we could compile
  grammar.cma (and q_constr.cmo) directly, no need for a separate
  subcall to make nor awkward include-failed-and-retry.

* February - September 2018 (Emilio Jesús Gallego Arias)

  Dune support added.

  The build setup is mostly vanilla for the OCaml part, however the
  `.v` to `.vo` compilation relies on `coq_dune` a `coqdep` wrapper
  that will generate the necessary `dune` files.

  As a developer, you should not have to deal with Dune configuration
  files on a regular basis unless adding a new library or plugin.

  The vanilla setup declares all the Coq libraries and binaries [we
  must respect proper containment/module implementation rules as to
  allow packing], and we build custom preprocessors (based on `camlp5`
  and `coqpp`) that will process the `ml4`/`mlg` files.

  This suffices to build `coqtop` and `coqide`, all that remains to
  handle is `.vo` compilation.

  To teach Dune about the `.vo`, we use a small utility `coq_dune`,
  that will generate a `dune` file for each directory in `plugins` and
  `theories`. The code is pretty straightforward and declares build
  and install rules for each `.v` straight out of `coqdep`. Thus, our
  build strategy looks like this:

  1. Use `dune` to build `coqdep` and `coq_dune`.
  2. Use `coq_dune` to generate `dune` files for each directory with `.v` files.
  3. ?
  4. Profit! [Seriously, at this point Dune has all the information to build Coq]

---------------------------------------------------------------------------

This file documents internals of the implementation of the make-based
build system. For what a Coq developer needs to know about the build
system, see build-system.txt and build-system.dune.md .

.ml4 files
----------

.ml4 are converted to .ml by camlp5. By default, they are produced
in the binary ast format understood by ocamlc/ocamlopt/ocamldep.
Pros:
- faster than parsing clear-text source file.
- no risk of editing them by mistake instead of the .ml4
- the location in the binary .ml are those of the initial .ml4,
   hence errors are properly reported in the .ml4.
Cons:
- This format may depend on your ocaml version, they should be
   cleaned if you change your build environment.
- Unreadable in case you want to inspect this generated code.
   For that, use make with the READABLE_ML4=1 option to switch to
   clear-text generated .ml.

Makefiles hierarchy
-------------------

The Makefile is separated in several files :

- Makefile: wrapper that triggers a call to Makefile.build, except for
  clean and a few other little things doable without dependency analysis.
- Makefile.common : variable definitions (mostly lists of files or
  directories)
- Makefile.build : contains compilation rules, and the "include" of dependencies
- Makefile.doc : specific rules for compiling the documentation.

FIND_SKIP_DIRS
--------------

The recommended style of using FIND_SKIP_DIRS is for example

find . $(FIND_SKIP_DIRS) '(' -name '*.example' ')' -print
find . $(FIND_SKIP_DIRS) '(' -name '*.example' -or -name '*.foo' ')' -print

1)
The parentheses even in the one-criteria case is so that if one adds
other conditions, e.g. change the first example to the second

find . $(FIND_SKIP_DIRS) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print

one is not tempted to write

find . $(FIND_SKIP_DIRS) -name '*.example' -and -not -name '*.bak.example' -print

because this will not necessarily work as expected; $(FIND_SKIP_DIRS)
ends with an -or, and how it combines with what comes later depends on
operator precedence and all that. Much safer to override it with
parentheses.

In short, it protects against the -or one doesn't see.

2)
As to the -print at the end, yes it is necessary. Here's why.

You are used to write:
find . -name '*.example'
and it works fine. But the following will not:
find . $(FIND_SKIP_DIRS) -name '*.example'
it will also list things directly matched by FIND_SKIP_DIRS
(directories we want to prune, in which we don't want to find
anything). C'est subtil... Il y a effectivement un -print implicite à
la fin, qui fait que la commande habituelle sans print fonctionne
bien, mais dès que l'on introduit d'autres commandes dans le lot (le
-prune de FIND_SKIP_DIRS), ça se corse à cause d'histoires de
parenthèses du -print implicite par rapport au parenthésage dans la
forme recommandée d'utilisation:

Si on explicite le -print et les parenthèses implicites, cela devient:

find . '(' '(' '(' -name .git -or -name debian ')' -prune ')' -or \
           '(' -name '*.example' ')'
       ')'
       -print

Le print agit TOUT ce qui précède, soit sur ce qui matche "'(' -name
.git -or -name debian ')'" ET sur ce qui matche "'(' -name '*.example' ')'".

alors qu'ajouter le print explicite change cela en

find . '(' '(' -name .git -or -name debian ')' -prune ')' -or \
       '(' '(' -name '*.example' ')' -print ')'

Le print n'agit plus que sur ce qui matche "'(' -name '*.example' ')'"

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.