| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: jfehrle
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: gares
|
|
|
|
Fixes #9532
Fixes #9490
|
|
Reviewed-by: gares
|
|
representation.
Reviewed-by: maximedenes
|
|
This change improves the relaxed ambiguous path condition of coercions (#9743)
to check that any circular inheritance path of `C >-> C` is definitionally equal
to the identity function of the class `C`. Moreover, for a new inheritance path
`p : C >-> D` and existing (valid) one `q : C >-> D`, the new mechanism does not
report the ambiguity of `p` and `q` if they have a common element, that is to
say:
`p = p1 @ [c] @ p2` and `q = q1 @ [c] @ q2`
for some coercion `c` and inheritance paths `p1`, `p2`, `q1`, and `q2`.
In that case, convertibility of `p1` and `q1`, also, `p2` and `q2` should be
checked; thus, checking the ambiguity of `p` and `q` is redundant with them.
If the new mechanism does not report any ambiguous path, the inheritance graph
must be coherent [Barthe 1995, Sect. 3.2] [Saïbi 1997, Sect. 7]:
1. for any circular path `p : C >-> C`, `p` is definitionally equal to the
identity function, and
2. for any two paths `p, q : C >-> D`, `p` and `q` are convertible.
[Barthe 1995] Gilles Barthe, Implicit coercions in type systems, In: TYPES '95,
LNCS, vol 1158, Springer, 1996, pp 1-15.
[Saïbi 1997] Amokrane Saïbi, Typing algorithm in type theory with inheritance,
In: POPL '97, ACM, 1997, pp 292-301.
|
|
|
|
c.f. https://dev.azure.com/coq/coq/_build/results?buildId=6485&view=logs&jobId=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&j=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&t=77aad734-2057-5694-9ae2-ee1f5f26eae8
|
|
Apparently `expr 1 \+ 1` is fine on Linux but not cygwin/Windows, where
it fails with "syntax error". Similarly for `-` and `/`.
|
|
This reverts commit ec505a2fa67b0776b624be54417e06c6512f1734.
A better fix is coming
|
|
Apparently the bogomips produced by cygwin are extra-bogo.
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
~strict flag
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
|
|
Ack-by: ejgallego
|
|
Reviewed-by: maximedenes
|
|
|
|
|
|
For now, the API is unchanged and this commit only splits pretyping code for
each glob_constr constructor into a record field.
|
|
|
|
|
|
Issue #10603
|
|
Reviewed-by: ejgallego
|
|
|
|
non-resolvable, always
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
PR #9725 fixes completness bugs introduces some inefficiency. The
current PR intends to fix the inefficiency while retaining
completness. The fix removes a pre-processing step and instead relies
on a more elaborate proof format introducing positivity constraints on
the fly.
Solve bootstrapping issues: RMicromega <-> Rbase <-> lia.
Fixes #11063 and fixes #11242 and fixes #11270
|
|
Reviewed-by: maximedenes
|
|
Fix #11266
|
|
avoid possible "breach of privacy"
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
It gets thrown away if the inductive is declared in a section anyway,
and there is no user syntax to specify it.
|
|
take only the template_check flag instead of the whole env
|
|
We do [solve_remaining_evars all_and_fail_flags] immediately before
calling [interp_mutual_inductive_constr] so these checks are extra.
|
|
There are no users in Coq but maybe some plugin wants it so don't
completely remove it
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
|
|
This is related to and fixes #10694 in part.
When calling bootstrap in an incremental build step, we must be sure
the generated dune files are in place. In the CI, these won't be in
place, so we must bootstrap without altering the digest and trace
database coming from the artifact.
Using a separate boot step to recreate the missing `dune` files works
fine and takes just a few seconds.
|
|
Closes #10694
We modify handling of artifacts for dune builds:
- we preserve `_build/log` log as artifact for ci-builds,
- we use a tar.gz as to preserve file permissions which is necessary
in order to reuse the artifacts in an incremental build.
Dune uses this rule to digest a file:
```
Digest.generic (file_contents f, f.stats.st_perm land 0o100 (* Only take USR_X in account *))
```
Since a few releases, Gitlab CI uses `.zip` as the storage format for
artifacts, this means that files in `_build` will get the executable
bit set when they did not have it originally, making all the digest
cache to miss. This caused #10694 .
See https://gitlab.com/gitlab-org/gitlab/issues/18711
|
|
|
