diff options
Diffstat (limited to 'dev/doc/critical-bugs')
| -rw-r--r-- | dev/doc/critical-bugs | 27 |
1 files changed, 26 insertions, 1 deletions
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 67becb251a..3260040248 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -158,7 +158,7 @@ Universes 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 released versions: V8.5-V8.10 impacted development branches: none impacted coqchk versions: immune fixed in: PR#10664 @@ -167,6 +167,19 @@ Universes GH issue number: none risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc) + component: algebraic universes + summary: Set+2 was incorrectly simplified to Set+1 + introduced: V8.10 (with the SProp commit 75508769762372043387c67a9abe94e8f940e80a) + impacted released versions: V8.10.0 V8.10.1 V8.10.2 + impacted coqchk versions: same + fixed in: PR#11422 + found by: Gilbert + exploit: see PR (custom application of Hurkens to get around the refreshing at elaboration) + GH issue number: see PR + risk: unlikely to be triggered through the vernacular (the system "refreshes" algebraic + universes such that +2 increments do not appear), mild risk from plugins which manipulate + algebraic universes. + Primitive projections component: primitive projections, guard condition @@ -255,6 +268,18 @@ Conversion machines GH issue number: #9925 risk: + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: broken long multiplication primitive integer emulation layer on 32 bits + introduced: e43b176 + impacted released versions: 8.10.0, 8.10.1, 8.10.2 + impacted development branches: 8.11 + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: 4e176a7 + found by: Soegtrop, Melquiond + exploit: test-suite/bugs/closed/bug_11321.v + GH issue number: #11321 + risk: critical, as any BigN computation on 32-bit architectures is wrong + component: "native" conversion machine (translation to OCaml which compiles to native code) summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False introduced: V8.5 |