| Age | Commit message (Collapse) | Author |
|---|
|
than our own.
Ack-by: aaronpuchert
Ack-by: gadmm
Reviewed-by: maximedenes
Ack-by: ppedrot
Reviewed-by: proux01
|
|
Add headers to a few files which were missing them.
|
|
This commit also prefixes young_ptr and young_limit along the way, so as
to not rely on OCaml's compatibility layer. This is a gratuitous change,
since this code is only meant to be compiled with OCaml < 4.10 anyway.
|
|
We cannot use caml_alloc_small because the macros Setup_for_gc and
Restore_after_gc are still relevant (and critical). This means defining
the CAML_INTERNALS macro, but it is a legit use and actually documented
in the OCaml manual.
This will help with forward compatibility with OCaml compilers, e.g.,
issue #10603. Unfortunately, it also means that we can no longer use #9914
to prevent memory corruption.
The old macro is still used for OCaml versions prior to 4.10, as the
upstream macro might process Ctrl+C when it is called.
|
|
|
|
|
|
Issue #10603
|
|
|
|
This is a follow up of #11010 ; I've realized that for example in #11123
a large part of the patch is detabification as indeed the files are
mixed in tabs/space style so developers are forced to do the cleanup
each time they work on them.
Command used:
```
for i in `find . -name '*.c' -or -name '*.h'; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
Checked empty diff with `git diff --ignore-all-space`
|
|
This is the minimal set of changes requires for Coq to build under 2.0
mode. We may likely take advantage of some more new features.
Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune
in older versions as it will install a secondary compiler.
|
|
|
|
|
|
* Fix the implementations and add tests
* Change shift from int63 to Z (was always used as a Z)
* Update FloatLemmas.v accordingly
Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
|
|
* Add a related test-suite in compare.v (generated by a bash script)
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
|
|
|
|
is_float was relying on Obj.tag triggering a check that we are in the
OCaml heap which is expensive. On extreme examples, this can lead to a
global 2x speedup.
Thanks to Maxime Dénès and Jacques-Henri Jourdan for their help in
diagnosing this.
|
|
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.
|
|
|
|
|
|
Replace `option comparison` with `float_comparison` (:= `FEq | FLt |
FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid
boxing and an extra match when using primitive float comparison.
|
|
Axioms on ldexp and frexp are replaced by proofs inside FloatLemmas.
The shift value has been increased to 2 * emax + prec because in ldexp
we want to be able to transform the smallest denormalized to the biggest
float value in one call.
|
|
* This commit add float instructions to the VM, their encoding in bytecode
and the interpretation of primitive float values after the reduction.
* The flag '-std=c99' could be added to the C compiler flags to ensure
that float computation strictly follows the norm (ie. i387 80-bits
format is not used as an optimization).
Actually, we use '-fexcess-precision=standard' instead of '-std=c99'
because the latter would disable GNU asm used in the VM.
|
|
All the implementations now return (0, 0) when the dividend is so large
that the quotient would overflow.
|
|
|
|
|
|
Reviewed-by: maximedenes
|
|
|
|
There are three implementations of this primitive:
* one in OCaml on 63 bits integer in kernel/uint63_amd64.ml
* one in OCaml on Int64 in kernel/uint63_x86.ml
* one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h
Its specification is the axiom `diveucl_21_spec` in
theories/Numbers/Cyclic/Int63/Int63.v
* comment the implementations with loop invariants to enable an easy
pen&paper proof of correctness (note to reviewers: the one in
uint63_amd64.ml might be the easiest to read)
* make sure the three implementations are equivalent
* fix the specification in Int63.v
(only the lowest part of the result is actually returned)
* make a little optimisation in div21 enabled by the proof of correctness
(cmp is computed at the end of the first loop rather than at the beginning,
potentially saving one loop iteration while remaining correct)
* update the proofs in Int63.v and Cyclic63.v to take into account the
new specifiation of div21
* add a test
|
|
Backport
https://github.com/ocaml/ocaml/commit/71b94fa3e8d73c40e298409fa5fd6501383d38a6
and
https://github.com/ocaml/ocaml/commit/d3e86fdfcc8f40a99380303f16f9b782233e047e
from OCaml VM
|
|
Backport
https://github.com/ocaml/ocaml/commit/c6ce97fe26e149d43ee2cf71ca821a4592ce1785
from OCaml VM
|
|
Backport
https://github.com/ocaml/ocaml/commit/eb1922c6ab88e832e39ba3972fab619081061928
from OCaml VM
|
|
Backport
https://github.com/ocaml/ocaml/commit/055d5c0379e42b4f561cb1fc5159659d8e9a7b6f
from OCaml VM
|
|
Backport
https://github.com/ocaml/ocaml/commit/bc333918980b97a2c81031ec33e72a417f854376
from OCaml VM
|
|
Protect accu and coq_env against GC calls in the VM when calling
primitive integer functions on 32 bits architecture.
|
|
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.
|
|
In order for Dune to work in Windows we need to tweak some script
calls, they need a POSIX shell and the `(run ...)` / `(system ...)`
actions use `cmd.exe` on Windows.
Hopefully, we will rely less on `bash` when Dune can understand Coq
libraries. This affects shell scripts in `kernel/**.sh` for example.
It is interesting to see how faster the Coq Windows build is with Dune
+ Windows.
There are some problems with PATHs that prevent the test suite from
working, these will be fixed in a future PR.
|
|
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>
|
|
[Dune](https://github.com/ocaml/dune) is a compositional declarative
build system for OCaml. It provides automatic generation of
`version.ml`, `.merlin`, `META`, `opam`, API documentation; install
management; easy integration with external libraries, test runners,
and modular builds.
In particular, Dune uniformly handles components regardless whether
they live in, or out-of-tree. This greatly simplifies cases where a
plugin [or CoqIde] is checked out in the current working copy but then
distributed separately [and vice-versa]. Dune can thus be used as a
more flexible `coq_makefile` replacement.
For now we provide experimental support for a Dune build. In order to
build Coq + the standard library with Dune type:
```
$ make -f Makefile.dune world
```
This PR includes a preliminary, developer-only preview of Dune for
Coq. There is still ongoing work, see
https://github.com/coq/coq/issues/8052 for tracking status towards
full support.
## Technical description.
Dune works out of the box with Coq, once we have fixed some modularity
issues. The main remaining challenge was to support `.vo` files.
As Dune doesn't support custom build rules yet, to properly build
`.vo` files we provide a small helper script `tools/coq_dune.ml`. The
script will scan the Coq library directories and generate the
corresponding rules for `.v -> .vo` and `.ml4 -> .ml` builds. The
script uses `coqdep` as to correctly output the dependencies of
`.v` files. `coq_dune` is akin to `coq_makefile` and should be able to
be used to build Coq projects in the future.
Due to this pitfall, the build process has to proceed in three stages:
1) build `coqdep` and `coq_dune`; 2) generate `dune` files for
`theories` and `plugins`; 3) perform a regular build with all
targets are in scope.
## FAQ
### Why Dune?
Coq has a moderately complex build system and it is not a secret that
many developer-hours have been spent fighting with `make`.
In particular, the current `make`-based system does offer poor support
to verify that the current build rules and variables are coherent, and
requires significant manual, error-prone. Many variables must be
passed by hand, duplicated, etc... Additionally, our make system
offers poor integration with now standard OCaml ecosystem tools such
as `opam`, `ocamlfind` or `odoc`. Another critical point is build
compositionality. Coq is rich in 3rd party contributions, and a big
shortcoming of the current make system is that it cannot be used to
build these projects; requiring us to maintain a custom tool,
`coq_makefile`, with the corresponding cost.
In the past, there has been some efforts to migrate Coq to more
specialized build systems, however these stalled due to a variety of
reasons. Dune, is a declarative, OCaml-specific build tool that is on
the path to become the standard build system for the OCaml ecosystem.
Dune seems to be a good fit for Coq well: it is well-supported, fast,
compositional, and designed for large projects.
### Does Dune replace the make-based build system?
The current, make-based build system is unmodified by this PR and kept
as the default option. However, Dune has the potential
### Is this PR complete? What does it provide?
This PR is ready for developer preview and feedback. The build system
is functional, however, more work is necessary in order to make Dune
the default for Coq.
The main TODOs are tracked at https://github.com/coq/coq/issues/8052
This PR allows developers to use most of the features of Dune today:
- Modular organization of the codebase; each component is built only
against declared dependencies so components are checked for
containment more strictly.
- Hygienic builds; Dune places all artifacts under `_build`.
- Automatic generation of `.install` files, simplified OPAM workflow.
- `utop` support, `-opaque` in developer mode, etc...
- `ml4` files are handled using `coqp5`, a native-code customized
camlp5 executable which brings much faster `ml4 -> ml` processing.
### What dependencies does Dune require?
Dune doesn't depend on any 3rd party package other than the OCaml compiler.
### Some Benchs:
```
$ /usr/bin/time make DUNEOPT="-j 1000" -f Makefile.dune states
59.50user 18.81system 0:29.83elapsed 262%CPU (0avgtext+0avgdata 302996maxresident)k
0inputs+646632outputs (0major+4893811minor)pagefaults 0swaps
$ /usr/bin/time sh -c "./configure -local -native-compiler no && make -j states"
88.21user 23.65system 0:32.96elapsed 339%CPU (0avgtext+0avgdata 304992maxresident)k
0inputs+1051680outputs (0major+5300680minor)pagefaults 0swaps
```
|
|
|
|
The Coq VM stack is scanned by the OCaml GC, but it can contain raw pointers
to C-allocated strings standing for VM bytecode. If the the no-naked-pointers
option is set, we perform the check that a stack value lives on the OCaml heap
ourselves.
|
|
We allocate an additional header so that the accumulator is not a naked
pointer. Indeed, it is contained in accumulator blocks which are scanned by
the GC as their tags is 0.
|
|
This prevents the existence of a few naked pointers to C heap from the OCaml
heap. VM bytecode is represented as any block of size at least 1 whose first
field points to a C-allocated string.
This representation is compatible with the Coq VM representation of
(potentially recursive) closures, which are already specifically tailored
in the OCaml GC to be able to contain out-of-heap data.
|
|
|
|
|
|
cofixpoint (bug #5286).
|
|
This was yet another bug in the VM long multiplication, that
I unfortunately introduced in ebc509ed2. It was impacting only 32-bit
architectures.
In the future, I'll try to make sure that
1) we provide unit tests for integer arithmetic (my int63 branch ships
with such tests)
2) our continuous testing infrastructure runs the test suite on a 32-bit
architecture. I tried to set up such an instance, but failed. Waiting
for support reply.
|
|
If the result had its 30th bit set, then all the high part of the result
on a 64-bit architecture would end up being set, thus breaking subsequent
computations.
This patch also fixes the incorrectly parenthesized definition of
uint32_of_value, which by luck was never misused.
|
|
|
|
The bytecode interpreter ensures that the stack space available at some
points is above a static threshold. However, arbitrary large stack space
can be needed between two check points, leading to segmentation faults
in some cases.
We track the use of stack space at compilation time and add
an instruction to ensure greater stack capacity when required. This is
inspired from OCaml's PR#339 and PR#7168.
Patch written with Benjamin Grégoire.
|
|
|
