This seems the official name, the byterun name is just an artifact
from the very preliminary dune build.

This makes it possible to skip the check when scanning the stack for the
garbage collector.

We introduce a new package structure for Coq:

- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`

This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.

The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.

Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.

There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.

This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.

IMHO the plan should work fine.

Signed primitive integers defined on top of the existing unsigned ones
with two's complement.

The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.

Additions to the kernel:
  les (signed <=), lts (signed <), compares (signed compare),
  divs (signed division), rems (signed remainder),
  asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)

The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).

A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.

Reviewed-by: gasche
Ack-by: ppedrot
Reviewed-by: xavierleroy

This avoids forgetting to add opcodes to coq_fix_code.c, and thus prevents
arities being mistakenly set to zero.

Since the compiler initializes the arities to zero, coq_tcode_of_code
wrongly believes that the word following a primitive operation contains
an opcode, while it is the global index of the primitive operation. So,
the function will try to translate it and thus corrupt it. But as long as
the evaluated term fully reduces (which is always the case for
CoqInterval), the corrupted word will never be read.

At this point, it all depends on the arity of the global index (seen as
an opcode). If it is zero, then coq_tcode_of_code will recover and
correctly translate the following opcodes. If it is nonzero, then the
function starts translating random words, possibly corrupting the memory
past the end of the translation buffer. Independently of this memory
corruption, coq_interprete will execute random code once it gets to the
opcode following the primitive operation, since it has not been
translated.

The reason CoqInterval is not always crashing due to this bug is just
plain luck. Indeed, the arity of the pseudo opcode only depends on the
global index of the primitive operations. So, as long as this arity is
zero, the memory corruption is fully contained. This happens in the vast
majority of cases, since coq_tcode_of_code translates any unrecognized
opcode to STOP, which has arity zero.

This bug is exploitable.

MAKEPROD is just MAKEBLOCK2(0), but one word shorter. Since this opcode is
never encountered in the fast path, this optimization is not worth the
extra complexity.