From 5dfa8c9d9e3f1a5391825338498e0aaac28b4e28 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 27 Jun 2018 23:29:00 +0200 Subject: Clean up documentation around beginner's guide. - move `README` to `README.md` to take advantage of markdown features - remove `setup.txt`, port the editor specific information to the wiki. Merge development information into `dev/doc/README.md`. Wiki merge link: https://github.com/coq/coq/wiki/DevelSetup. - Add new links to files into `dev/README.md`. - Remove stale `translate.txt`. --- dev/README | 50 ----- dev/README.md | 46 +++++ dev/doc/README.md | 77 ++++++++ dev/doc/setup.txt | 269 --------------------------- dev/doc/translate.txt | 495 -------------------------------------------------- 5 files changed, 123 insertions(+), 814 deletions(-) delete mode 100644 dev/README create mode 100644 dev/README.md create mode 100644 dev/doc/README.md delete mode 100644 dev/doc/setup.txt delete mode 100644 dev/doc/translate.txt (limited to 'dev') diff --git a/dev/README b/dev/README deleted file mode 100644 index 453f85f0d..000000000 --- a/dev/README +++ /dev/null @@ -1,50 +0,0 @@ -This directory contains information and tools to help develop the - Coq system - ====================== - - -Debugging and profiling (in current directory - see doc/debugging.txt) ------------------------ - -ocamldebug-coq: to launch ocaml debugger (generated by the configure script) - -db: to install pretty-printers from ocaml debugger -base_db: to install raw pretty-printers from ocaml debugger - -include: to install pretty-printers from ocaml toplevel (use with the coq Drop command) -base_include: to install raw pretty-printers from ocaml toplevel - -vm_printers.ml, top_printers.ml: ML pretty-printers for debugging - - -Miscellaneous information about the code (directory doc) ------------------------------------------ - -changes.md: (partial) per-version summary of the evolution of Coq ML source -style.txt: a few style recommendations for writing Coq ML files -debugging.md: help for debugging or profiling -universes.txt: help for debugging universes -translate.txt: help for using coq translator -extensions.txt: some help about TACTIC EXTEND - -header: standard header for Coq ML files -perf-analysis: analysis of perfs measured on the compilation of user contribs -cic.dtd: official dtd of the calc. of ind. constr. for im/ex-portation - - -Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) ----------------------------------------- -"make mli-doc" in coq root directory. - - -Other development tools (directory tools) ------------------------ - -coqdev.el: helper customizations for everyday Coq development, eg - making `compile' work in subdirectories - -objects.el: various development utilities at emacs level - -anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse - location of Anomaly backtraces and jump to them conveniently from - the Emacs *compilation* output. diff --git a/dev/README.md b/dev/README.md new file mode 100644 index 000000000..4642aaf06 --- /dev/null +++ b/dev/README.md @@ -0,0 +1,46 @@ +# This directory contains information and tools to help develop the Coq system + + +## Debugging and profiling (`dev/`) +**More info on debugging: [`doc/debugging.md`](doc/debugging.md)** + +| File | Description | +| ---- | ----------- | +| dev/ocamldebug-coq | To launch ocaml debugger (generated by the configure script) | +| dev/db | To install pretty-printers from ocaml debugger | +| dev/base_db | To install raw pretty-printers from ocaml debugger | +| dev/include | To install pretty-printers from ocaml toplevel (use with the coq Drop command) | +| dev/base_include | To install raw pretty-printers from ocaml toplevel | +| dev/vm_printers.ml, top_printers.ml | ML pretty-printers for debugging | + + +## Miscellaneous information about the code (`dev/doc`) +**Beginner's guide to hacking Coq: [`dev/doc/README.md`](doc/README.md)** + +| File | Description | +| ---- | ----------- | +| [`dev/doc/changes.md`](doc/changes.md) | (partial) Per-version summary of the evolution of Coq ML source | +| [`dev/doc/style.txt`](doc/style.txt) | A few style recommendations for writing Coq ML files | +| [`dev/doc/debugging.md`](doc/debugging.md) | Help for debugging or profiling | +| [`dev/doc/universes.txt`](doc/universes.txt) | Help for debugging universes | +| [`dev/doc/extensions.txt`](doc/extensions.txt) | Some help about TACTIC EXTEND | +| [`dev/doc/perf-analysis`](doc/perf-analysis)| Analysis of perfs measured on the compilation of user contribs | +| [`dev/doc/cic.dtd`](doc/cic.dtd) | Official dtd of the calc. of ind. constr. for im/ex-portation | +| [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine | +| [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections | +| [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine | +| [`dev/doc/xml-protocol.md`](doc/proof-engine.md) | XML protocol that coqtop and IDEs use to communicate | +| [`dev/doc/MERGING.md`](doc/MERGING.md) | How pull requests should be merged into `master` | +| [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release | + + +## Documentation of ML interfaces using ocamldoc ( `dev/ocamldoc/html`) +`make mli-doc` in coq root directory. + + +## Other development tools (`dev/tools`) + +| File | Description | +| ---- | ----------- | +| [`dev/tools/coqdev.el`](tools/coqdev.el) | Helper customizations for everyday Coq development, eg making `compile` work in subdirectories +| [`dev/tools/objects.el`](tools/objects.el) | Various development utilities at emacs level | diff --git a/dev/doc/README.md b/dev/doc/README.md new file mode 100644 index 000000000..1a4e40f68 --- /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, is 4.06.1. +# The latest version number is available at: https://ocaml.org/releases/ + +$ opam init --comp + +# 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) + + + +$ make -j $JOBS states # builds just enough to run coqtop +$ bin/coqtop -compile + + + +``` + +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/setup.txt b/dev/doc/setup.txt deleted file mode 100644 index c48c2d5d1..000000000 --- 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 , 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: - - customize-group merlin - - 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 . - -If you want to jump back, type: - -If you want to learn the type of the value at current cursor's position, type: - - -Enabling auto-completion in emacs ---------------------------------- - -In Emacs, type: list-packages - -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 . -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 "") 'ocamldebug-break) - (global-set-key (kbd "") 'ocamldebug-run) - (global-set-key (kbd "") 'ocamldebug-next) - (global-set-key (kbd "") 'ocamldebug-step) - (global-set-key (kbd "") 'ocamldebug-finish) - (global-set-key (kbd "") 'ocamldebug-print) - (global-set-key (kbd "") '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: - - ../bin/coqtop.byte ../dev/ocamldebug-coq - -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 you set a breakpoint to the cursor's position. - 6. By pressing you start the bin/coqtop process. - 7. Then you can: - - step over function calls: - - step into function calls: - - or finish execution of the current function until it returns: . - -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 5b372c96c..000000000 --- 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](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](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). - -- cgit v1.2.3