| Age | Commit message (Collapse) | Author |
|---|
|
|
|
That release includes non trivial changes related C compilers, in
particular due to `-fno-common` support.
|
|
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.
|
|
|
|
|
|
The changes are large due to `Pervasives` deprecation:
- the `Pervasives` module has been deprecated in favor of `Stdlib`, we
have opted for introducing a few wrapping functions in `Util` and
just unqualified the rest of occurrences. We avoid the shims as in
the previous attempt.
- a bug regarding partial application have been fixed.
- some formatting functions have been deprecated, but previous
versions don't include a replacement, thus the warning has been
disabled.
We may want to clean up things a bit more, in particular
w.r.t. modules once we can move to OCaml 4.07 as the minimum required
version.
Note that there is a clash between 4.08.0 modules `Option` and `Int`
and Coq's ones. It is not clear if we should resolve that clash or
not, see PR #10469 for more discussion.
On the good side, OCaml 4.08.0 does provide a few interesting
functionalities, including nice new warnings useful for devs.
|
|
Also update CAMLP5_VER_EDGE: 7.06 → 7.06.10-g84ce6cc4
This is to avoid an OCaml bug that occurs when compiling the OCaml code
extracted from part of a patched version of CompCert.
~~~
File "extraction/Parser.ml", line 12375, characters 19-29:
Error: Constraints are not satisfied in this type.
Type initstate' should be an instance of initstate'
~~~
This compiler issue only appears with OCaml 4.07.0 (neither with 4.06
nor with 4.07.1); hence this update.
|
|
We need to update in Docker:
- dune to 1.4.0: as it honors `-p` on test stanzas
- dune-release to 1.1.0: support for OPAM 2.0 + fixes
This makes `dune-release distrib` / `dune-release opam pkg` work.
TODO: we need to figure out what is going on with the
versioning. Should we do `dune subst` on `pinned`?
|
|
This satisfies a wish by @ppedrot
|
|
I forgot to update `.PHONY` and to put the proper flags in the new
workspace file.
|
|
|
