| Age | Commit message (Collapse) | Author |
|---|
|
Fix #11452
|
|
if the .vos file is empty, rename -quick to -vio, dump empty .vos when producing .vio, dump empty .vos and .vok files when producing .vo from .vio.
|
|
Ack-by: Zimmi48
|
|
Update doc_grammar tool
The grammar in the doc is generated semi-automatically with doc_grammar:
- the grammar is automatically extracted from the mlg files
- developer-prepared editing scripts *.mlg_edit modify the extracted
grammar for clarity, simplicity and ordering of productions
- chunks of the resulting grammar are automatically inserted into the
rsts using instructions embedded in the rsts
Running doc_grammar is currently a manual step.
The grammar updates in the rst files have been manually reviewed.
|
|
This fixes dune. TBH the problem is that dune is too strict, but we
can't go back in time to change it.
|
|
|
|
Flag -fexcess-precision=standard is not enough on x86_32
where -msse2 -mfpmath=sse is required (-msse is not enough)
to avoid double rounding issues in the VM.
Most floating-point operation are now implemented in C because OCaml
is suffering double rounding issues on x86_32 with 80 bits extended
precision registers used for floating-point values, causing double
rounding making floating-point arithmetic incorrect with respect to
its specification.
Add a runtime test for double roundings.
|
|
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
|
|
- Specialised hash and equality functions.
Avoid collisions in extreme scenarios.
- Flags to disable the use of the caches.
fixes #10772
|
|
|
|
|
|
- remove the architecture component (we don't do anything
arch-specific so it was just a rewording of int_size)
- have configure tell the make build system about int_size instead of
reimplementing cp
As a bonus, add the copyright header to uint63.mli.
|
|
and inserting it into the .rst files
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
Reviewed-by: vbgl
|
|
|
|
This seems more robust and avoids having another implementation of
`cp`.
|
|
Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.
Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
|
|
Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and
kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program
rather than a pipeline of sed and awk text processing.
|
|
The `-boot` option was used to:
- suppress loading of the rc_file
- allow to save modules with prefix `Coq`
There is no good reason disable saving of modules with `Coq` prefix by
default, thus we remove this option.
Fixes: #9575
|
|
In passing add -coqlib to coqchk's usage message.
|
|
Instead, if the coqlib is special, we set it explicitly in the command
line, as Dune does.
This is a continuation of #9523.
In Sphinx, we stop using -boot, and pass `-coqlib` through the
environment instead.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
- default targets don't depend on ocamlopt when it's unavailable
- coqc.byte is built by byte target and coqc by coqbinaries target
- unit tests use best ocaml
- poly-capture-global-univs tests ml compilation with ocamlc
- don't try to install .cmx and native-compute .o files
cf https://github.com/coq/coq/issues/9464
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
We make `coqc` a truly standalone binary, whereas `coqtop` is
restricted to interactive use.
Thus, `coqtop -compile` will emit a warning and call `coqc`.
We have also refactored `Coqargs` into a common `Coqargs` module and a
compilation-specific module `Coqcargs`.
This solves problems related to `coqc` having its own argument
parsing, and reduces the number of strange argument combinations a
lot.
|
|
This PR deprecates the use of `coqtop` as a compiler.
There is no point on having two binaries with the same purpose; after
the experiment in #8690, IMHO we have a lot to gain in terms of code
organization by splitting the compiler and the interactive binary.
We adapt the documentation and adapt the test-suite.
Note that we don't make `coqc` a true binary yet, but here we take
care only of the user-facing part.
The conversion of the binary will take place in #8690 and will bring
code simplification, including a unified handling of arguments.
|
|
|
|
The variable QUICK enables the quick compilation chain:
- all v files are compiled with -quick to vio files (also
-native-compiler no, since it is quicker)
- then all vio files are turned to vo files $NJOBS at a time
All occurrences of .vo use now .$(VO) that can be either
.vo or .vio depending of QUICK being defined. Targets that
only make sense for .vo files have to use $(VAR:.$(VO)=.vo)
|
|
|
|
This was introduced in PR #8985.
|
|
|
|
It's a bit cleaner this way, especially wrt the number of toplevel directories.
Also fix warning about undefined GRAMMARCMA while we're at it.
|
|
|
|
|
|
|
|
Now that the checker shares code with the kernel using md5 cic.mli
doesn't work. We could md5 declarations.ml but this would miss changes
to constr (and cic.mli already missed changes to names, univs).
Instead we just print a bit of information (the last seen type
name/annotation) when validate fails. This should help debugging when
forgetting to update values.ml without the full verbosity of -debug.
As such there is no need to -debug in the makefile validate
target (NB: CI has an independent implementation of the validate rule
since the vos are installed there).
|
|
This makes the make-based build system stop linking to Camlp5's
gramlib and instead links to our own gramlib.
We use the style done in the packing of `Stdlib` in OCaml 4.07.
As to introduce a minimal amount of noise in history we use an
autogenerated `gramlib__pack` directory.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.
With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.
We also rename some files from the checker so that they don't clash with
kernel files.
|
|
|
|
We make `config` into a properly library. This is more uniform and
useful for some clients. This also matches what was done in Dune.
Next step would be to push dependencies on `Coq_config` upwards, only
the actual toplevel binaries should depend on it.
We also remove the stale `camlp5.dbg` and refactor the dbg files a
bit, isolating the bits that are specific to the plugin / lib building
method used by makefile.
|
|
Since the removal of the dependency in camlp5 for CLexer, it looks like this
file was never generated, leading to installation failure. We add it as a
dependency of the install step.
|
|
|
|
Even if `fake_ide` was under tools, it depended on libraries from
`ide`. Thus, we move `fake_ide` to `ide`, and make it "private" to the
test-suite [this means `test-suite` depends on the `ide` folder then].
In the Dune side, we reorganize libraries so `fake_ide` doesn't depend
on GTK anymore, this allows to run the test-suite when GTK is not
available.
In order to achieve this, we had to split the `coqide` package in a
server and client version.
|
