diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dune.md | 8 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 10 |
2 files changed, 14 insertions, 4 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 372e40a0b7..37c6e2f619 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -52,7 +52,7 @@ order to use them, do: ``` $ make -f Makefile.dune voboot # Only once per session -$ dune exec dev/shim/coqtop-prelude +$ dune exec -- dev/shim/coqtop-prelude ``` or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets @@ -108,14 +108,14 @@ automatically. You can use `ocamldebug` with Dune; after a build, do: ``` -dune exec dev/dune-dbg /path/to/foo.v +dune exec -- dev/dune-dbg /path/to/foo.v (ocd) source dune_db ``` or ``` -dune exec dev/dune-dbg checker Foo +dune exec -- dev/dune-dbg checker Foo (ocd) source dune_db ``` @@ -130,7 +130,7 @@ For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. After doing `make -f Makefile.dune voboot`, the following commands should work: ``` -dune exec dev/shim/coqbyte-prelude +dune exec -- dev/shim/coqbyte-prelude > Drop. # #directory "dev";; # #use "include_dune";; diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 01c2b574a2..d00c8cb11a 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -119,6 +119,16 @@ Universes 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 + Primitive projections component: primitive projections, guard condition |