diff options
Diffstat (limited to 'dev/doc/critical-bugs')
| -rw-r--r-- | dev/doc/critical-bugs | 37 |
1 files changed, 35 insertions, 2 deletions
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 01c2b574a2..0631b3ad59 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -112,13 +112,35 @@ Universes component: universe polymorphism summary: universe polymorphism can capture global universes impacted released versions: V8.5 to V8.8 - impacted coqchk versions: V8.5 to current (NOT FIXED) - fixed in: 2385b5c1ef + impacted coqchk versions: V8.5 to V8.9 + fixed in: ec4aa4971f (58e1d0f200 for the checker) found by: Gaëtan Gilbert exploit: test-suite/misc/poly-capture-global-univs GH issue number: #8341 risk: unlikely to be activated by chance (requires a plugin) + component: template polymorphism + summary: template polymorphism not collecting side constrains on the universe level of a parameter; this is a general form of the previous issue about template polymorphism exploiting other ways to generate untracked constraints introduced: morally at the introduction of template polymorphism, 23 May 2006, 9c2d70b, r8845, Herbelin impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3, V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found there yet (an exploit using a plugin to force sharing of universe level is in principle possible though) + impacted development branches: all from 8.4 to 8.9 at the time of writing and suspectingly also all from 8.1 to 8.4 if a way to create untracked constraints can be found + impacted coqchk versions: a priori all (tested with V8.4 and V8.9 which accept the exploit) + fixed in: soon in master and V8.10.0 (PR #9918, Aug 2019, Dénès and Sozeau) + found by: Gilbert using explicit sharing of universes, exploit found for 8.5-8.9 by Pédrot, other variants generating sharing using sections, or using ltac tricks by Sozeau, exploit in 8.4 by Herbelin and Jason Gross by adding new tricks to Sozeau's variants + exploit: test-suite/failure/Template.v + GH issue number: #9294 + risk: moderate risk to be activated by chance + + component: universe polymorphism, asynchronous proofs + summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section + introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one + impacted released: V8.5-V8.10 + impacted development branches: none + impacted coqchk versions: immune + fixed in: PR#10664 + found by: Pédrot + exploit: no test + GH issue number: none + risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc) + Primitive projections component: primitive projections, guard condition @@ -228,6 +250,17 @@ Conversion machines exploit: test-suite/bugs/closed/bug_9684.v GH issue number: #9684 + component: lazy machine + summary: incorrect De Bruijn handling when inferring the relevance mark for a lambda + introduced: 2019-03-15, 23f84f37c674a07e925925b7e0d50d7ee8414093 and 71b9ad8526155020c8451dd326a52e391a9a8585, SkySkimmer + impacted released versions: 8.10.0 + impacted coqchk versions: 8.10.0 + found by: ppedrot investigating unexpected conversion failures with SProp + exploit: test-suite/bugs/closed/bug_10904.v + GH issue number: #10904 + risk: none without using -allow-sprop (off by default in 8.10.0), + otherwise could be exploited by mistake + Conflicts with axioms in library component: library of real numbers |