| Age | Commit message (Collapse) | Author |
|---|
|
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
|
|
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
|
|
|
|
See CEP#44 for futher details.
|
|
There were single quotes which were not interpreted in "PATH" syntax.
|
|
|
|
Recent OCaml don't allow to build the VM with `--std=c99` anymore due
to changes in header files. `gnu99` is required, but it turns out this
is already enforced by OCaml, so we just remove the flag altogether.
See the discussion in #11432
|
|
Compile buffer, and with building from a path containing spaces.
Updated CHANGES.md
Now using Filename.quote instead of enclosing in single quotes.
Fixed rebasing problems.
|
|
Use -std=c99 instead of the GCC argument -fexcess-precision=standard
This requires the -fasm as the VM is using the asm GNU extension
(also implemented by other compilers).
These flags should be more portable accross C compilers.
|
|
in order to make builds reproducible.
See https://reproducible-builds.org/ for why this is good
and https://reproducible-builds.org/specs/source-date-epoch/
for the definition of this variable.
Fixes #11037
|
|
|
|
|
|
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.
|
