diff options
| author | Gaëtan Gilbert | 2019-11-15 15:53:48 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-26 11:28:55 +0100 |
| commit | a5d124dd7c3d43a5ead81cfac30c7d1448002d56 (patch) | |
| tree | cd208e03429266330c3076260e9b905418b6a15e /dev/doc | |
| parent | d7879b8566e48aabfdbee5c27bd4c29691352233 (diff) | |
Fix #11039: proof of False with template poly and nonlinear universes
Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.
A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.
Also fixes #10504.
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/critical-bugs | 28 |
1 files changed, 27 insertions, 1 deletions
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 0631b3ad59..67becb251a 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -120,7 +120,17 @@ Universes 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) + 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) @@ -129,6 +139,22 @@ Universes GH issue number: #9294 risk: moderate risk to be activated by chance + component: template polymorphism + summary: using the same universe in the parameters and the + constructor arguments of a template polymorphic inductive (using + named universes in modern Coq, or unification tricks in older Coq) + produces implicit equality constraints not caught by the previous + template polymorphism fix. + introduced: same as the previous template polymorphism bug, morally + from V8.1, first verified impacted version V8.5 (the universe + unification is sufficiently different in V8.4 to prevent our trick + from working) + fixed in: expected in 8.10.2, 8.11+beta, master (#11128, Nov 2019, Gilbert) + found by: Gilbert + exploit: test-suite/bugs/closed/bug_11039.v + GH issue number: #11039 + risk: moderate risk (found by investigating #10504) + 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 |