GitLab

Generate artifacts with dx and all of its dependencies

Switch from `Elpi Debug "VERBOSE_INFO"` to an attribut `#[verbose]` to
enable a verbose trace of the GenerateIntermediateRepresentation command
(`Elpi Debug` must now all be set before the code that rely on it so it
is no longer useful to enable verbosity in code using dx)

configure normally picks up the build directory for the coq-compcert
opam package as the default value form compcertdir
`opam var coq-compcert:build` returns sometimes (since opam 2.1?) an
empty result when called in configure, so set the directory explicitly
on the command line

CompCert must be installed where Coq will find it even when setting the
option --compcertdir

Give the example of the coq-compcert-32 package

Unfortunately, this breaks support for previous versions

Since .h files are meant to be included anyway, we might as well
generate include guards in all cases

Since the dependency is between generated files, it would be tricky to
use ocamldep on the fly, so use a static dependency

Evaluating the DXModule can be quite compute intensive, on medium-sized
example the improvement of performance can be massive

Due to dropping the `const` attribute, the C code produced by the tests
changed

To declare all global variables as const puts a strong constraint on how
they must be initialised by the raw C code

Now that they are user-defined identifiers, use them for main

They are superseded by more appropriate makeDXModule specialisations

Clarify that the values are CompCert identifiers, not any positive

Change the mapping to leave odd numbers for user-defined identifiers

resolveId should always succeed. If the identifier cannot be found, this
is a global error

Generate an error instead of a warning for names using characters
besides [a-zA-Z0-9_]
Drop the variable name for the second argument since it’s not used in
that error case

Since coq 8.14, coqdep no longer supports the "-w" option so use a
different variable for coqc and coqdep options

Commit "Ensure names (as strings) are all unique" changed the output C
code: modify the test results accordingly

With a Definition, the Elpi code to recognize the primitive (since we
do not want to trigger evaluation during the conversion)

Avoid boilerplate of checking that constants are not given arguments