diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/README.md | 77 | ||||
| -rw-r--r-- | dev/doc/changes.md | 113 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 252 | ||||
| -rw-r--r-- | dev/doc/profiling.txt | 2 | ||||
| -rw-r--r-- | dev/doc/setup.txt | 269 | ||||
| -rw-r--r-- | dev/doc/translate.txt | 495 | ||||
| -rw-r--r-- | dev/doc/versions-history.tex | 12 | ||||
| -rw-r--r-- | dev/doc/xml-protocol.md | 4 |
8 files changed, 456 insertions, 768 deletions
diff --git a/dev/doc/README.md b/dev/doc/README.md new file mode 100644 index 0000000000..1a4e40f68b --- /dev/null +++ b/dev/doc/README.md @@ -0,0 +1,77 @@ +# Beginner's guide to hacking Coq + +## Getting dependencies + +Assuming one is running Ubuntu (if not, replace `apt` with the package manager of choice) + +``` +$ sudo apt-get install make opam git + +# At the time of writing, <latest-ocaml-version> is 4.06.1. +# The latest version number is available at: https://ocaml.org/releases/ + +$ opam init --comp <latest-ocaml-version> + +# Then follow the advice displayed at the end as how to update your + ~/.bashrc and ~/.ocamlinit files. + +$ source ~/.bashrc +$ opam install camlp5 + +# needed if you want to build "coqide" target + +$ sudo apt-get install liblablgtksourceview2-ocaml-dev \ + libgtk2.0-dev libgtksourceview2.0-dev +$ opam install lablgtk +``` + +## Building `coqtop` +The general workflow is to first setup a development environment with +the correct `configure` settings, then hacking on Coq, make-ing, and testing. + + +This document will use `$JOBS` to refer to the number of parallel jobs one +is willing to have with `make`. + + +``` +$ git clone git clone https://github.com/coq/coq.git +$ cd coq +$ ./configure -profile devel +$ make -j $JOBS # Make once for `merlin`(autocompletion tool) + +<hack> + +$ make -j $JOBS states # builds just enough to run coqtop +$ bin/coqtop -compile <test_file_name.v> +<goto hack until stuff works> + +<run test-suite> +``` + +To learn how to run the test suite, you can read +[`test-suite/README.md`](../../test-suite/README.md). + +## Coq functions of interest +- `Coqtop.start`: This function is the main entry point of coqtop. +- `Coqtop.parse_args `: This function is responsible for parsing command-line arguments. +- `Coqloop.loop`: This function implements the read-eval-print loop. +- `Vernacentries.interp`: This function is called to execute the Vernacular command user have typed. + It dispatches the control to specific functions handling different Vernacular command. +- `Vernacentries.vernac_check_may_eval`: This function handles the `Check ...` command. + + +## Development environment + tooling +- [`Merlin`](https://github.com/ocaml/merlin) for autocomplete. +- [Wiki pages on tooling containing `emacs`, `vim`, and `git` information](https://github.com/coq/coq/wiki/DevelSetup) + +## A note about rlwrap + +When using `rlwrap coqtop` make sure the version of `rlwrap` is at least +`0.42`, otherwise you will get + +``` +rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory +``` + +If this happens either update or use an alternate readline wrapper like `ledit`. diff --git a/dev/doc/changes.md b/dev/doc/changes.md index f3fc126f92..6d5023405a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -53,6 +53,16 @@ Printer.ml API pr_subgoal and pr_goal was removed to simplify the code. It was earlierly used by PCoq. +Kernel + + The following renamings happened: + - `Context.Rel.t` into `Constr.rel_context` + - `Context.Named.t` into `Constr.named_context` + - `Context.Compacted.t` into `Constr.compacted_context` + - `Context.Rel.Declaration.t` into `Constr.rel_declaration` + - `Context.Named.Declaration.t` into `Constr.named_declaration` + - `Context.Compacted.Declaration.t` into `Constr.compacted_declaration` + Source code organization - We have eliminated / fused some redundant modules and relocated a @@ -72,11 +82,114 @@ Vernacular commands `tactics/`. In all cases adapting is a matter of changing the module name. +Primitive number parsers + +- For better modularity, the primitive parsers for positive, N and Z + have been split over three files (plugins/syntax/positive_syntax.ml, + plugins/syntax/n_syntax.ml, plugins/syntax/z_syntax.ml). + ### Unit testing The test suite now allows writing unit tests against OCaml code in the Coq code base. Those unit tests create a dependency on the OUnit test framework. +### Transitioning away from Camlp5 + +In an effort to reduce dependency on camlp5, the use of several grammar macros +is discouraged. Coq is now shipped with its own preprocessor, called coqpp, +which serves the same purpose as camlp5. + +To perform the transition to coqpp macros, one first needs to change the +extension of a macro file from `.ml4` to `.mlg`. Not all camlp5 macros are +handled yet. + +Due to parsing constraints, the syntax of the macros is slightly different, but +updating the source code is mostly a matter of straightforward +search-and-replace. The main differences are summarized below. + +#### OCaml code + +Every piece of toplevel OCaml code needs to be wrapped into braces. + +For instance, code of the form +``` +let myval = 0 +``` +should be turned into +``` +{ +let myval = 0 +} +``` + +#### TACTIC EXTEND + +Steps to perform: +- replace the brackets enclosing OCaml code in actions with braces +- if not there yet, add a leading `|̀ to the first rule + +For instance, code of the form: +``` +TACTIC EXTEND my_tac + [ "tac1" int_or_var(i) tactic(t) ] -> [ mytac1 ist i t ] +| [ "tac2" tactic(t) ] -> [ mytac2 t ] +END +``` +should be turned into +``` +TACTIC EXTEND my_tac +| [ "tac1" int_or_var(i) tactic(t) ] -> { mytac1 ist i t } +| [ "tac2" tactic(t) ] -> { mytac2 t } +END +``` + +#### VERNAC EXTEND + +Not handled yet. + +#### ARGUMENT EXTEND + +Not handled yet. + +#### GEXTEND + +Most plugin writers do not need this low-level interface, but for the sake of +completeness we document it. + +Steps to perform are: +- replace GEXTEND with GRAMMAR EXTEND +- wrap every occurrence of OCaml code in actions into braces { } + +For instance, code of the form +``` +GEXTEND Gram + GLOBAL: my_entry; + +my_entry: +[ [ x = bar; y = qux -> do_something x y + | "("; z = LIST0 my_entry; ")" -> do_other_thing z +] ]; +END +``` +should be turned into +``` +GRAMMAR EXTEND Gram + GLOBAL: my_entry; + +my_entry: +[ [ x = bar; y = qux -> { do_something x y } + | "("; z = LIST0 my_entry; ")" -> { do_other_thing z } +] ]; +END +``` + +Caveats: +- No `GLOBAL` entries mean that they are all local, while camlp5 special-cases + this as a shorthand for all global entries. Solution: always define a `GLOBAL` + section. +- No complex patterns allowed in token naming. Solution: match on it inside the + OCaml quotation. + ## Changes between Coq 8.7 and Coq 8.8 ### Bug tracker diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs new file mode 100644 index 0000000000..6166d24b70 --- /dev/null +++ b/dev/doc/critical-bugs @@ -0,0 +1,252 @@ +Preliminary compilation of critical bugs in stable releases of Coq +================================================================== + WORK IN PROGRESS WITH SEVERAL OPEN QUESTIONS + + +To add: #7723 (vm_compute universe polymorphism), #7695 (modules and algebraic universes), #7615 (lost functor substitutions) + +Typing constructions + + component: "match" + summary: substitution missing in the body of a let + introduced: ? + impacted released versions: V8.3-V8.3pl2, V8.4-V8.4pl4 + impacted development branches: none + impacted coqchk versions: ? + fixed in: master/trunk/v8.5 (e583a79b5, 22 Nov 2015, Herbelin), v8.4 (525056f1, 22 Nov 2015, Herbelin), v8.3 (4bed0289, 22 Nov 2015, Herbelin) + found by: Herbelin + exploit: test-suite/success/Case22.v + GH issue number: ? + risk: ? + + component: fixpoint, guard + summary: missing lift in checking guard + introduced: probably from V5.10 + impacted released versions: probably V5-V7, V8.0-V8.0pl4, V8.1-V8.1pl4 + impacted development branches: v8.0 ? + impacted coqchk versions: ? + fixed in: master/trunk/v8.2 (ff45afa8, r11646, 2 Dec 2008, Barras), v8.1 (f8e7f273, r11648, 2 Dec 2008, Barras) + found by: Barras + exploit: test-suite/failure/guard.v + GH issue number: none + risk: unprobable by chance + + component: cofixpoint, guard + summary: de Bruijn indice bug in checking guard of nested cofixpoints + introduced: after V6.3.1, before V7.0 + impacted released versions: V8.0-V8.0pl4, V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2, V8.4-V8.4pl4 + impacted development branches: none + impacted coqchk versions: ? + fixed in: master (9f81e2c36, 10 Apr 2014, Dénès), v8.4 (f50ec9e7d, 11 Apr 2014, Dénès), v8.3 (40c0fe7f4, 11 Apr 2014, Dénès), v8.2 (06d66df8c, 11 Apr 2014, Dénès), v8.1 (977afae90, 11 Apr 2014, Dénès), v8.0 (f1d632992, 29 Nov 2015, Herbelin, backport) + found by: Dénès + exploit: ? + GH issue number: none ? + risk: ? + + component: inductive types, elimination principle + summary: de Bruijn indice bug in computing allowed elimination principle + introduced: 23 May 2006, 9c2d70b, r8845, Herbelin (part of universe polymorphism) + impacted released versions: V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2, V8.4-V8.4pl4 + impacted development branches: none + impacted coqchk versions: ? + fixed in: master (8a01c3685, 24 Jan 2014, Dénès), v8.4 (8a01c3685, 25 Feb 2014, Dénès), v8.3 (2b3cc4f85, 25 Feb 2014, Dénès), v8.2 (459888488, 25 Feb 2014, Dénès), v8.1 (79aa20872, 25 Feb 2014, Dénès) + found by: Dénès + exploit: see GH#3211 + GH issue number: #3211 + risk: ? + + component: universe subtyping + summary: bug in Prop<=Set conversion which made Set identifiable with Prop, preventing a proof-irrelevant interpretation of Prop + introduced: V8.2 (bba897d5f, 12 May 2008, Herbelin) + impacted released versions: V8.2-V8.2pl2 + impacted development branches: none + impacted coqchk versions: ? + fixed in: master/trunk (679801, r13450, 23 Sep 2010, Glondu), v8.3 (309a53f2, r13449, 22 Sep 2010, Glondu), v8.2 (41ea5f08, r14263, 6 Jul 2011, Herbelin, backport) + found by: Georgi Guninski + exploit: test-suite/bugs/closed/4294.v + GH issue number: #4294 + risk: ? + +Module system + + component: modules, universes + summary: missing universe constraints in typing "with" clause of a module type + introduced: ? + impacted released versions: V8.3-V8.3pl2, V8.4-V8.4pl6; unclear for V8.2 and previous versions + impacted development branches: none + impacted coqchk versions: ? + fixed in: master/trunk (d4869e059, 2 Oct 2015, Sozeau), v8.4 (40350ef3b, 9 Sep 2015, Sozeau) + found by: Dénès + exploit: test-suite/bugs/closed/4294.v + GH issue number: #4294 + risk: ? + +Module system + + component: modules, universes + summary: universe constraints for module subtyping not stored in vo files + introduced: presumably 8.2 (b3d3b56) + impacted released versions: 8.2, 8.3, 8.4 + impacted development branches: v8.5 + impacted coqchk versions: none + fixed in: v8.2 (c1d9889), v8.3 (8056d02), v8.4 (a07deb4), trunk (0cd0a3e) Mar 5, 2014, Tassi + found by: Tassi by running coqchk on the mathematical components library + exploit: requires multiple files, no test provided + GH issue number: #3243 + risk: could be exploited by mistake + +Universes + + component: template polymorphism + summary: issue with two parameters in the same universe level + introduced: 23 May 2006, 9c2d70b, r8845, Herbelin + impacted released versions: V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 + impacted development branches: none + impacted coqchk versions: ? + fixed in: trunk/master/v8.4 (8082d1faf, 5 Oct 2011, Herbelin), V8.3pl3 (bb582bca2, 5 Oct 2011, Herbelin), v8.2 branch (3333e8d3, 5 Oct 2011, Herbelin), v8.1 branch (a8fc2027, 5 Oct 2011, Herbelin), + found by: Barras + exploit: test-suite/failure/inductive4.v + GH issue number: none + risk: unlikely to be activated by chance + +Primitive projections + + component: primitive projections, guard condition + summary: check of guardedness of extra arguments of primitive projections missing + introduced: 6 May 2014, a4043608f, Sozeau + impacted released versions: V8.5-V8.5pl2, + impacted development branches: none + impacted coqchk versions: ? + fixed in: trunk/master/v8.5 (ba00867d5, 25 Jul 2016, Sozeau) + found by: Sozeau, by analyzing bug report #4876 + exploit: to be done (?) + GH issue number: #4876 + risk: consequence of bug found by chance, unlikely to be exploited by chance (MS?) + + component: primitive projections, guard condition + summary: records based on primitive projections became possibly recursive without the guard condition being updated + introduced: 10 Sep 2014, 6624459e4, Sozeau (?) + impacted released versions: V8.5 + impacted development branches: none + impacted coqchk versions: ? + fixed in: trunk/master/v8.5 (120053a50, 4 Mar 2016, Dénès) + found by: Dénès exploiting bug #4588 + exploit: test-suite/bugs/closed/4588.v + GH issue number: #4588 + risk: ? + +Conversion machines + + component: "lazy machine" (lazy krivine abstract machine) + summary: the invariant justifying some optimization was wrong for some combination of sharing side effects + introduced: prior to V7.0 + impacted released versions: V8.0-V8.0pl4, V8.1-V8.1pl3 + impacted development branches: none + impacted coqchk versions: (eefe63d52, Barras, 20 May 2008), was in beta-development for 8.2 at this time + fixed in: master/trunk/8.2 (f13aaec57/a8b034513, 15 May 2008, Barras), v8.1 (e7611477a, 15 May 2008, Barras), v8.0 (6ed40a8bc, 29 Nov 2016, Herbelin, backport) + found by: Gonthier + exploit: by Gonthier + GH issue number: none + risk: unrealistic to be exploited by chance + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: collision between constructors when more than 256 constructors in a type + introduced: V8.1 + impacted released versions: V8.1-V8.5pl3, V8.2-V8.2pl2, V8.3-V8.3pl3, V8.4-V8.4pl5 + impacted development branches: none + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: master/trunk/v8.5 (00894adf6/596a4a525, 26-39 Mar 2015, Grégoire), v8.4 (cd2101a39, 1 Apr 2015, Grégoire), v8.3 (a0c7fc05b, 1 Apr 2015, Grégoire), v8.2 (2c6189f61, 1 Apr 2015, Grégoire), v8.1 (bb877e5b5, 29 Nov 2015, Herbelin, backport) + found by: Dénès, Pédrot + exploit: test-suite/failure/vm-bug4157.v + GH issue number: #4157 + risk: + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: wrong universe constraints + introduced: possibly exploitable from V8.1; exploitable at least from V8.5 + impacted released versions: V8.1-V8.4pl5 unknown, V8.5-V8.5pl3, V8.6-V8.6.1, V8.7.0-V8.7.1 + impacted development branches: unknown for v8.1-v8.4, none from v8.5 + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: master (c9f3a6cbe, 12 Feb 2018, PR#6713, Dénès), v8.7 (c058a4182, 15 Feb 2018, Zimmermann, backport), v8.6 (a2cc54c64, 21 Feb 2018, Herbelin, backport), v8.5 (d4d550d0f, 21 Feb 2018, Herbelin, backport) + found by: Dénès + exploit: test-suite/bugs/closed/6677.v + GH issue number: #6677 + risk: + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: missing pops in executing 31bit arithmetic + introduced: V8.5 + impacted released versions: V8.1-V8.4pl5 + impacted development branches: v8.1 (probably) + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: master/trunk/v8.5 (a5e04d9dd, 6 Sep 2015, Dénès), v8.4 (d5aa3bf6, 9 Sep 2015, Dénès), v8.3 (5da5d751, 9 Sep 2015, Dénès), v8.2 (369e82d2, 9 Sep 2015, Dénès), + found by: Catalin Hritcu + exploit: lost? + GH issue number: ? + risk: + + 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 + impacted released versions: V8.5-V8.5pl1 + impacted development branches: none + impacted coqchk versions: none (no native computation in coqchk) + fixed in: master/trunk/v8.6 (244d7a9aa, 19 May 2016, letouzey), v8.5 (088b3161c, 19 May 2016, letouzey), + found by: Letouzey, Dénès + exploit: lost? + GH issue number: ? + risk: + +Conflicts with axioms in library + + component: library of real numbers + summary: axiom of description and decidability of equality on real numbers in library Reals was inconsistent with impredicative Set + introduced: 67c75fa01, 20 Jun 2002 + impacted released versions: 7.3.1, 7.4 + impacted coqchk versions: + fixed by deciding to drop impredicativity of Set: bac707973, 28 Oct 2004 + found by: Herbelin & Werner + exploit: need to find the example again + GH issue number: no + risk: unlikely to be exploited by chance + + component: library of extensional sets, guard condition + summary: guard condition was unknown to be inconsistent with propositional extensionality in library Sets + introduced: not a bug per se but an incompatibility discovered late + impacted released versions: technically speaking from V6.1 with the introduction of the Sets library which was then inconsistent from the very beginning without we knew it + impacted coqchk versions: ? + fixed by constraining the guard condition: (9b272a8, ccd7546c 28 Oct 2014, Barras, Dénès) + found by: Schepler, Dénès, Azevedo de Amorim + exploit: ? + GH issue number: none + risk: unlikely to be exploited by chance (?) + + component: library for axiom of choice and excluded-middle + summary: incompatibility axiom of choice and excluded-middle with elimination of large singletons to Set + introduced: not a bug but a change of intended "model" + impacted released versions: strictly before 8.1 + impacted coqchk versions: ? + fixed by constraining singleton elimination: b19397ed8, r9633, 9 Feb 2007, Herbelin + found by: Benjamin Werner + exploit: + GH issue number: none + risk: + +There were otherwise several bugs in beta-releases, from memory, bugs with beta versions of primitive projections or template polymorphism or native compilation or guard (e7fc96366, 2a4d714a1). + +There were otherwise maybe unexploitable kernel bugs, e.g. 2df88d83 (Require overloading), 0adf0838 ("Univs: uncovered bug in strengthening of opaque polymorphic definitions."), 5122a398 (#3746 about functors), #4346 (casts in VM), a14bef4 (guard condition in 8.1), 6ed40a8 ("Georges' bug" with ill-typed lazy machine), and various other bugs in 8.0 or 8.1 w/o knowing if they are critical. + +Another non exploitable bug? + + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: bug in 31bit arithmetic + introduced: V8.1 + impacted released versions: none + impacted development branches: + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: master/trunk/v8.5 (0f8d1b92c, 6 Sep 2015, Dénès) + found by: Dénès, from a bug report by Tahina Ramananandro + exploit: ? + GH issue number: ? + risk: + diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt index 9d2ebf0d4c..b5dd8445db 100644 --- a/dev/doc/profiling.txt +++ b/dev/doc/profiling.txt @@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux. In Coq source folder: -opam switch 4.02.1+fp +opam switch 4.02.3+fp ./configure -local -debug make perf record -g bin/coqtop -compile file.v diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt deleted file mode 100644 index c48c2d5d16..0000000000 --- a/dev/doc/setup.txt +++ /dev/null @@ -1,269 +0,0 @@ -This document provides detailed guidance on how to: -- compile Coq -- take advantage of Merlin in Emacs -- enable auto-completion for Ocaml source-code -- use ocamldebug in Emacs for debugging coqtop -The instructions were tested with Debian 8.3 (Jessie). - -The procedure is somewhat tedious, but the final results are (still) worth the effort. - -How to compile Coq ------------------- - -Getting build dependencies: - - sudo apt-get install make opam git - opam init --comp 4.02.3 - # Then follow the advice displayed at the end as how to update your ~/.bashrc and ~/.ocamlinit files. - - source ~/.bashrc - - # needed if you want to build "coqtop" target - opam install camlp5 - - # needed if you want to build "coqide" target - sudo apt-get install liblablgtksourceview2-ocaml-dev libgtk2.0-dev libgtksourceview2.0-dev - opam install lablgtk - - # needed if you want to build "doc" target - sudo apt-get install texlive-latex-recommended texlive-fonts-extra texlive-math-extra \ - hevea texlive-latex-extra latex-xcolor - -Cloning Coq: - - # Go to the directory where you want to clone Coq's source-code. E.g.: - cd ~/git - - git clone https://github.com/coq/coq.git - -Building coqtop: - - cd ~/git/coq - git checkout trunk - make distclean - ./configure -profile devel - make clean - make -j4 coqide printers - -The "-profile devel" enables all options recommended for developers (like -warnings, support for Merlin, etc). Moreover Coq is configured so that -it can be run without installing it (i.e. from the current directory). - -Once the compilation is over check if -- bin/coqtop -- bin/coqide -behave as expected. - - -A note about rlwrap -------------------- - -When using "rlwrap coqtop" make sure the version of rlwrap is at least -0.42, otherwise you will get - - rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory - -If this happens either update or use an alternate readline wrapper like "ledit". - - -How to install and configure Merlin (for Emacs) ------------------------------------------------ - - sudo apt-get install emacs - - opam install tuareg - # Follow the advice displayed at the end as how to update your ~/.emacs file. - - opam install merlin - # Follow the advice displayed at the end as how to update your ~/.emacs file. - -Then add this: - - (push "~/.opam/4.02.3/share/emacs/site-lisp" load-path) ; directory containing merlin.el - (setq merlin-command "~/.opam/4.02.3/bin/ocamlmerlin") ; needed only if ocamlmerlin not already in your PATH - (autoload 'merlin-mode "merlin" "Merlin mode" t) - (add-hook 'tuareg-mode-hook 'merlin-mode) - (add-hook 'caml-mode-hook 'merlin-mode) - (load "~/.opam/4.02.3/share/emacs/site-lisp/tuareg-site-file") - - ;; Do not use TABs. These confuse Merlin. - (setq-default indent-tabs-mode nil) - -to your ~/.emacs file. - -Further Emacs configuration when we start it for the first time. - -Try to open some *.ml file in Emacs, e.g.: - - cd ~/git/coq - emacs toplevel/coqtop.ml & - -Emacs display the following strange message: - - The local variables list in ~/git/coq - contains values that may be safe (*). - - Do you want to apply it? - -Just press "!", i.e. "apply the local variable list, and permanently mark these values (\*) as safe." - -Emacs then shows two windows: -- one window that shows the contents of the "toplevel/coqtop.ml" file -- and the other window that shows greetings for new Emacs users. - -If you do not want to see the second window next time you start Emacs, just check "Never show it again" and click on "Dismiss this startup screen." - -The default key-bindings are described here: - - https://github.com/the-lambda-church/merlin/wiki/emacs-from-scratch - -If you want, you can customize them by replacing the following lines: - - (define-key merlin-map (kbd "C-c C-x") 'merlin-error-next) - (define-key merlin-map (kbd "C-c C-l") 'merlin-locate) - (define-key merlin-map (kbd "C-c &") 'merlin-pop-stack) - (define-key merlin-map (kbd "C-c C-t") 'merlin-type-enclosing) - -in the file "~/.opam/4.02.3/share/emacs/site-lisp/merlin.el" with what you want. -In the text below we assume that you changed the origin key-bindings in the following way: - - (define-key merlin-map (kbd "C-n") 'merlin-error-next) - (define-key merlin-map (kbd "C-l") 'merlin-locate) - (define-key merlin-map (kbd "C-b") 'merlin-pop-stack) - (define-key merlin-map (kbd "C-t") 'merlin-type-enclosing) - -Now, when you press <Ctrl+L>, Merlin will show the definition of the symbol in a separate window. -If you prefer to jump to the definition within the same window, do this: - - <Alt+X> customize-group <ENTER> merlin <ENTER> - - Merlin Locate In New Window - - Value Menu - - Never Open In New Window - - State - - Set For Future Sessions - -Testing (Merlin): - - cd ~/git/coq - emacs toplevel/coqtop.ml & - -Go to the end of the file where you will see the "start" function. - -Go to a line where "init_toplevel" function is called. - -If you want to jump to the position where that function or datatype under the cursor is defined, press <Ctrl+L>. - -If you want to jump back, type: <Ctrl+B> - -If you want to learn the type of the value at current cursor's position, type: <Ctrl+T> - - -Enabling auto-completion in emacs ---------------------------------- - -In Emacs, type: <Alt+M> list-packages <ENTER> - -In the list that is displayed, click on "company". - -A new window appears where just click on "Install" and then answer "Yes". - -These lines: - - (package-initialize) - (require 'company) - ; Make company aware of merlin - (add-to-list 'company-backends 'merlin-company-backend) - ; Enable company on merlin managed buffers - (add-hook 'merlin-mode-hook 'company-mode) - (global-set-key [C-tab] 'company-complete) - -then need to be added to your "~/.emacs" file. - -Next time when you start emacs and partially type some identifier, -emacs will offer the corresponding completions. -Auto-completion can also be manually invoked by typing <Ctrl+TAB>. -Description of various other shortcuts is here. - - http://company-mode.github.io/ - - -Getting along with ocamldebug ------------------------------ - -The default ocamldebug key-bindings are described here. - - http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec369 - -If you want, you can customize them by putting the following commands: - - (global-set-key (kbd "<f5>") 'ocamldebug-break) - (global-set-key (kbd "<f6>") 'ocamldebug-run) - (global-set-key (kbd "<f7>") 'ocamldebug-next) - (global-set-key (kbd "<f8>") 'ocamldebug-step) - (global-set-key (kbd "<f9>") 'ocamldebug-finish) - (global-set-key (kbd "<f10>") 'ocamldebug-print) - (global-set-key (kbd "<f12>") 'camldebug) - -to your "~/.emacs" file. - -Let us try whether ocamldebug in Emacs works for us. -(If necessary, re-)compile coqtop: - - cd ~/git/coq - make -j4 coqide printers - -open Emacs: - - emacs toplevel/coqtop.ml & - -and type: - - <F12> ../bin/coqtop.byte <ENTER> ../dev/ocamldebug-coq <ENTER> - -As a result, a new window is open at the bottom where you should see: - - (ocd) - -i.e. an ocamldebug shell. - - 1. Switch to the window that contains the "coqtop.ml" file. - 2. Go to the end of the file. - 3. Find the definition of the "start" function. - 4. Go to the "let" keyword that is at the beginning of the first line. - 5. By pressing <F5> you set a breakpoint to the cursor's position. - 6. By pressing <F6> you start the bin/coqtop process. - 7. Then you can: - - step over function calls: <F7> - - step into function calls: <F8> - - or finish execution of the current function until it returns: <F9>. - -Other ocamldebug commands, can be typed to the window that holds the ocamldebug shell. - -The points at which the execution of Ocaml program can stop are defined here: - - http://caml.inria.fr/pub/docs/manual-ocaml/debugger.html#sec350 - - -Installing printers to ocamldebug ---------------------------------- - -There is a pretty comprehensive set of printers defined for many common data types. -You can load them by switching to the window holding the "ocamldebug" shell and typing: - - (ocd) source "../dev/db" - - -Some of the functions were you might want to set a breakpoint and see what happens next ---------------------------------------------------------------------------------------- - -- Coqtop.start : This function is the main entry point of coqtop. -- Coqtop.parse_args : This function is responsible for parsing command-line arguments. -- Coqloop.loop : This function implements the read-eval-print loop. -- Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\ - It dispatches the control to specific functions handling different Vernacular command. -- Vernacentries.vernac_check_may_eval : This function handles the "Check ..." command. diff --git a/dev/doc/translate.txt b/dev/doc/translate.txt deleted file mode 100644 index 5b372c96c3..0000000000 --- a/dev/doc/translate.txt +++ /dev/null @@ -1,495 +0,0 @@ - - How to use the translator - ========================= - - (temporary version to be included in the official - TeX document describing the translator) - -The translator is a smart, robust and powerful tool to improve the -readibility of your script. The current document describes the -possibilities of the translator. - -In case of problem recompiling the translated files, don't waste time -to modify the translated file by hand, read first the following -document telling on how to modify the original files to get a smooth -uniform safe translation. All 60000 lines of Coq lines on our -user-contributions server have been translated without any change -afterwards, and 0,5 % of the lines of the original files (mainly -notations) had to be modified beforehand to get this result. - -Table of contents ------------------ - -I) Implicit Arguments - 1) Strict Implicit Arguments - 2) Implicit Arguments in standard library - -II) Notations - 1) Translating a V7 notation as it was - 2) Translating a V7 notation which conflicts with the new syntax - a) Associativity conflicts - b) Conflicts with other notations - b1) A notation hides another notation - b2) A notation conflicts with the V8 grammar - b3) My notation is already defined at another level - c) How to use V8only with Distfix ? - d) Can I overload a notation in V8, e.g. use "*" and "+" ? - 3) Using the translator to have simplest notations - 4) Setting the translator to automatically use new notations that - wasn't used in old syntax - 5) Defining a construction and its notation simultaneously - -III) Various pitfalls - 1) New keywords - 2) Old "Case" and "Match" - 3) Change of definition or theorem names - 4) Change of tactic names - ---------------------------------------------------------------------- - -I) Implicit Arguments - ------------------ - -1) Strict Implicit Arguments - - "Set Implicit Arguments" changes its meaning in V8: the default is -to turn implicit only the arguments that are _strictly_ implicit (or -rigid), i.e. that remains inferable whatever the other arguments -are. E.g "x" inferable from "P x" is not strictly inferable since it -can disappears if "P" is instanciated by a term which erase "x". - - To respect the old semantics, the default behaviour of the -translator is to replace each occurrence "Set Implicit Arguments" by - - Set Implicit Arguments. - Unset Strict Implicits. - - However, you may wish to adopt the new semantics of "Set Implicit -Arguments" (for instance because you think that the choice of -arguments it setsimplicit is more "natural" for you). In this case, -add the option -strict-implicit to the translator. - - Warning: Changing the number of implicit arguments can break the -notations. Then use the V8only modifier of Notations. - -2) Implicit Arguments in standard library - - Main definitions of standard library have now implicit -arguments. These arguments are dropped in the translated files. This -can exceptionally be a source of incompatibilities which has to be -solved by hand (it typically happens for polymorphic functions applied -to "nil" or "None"). - -II) Notations - --------- - - Grammar (on constr) and Syntax are no longer supported. Replace them by -Notation before translation. - - Precedence levels are now from 0 to 200. In V8, the precedence and -associativity of an operator cannot be redefined. Typical level are -(refer to the chapter on notations in the Reference Manual for the -full list): - - <-> : 95 (no associativity) - -> : 90 (right associativity) - \/ : 85 (right associativity) - /\ : 80 (right associativity) - ~ : 75 (right associativity) - =, <, >, <=, >=, <> : 70 (no associativity) - +, - : 50 (left associativity) - *, / : 40 (left associativity) - ^ : 30 (right associativity) - -1) Translating a V7 notation as it was - - By default, the translator keeps the associativity given in V7 while -the levels are mapped according to the following table: - - the V7 levels [ 0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10] - are resp. mapped in V8 to [ 0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100] - with predefined assoc [ No; L; R; L; L; No; R; R; R; No; L] - - If this is OK for you, just simply apply the translator. - -2) Translating a V7 notation which conflicts with the new syntax - -a) Associativity conflict - - Since the associativity of the levels obtained by translating a V7 -level (as shown on table above) cannot be changed, you have to choose -another level with a compatible associativity. - - You can choose any level between 0 and 200, knowing that the -standard operators are already set at the levels shown on the list -above. - -Example 1: Assume you have a notation - -Infix NONA 2 "=_S" my_setoid_eq. - -By default, the translator moves it to level 30 which is right -associative, hence a conflict with the expected no associativity. - -To solve the problem, just add the "V8only" modifier to reset the -level and enforce the associativity as follows: - -Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity). - -The translator now knows that it has to translate "=_S" at level 70 -with no associativity. - -Rem: 70 is the "natural" level for relations, hence the choice of 70 -here, but any other level accepting a no-associativity would have been -OK. - -Example 2: Assume you have a notation - -Infix RIGHTA 1 "o" my_comp. - -By default, the translator moves it to level 20 which is left -associative, hence a conflict with the expected right associativity. - -To solve the problem, just add the "V8only" modifier to reset the -level and enforce the associativity as follows: - -Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity). - -The translator now knows that it has to translate "o" at level 20 -which has the correct "right associativity". - -Rem: We assumed here that the user wants a strong precedence for -composition, in such a way, say, that "f o g + h" is parsed as -"(f o g) + h". To get "o" binding less than the arithmetical operators, -an appropriated level would have been close of 70, and below, e.g. 65. - -b) Conflicts with other notations - -Since the new syntax comes with new keywords and new predefined -symbols, new conflicts can occur. Again, you can use the option V8only -to inform the translator of the new syntax to use. - -b1) A notation hides another notation - -Rem: use Print Grammar constr in V8 to diagnose the overlap and see the -section on factorization in the chapter on notations of the Reference -Manual for hints on how to factorize. - -Example: - -Notation "{ x }" := (my_embedding x) (at level 1). - -overlaps in V8 with notation "{ x : A & P }" at level 0 and with x at -level 99. The conflicts can be solved by left-factorizing the notation -as follows: - -Notation "{ x }" := (my_embedding x) (at level 1) - V8only (at level 0, x at level 99). - -b2) A notation conflicts with the V8 grammar. - -Again, use the V8only modifier to tell the translator to automatically -take in charge the new syntax. - -Example: - -Infix 3 "@" app. - -Since "@" is used in the new syntax for deactivating the implicit -arguments, another symbol has to be used, e.g. "@@". This is done via -the V8only option as follows: - -Infix 3 "@" app V8only "@@" (at level 40, left associativity). - -or, alternatively by - -Notation "x @ y" := (app x y) (at level 3, left associativity) - V8only "x @@ y" (at level 40, left associativity). - -b3) My notation is already defined at another level (or with another -associativity) - -In V8, the level and associativity of a given notation can no longer -be changed. Then, either you adopt the standard reserved levels and -associativity for this notation (as given on the list above) or you -change your notation. - -- To change the notation, follow the directions in section b2. - -- To adopt the standard level, just use V8only without any argument. - -Example. - -Infix 6 "*" my_mult. - -is not accepted as such in V8. Write - -Infix 6 "*" my_mult V8only. - -to tell the translator to use "*" at the reserved level (i.e. 40 with -left associativity). Even better, use interpretation scopes (look at -the Reference Manual). - -c) How to use V8only with Distfix ? - -You can't, use Notation instead of Distfix. - -d) Can I overload a notation in V8, e.g. use "*" and "+" for my own -algebraic operations ? - -Yes, using interpretation scopes (see the corresponding chapter in the -Reference Manual). - -3) Using the translator to have simplest notations - -Thanks to the new syntax, * has now the expected left associativity, -and the symbols <, >, <= and >= are now available. - -Thanks to the interpretation scopes, you can overload the -interpretation of these operators with the default interpretation -provided in Coq. - -This may be a motivation to use the translator to automatically change -the notations while switching to the new syntax. - -See sections b) and d) above for examples. - -4) Setting the translator to automatically use new notations that -wasn't used in old syntax - -Thanks to the "Notation" mechanism, defining symbolic notations is -simpler than in the previous versions of Coq. - -Thanks to the new syntax and interpretation scopes, new symbols and -overloading is available. - -This may be a motivation for using the translator to automatically change -the notations while switching to the new syntax. - -Use for that the commands V8Notation and V8Infix. - -Examples: - -V8Infix "==>" my_relation (at level 65, right associativity). - -tells the translator to write an infix "==>" instead of my_relation in -the translated files. - -V8Infix ">=" my_ge. - -tells the translator to write an infix ">=" instead of my_ge in the -translated files and that the level and associativity are the standard -one (as defined in the chart above). - -V8Infix ">=" my_ge : my_scope. - -tells the translator to write an infix ">=" instead of my_ge in the -translated files, that the level and associativity are the standard -one (as defined in the chart above), but only if scope my_scope is -open or if a delimiting key is available for "my_scope" (see the -Reference Manual). - -5) Defining a construction and its notation simultaneously - -This is permitted by the new syntax. Look at the Reference Manual for -explanation. The translator is not fully able to take this in charge... - -III) Various pitfalls - ---------------- - -1) New keywords - - The following identifiers are new keywords - - "forall"; "fun"; "match"; "fix"; "cofix"; "for"; "if"; "then"; - "else"; "return"; "mod"; "at"; "let"; "_"; ".(" - - The translator automatically add a "_" to names clashing with a -keyword, except for files. Hence users may need to rename the files -whose name clashes with a keyword. - - Remark: "in"; "with"; "end"; "as"; "Prop"; "Set"; "Type" - were already keywords - -2) Old "Case" and "Match" - - "Case" and "Match" are normally automatically translated into - "match" or "match" and "fix", but sometimes it fails to do so. It - typically fails when the Case or Match is argument of a tactic whose - typing context is unknown because of a preceding Intro/Intros, as e.g. in - - Intros; Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end) - - The solution is then to replace the invocation of the sequence of - tactics into several invocation of the elementary tactics as follows - - Intros. Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end) - ^^^ - -3) Change of definition or theorem names - - Type "entier" from fast_integer.v is renamed into "N" by the -translator. As a consequence, user-defined objects of same name "N" -are systematically qualified even tough it may not be necessary. The -same apply for names "GREATER", "EQUAL", "LESS", etc... [COMPLETE LIST -TO GIVE]. - -4) Change of tactics names - - Since tactics names are now lowercase, this can clash with -user-defined tactic definitions. To pally this, clashing names are -renamed by adding an extra "_" to their name. - -====================================================================== -Main examples for new syntax ----------------------------- - -1) Constructions - - Applicative terms don't any longer require to be surrounded by parentheses as -e.g in - - "x = f y -> S x = S (f y)" - - - Product is written - - "forall x y : T, U" - "forall x y, U" - "forall (x y : T) z (v w : V), U" - etc. - - Abstraction is written - - "fun x y : T, U" - "fun x y, U" - "fun (x y : T) z (v w : V), U" - etc. - - Pattern-matching is written - - "match x with c1 x1 x2 => t | c2 y as z => u end" - "match v1, v2 with c1 x1 x2, _ => t | c2 y, d z => u end" - "match v1 as y in le _ n, v2 as z in I p q return P n y p q z with - c1 x1 x2, _ => t | c2 y, d z => u end" - - The last example is the new form of what was written - - "<[n;y:(le ? n);p;q;z:(I p q)](P n y p q z)>Cases v1 v2 of - (c1 x1 x2) _ => t | (c2 y) (d z) => u end" - - Pattern-matching of type with one constructors and no dependencies -of the arguments in the resulting type can be written - - "let (x,y,z) as u return P u := t in v" - - Local fixpoints are written - - "fix f (n m:nat) z (x : X) {struct m} : nat := ... - with ..." - - and "struct" tells which argument is structurally decreasing. - - Explicitation of implicit arguments is written - - "f @1:=u v @3:=w t" - "@f u v w t" - -2) Tactics - - The main change is that tactics names are now lowercase. Besides -this, the following renaming are applied: - - "NewDestruct" -> "destruct" - "NewInduction" -> "induction" - "Induction" -> "simple induction" - "Destruct" -> "simple destruct" - - For tactics with occurrences, the occurrences now comes after and - repeated use is separated by comma as in - - "Pattern 1 3 c d 4 e" -> "pattern c at 3 1, d, e at 4" - "Unfold 1 3 f 4 g" -> "unfold f at 1 3, g at 4" - "Simpl 1 3 e" -> "simpl e at 1 3" - -3) Tactic language - - Definitions are now introduced with keyword "Ltac" (instead of -"Tactic"/"Meta" "Definition") and are implicitly recursive -("Recursive" is no longer used). - - The new rule for distinguishing terms from ltac expressions is: - - Write "ltac:" in front of any tactic in argument position and - "constr:" in front of any construction in head position - -4) Vernacular language - -a) Assumptions - - The syntax for commands is mainly unchanged. Declaration of -assumptions is now done as follows - - Variable m : t. - Variables m n p : t. - Variables (m n : t) (u v : s) (w : r). - -b) Definitions - - Definitions are done as follows - - Definition f m n : t := ... . - Definition f m n := ... . - Definition f m n := ... : t. - Definition f (m n : u) : t := ... . - Definition f (m n : u) := ... : t. - Definition f (m n : u) := ... . - Definition f a b (p q : v) r s (m n : t) : t := ... . - Definition f a b (p q : v) r s (m n : t) := ... . - Definition f a b (p q : v) r s (m n : t) := ... : t. - -c) Fixpoints - - Fixpoints are done this way - - Fixpoint f x (y : t) z a (b c : u) {struct z} : v := ... with ... . - Fixpoint f x : v := ... . - Fixpoint f (x : t) : v := ... . - - It is possible to give a concrete notation to a fixpoint as follows - - Fixpoint plus (n m:nat) {struct n} : nat as "n + m" := - match n with - | O => m - | S p => S (p + m) - end. - -d) Inductive types - - The syntax for inductive types is as follows - - Inductive t (a b : u) (d : e) : v := - c1 : w1 | c2 : w2 | ... . - - Inductive t (a b : u) (d : e) : v := - c1 : w1 | c2 : w2 | ... . - - Inductive t (a b : u) (d : e) : v := - c1 (x y : t) : w1 | c2 (z : r) : w2 | ... . - - As seen in the last example, arguments of the constructors can be -given before the colon. If the type itself is omitted (allowed only in -case the inductive type has no real arguments), this yields an -ML-style notation as follows - - Inductive nat : Set := O | S (n:nat). - Inductive bool : Set := true | false. - - It is even possible to define a syntax at the same time, as follows: - - Inductive or (A B:Prop) : Prop as "A \/ B":= - | or_introl (a:A) : A \/ B - | or_intror (b:B) : A \/ B. - - Inductive and (A B:Prop) : Prop as "A /\ B" := conj (a:A) (b:B). - diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 3867d4af90..8f9c3171da 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -395,7 +395,17 @@ Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect pl Coq V8.7 beta 2 & released 6 October 2017 & \\ -Coq V8.7 & released 18 October 2016 & \\ +Coq V8.7.0 & released 18 October 2017 & \\ + +Coq V8.7.1 & released 15 December 2017 & \\ + +Coq V8.7.2 & released 17 February 2018 & \\ + +Coq V8.8 beta1 & released 19 March 2018 & \\ + +Coq V8.8.0 & released 17 April 2018 & \feature{reference manual moved to Sphinx} \\ +&& \feature{effort towards better documented, better structured ML API}\\ +&& \feature{miscellaneous changes/improvements of existing features}\\ \end{tabular} diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index b35571e9ca..48671c03b6 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -10,9 +10,9 @@ versions of Proof General. A somewhat out-of-date description of the async state machine is [documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md). -OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli). +OCaml types for the protocol can be found in the [`ide/protocol/interface.ml` file](/ide/protocol/interface.ml). -Changes to the XML protocol are documented as part of [`dev/doc/changes.txt`](/dev/doc/changes.txt). +Changes to the XML protocol are documented as part of [`dev/doc/changes.md`](/dev/doc/changes.md). * [Commands](#commands) - [About](#command-about) |