| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
|
|
|
|
|
|
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
|
|
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.
|
|
* 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.
|
|
|
|
|
|
|
|
- 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.
|
|
|
|
Use it to not include unreleased changes when building a released
version.
|
|
- Update Docker images to install compatible version of lablgtk3
- We remove unnecesary variables from configure.
- We fix path detection of GTK libs in makefile
|
|
|
|
fields are given.
|
|
The regular make build uses a non-standard header path for their files
[as a way to workaround the ugliness of the non-hygienic build]
This breaks in Dune as it uses the regular object file pack, so
`coq_makefile` won't find it. We cherry pick a change from #8729 which
fixes the updated version of bug #9735 , even tho `coq_makefile`
should stop relying on hardcoded paths and use findlib instead.
Closes #9735
|
|
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.
|
|
|
|
comments.
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
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.
|
|
|
|
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>
|
|
These directories don't contain Coq sources but internal developer
files. This can create problems, for example, in #8919.
|
|
This reverts commit c4880effb91fab55c250a799cbceac9b04681db0, reversing
changes made to 65927c22bcad62e1bc9a28a57377d82eba215a2d.
|
|
This is the first release that contains the type-safe grammar API.
|
|
The kernel no longer has to read the configure flag, its value can now
be overriden by a coqtop/coqc argument, and more generally is easier to
set from a toplevel (such as the checker).
We also add a `-bytecode-compiler` flag.
Fixes #4607
|
|
|
|
Fixes #8621
|
|
|
|
|
|
These are unused and not likely to come back.
|
|
Fix silly typo that created havoc in developer out-of-the-box setups.
|
|
In order to support sending the OPAM prefix to configure via Dune, we
introduced a `COQ_CONFIGURE_PREFIX` variable.
However, this had the pitfall that now the developer had to set it or
else face a hanging build due to configure expecting user input.
While we wait for a larger cleanup in `-prefix`, we introduce a
`no-ask` option in `./configure` that will avoid this problem. If
`-no-ask` is passed to `configure` no interactive question or display
will be shown to the user.
|
|
Dune calls `./configure` under the build sandbox, which, if the voboot
target has not been executed will contain only the OCaml parts of Coq.
Thus, we make configure not to die if the `plugins` directory is not
present.
This makes Dune usable without calling the `voboot` target.
|
|
Closes #7380. Ubuntu 18.04 and Debian Buster will ship this OCaml
version so it makes sense we bump our dependency to 4.05.0 as we can
use some newer compiler features.
|
|
After #8043 was fixed we can come back to a stricter warning profile
for flambda.
|
|
This is a hack to enable correct OPAM building, the medium-term plan
is to avoid having to set a prefix at configure time but instead using
a set of rules to locate the Coq library.
We use `(env_var ...)` in a dependency rule, which a feature of Dune 1.2
|
|
|
|
|
|
Fixes #8067. This is becoming the default in many developments, so it
makes sense to require it too, both for Coq and for Plugins.
|
|
We turn all Coq warnings that are on by default into errors.
|
|
See https://github.com/ocaml/num/issues/9
|
|
flambda happy.
See issue #8043.
Using `[@@@ocaml.warning "-59"]` to disable this fails, it seems like
an OCaml bug.
|
|
They are not used anymore.
People should use Proof-General (and optionally Company-Coq) instead.
|
|
|
|
|
