| Age | Commit message (Collapse) | Author |
|---|
|
This removes the need for the remote counter.
|
|
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: gares
Ack-by: herbelin
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
|
|
Contrarily to the comments, Coq_config.date was not the "release date" but
just another "compile date".
|
|
Reviewed-by: SkySkimmer
|
|
We expose the representation function in UGraph and change the printer
signature to work over the representation instead of the abstract type.
Similarly, the topological sorting algorithm is moved to Vernacentries.
It is now even simpler.
|
|
|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
|
|
|
Instead we store that data in the native code that was generated in adapt
the compilation scheme accordingly. Less indirections and less imperative
tinkering makes the code safer.
The global symbol table was originally introduced in #10359 as a way not to
depend on the Global module in the generated code. By storing all the
native-related information in the cmxs file itself, this PR also makes other
changes easier, such as e.g. #13287.
|
|
This allows to quickly spot the parts of the code that rely on the canonical
ordering. When possible we directly introduce the quotient-aware versions.
|
|
Fixes #12845 (coqchk reports names from inner modules of opaque modules
as axioms)
I don't fully understand the code here, so I can't speak as to its
correctness, but it should be simple enough that reviewers can
understand what it's doing and whether or not it's correct.
This is useful for me in making progress towards
https://github.com/mit-plv/fiat-crypto/issues/736
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
Ack-by: proux01
Ack-by: silene
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
Instead of considering all constants without body in the environment,
consider only the ones appearing in the body of the opacified constant.
|
|
When encountering
```Coq
Module M : T.
...
Lemma c :...
...
Qed.
...
End M.
```
every field `c` without body in `T` but with a body in `M` is
registered as opacified in a table along with all constants
`opacified(c)` without body in the environment at this point (i.e.,
all axioms potentially used by c).
Then, when printing axioms, if `c` appears in the final environment it
is replaced by `opacified(c)` in the resulting list of axioms.
|
|
|
|
We tweak the message a bit.
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
See CEP#44 for futher details.
|
|
|
|
|
|
|
|
|
|
|
|
Add headers to a few files which were missing them.
|
|
|
|
This could have been at the root of strange behaviours (read unsoundness).
|
|
For an inductive block to be template, all its components must also
be. This is probably fixing a few soundness bugs in the process, but I
do not want to think too much about it.
|
|
|
|
data from a part where it should never access it.
|
|
This was the only part in the kernel that really relied on the contents
of the Monomorphic node.
|
|
And enable related test.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
|
|
preparation for direct discharge
|
|
representation.
Reviewed-by: maximedenes
|
|
It gets thrown away if the inductive is declared in a section anyway,
and there is no user syntax to specify it.
|
|
dune-dbg depends on coqchk.bc and coqide_main.bc, and apparently they
now need explicit modes to be produced.
|
