From 9a14a95f96c77ff3850d694637738358c164f4b5 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 8 Jun 2017 11:17:22 +0200 Subject: Normalize deprecation notices of ./configure Always output a warning on stderr when a deprecated option is used. --- dev/doc/setup.txt | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'dev/doc') diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 1b016a4e26..0c6d3ee80d 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -12,7 +12,7 @@ How to compile Coq Getting build dependencies: - sudo apt-get install make opam git mercurial darcs + 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. @@ -41,7 +41,7 @@ Building coqtop: cd ~/git/coq git checkout trunk make distclean - ./configure -annotate -with-doc no -local -debug -usecamlp5 + ./configure -annotate -local make clean make -j4 coqide printers @@ -49,8 +49,6 @@ The "-annotate" option is essential when one wants to use Merlin. The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install -The "-debug" option is essential if one wants to use ocamldebug with the coqtop binary. - Then check if - bin/coqtop - bin/coqide @@ -60,7 +58,7 @@ behave as expected. A note about rlwrap ------------------- -Running "coqtop" under "rlwrap" is possible, but there is a catch. If you try: +Running "coqtop" under "rlwrap" is possible, but (on Debian) there is a catch. If you try: cd ~/git/coq rlwrap bin/coqtop -- cgit v1.2.3 From 3cfb38cb0e5491d13a6ef5cda81dfec7f979cced Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 9 May 2017 17:28:23 +0200 Subject: Documenting the change of default flag value of Refine.refine. --- dev/doc/changes.txt | 3 +++ 1 file changed, 3 insertions(+) (limited to 'dev/doc') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index bcda4ff50a..8456195e6b 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -144,6 +144,9 @@ In Coqlib / reference location: - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase was very specific. Use tclPROGRESS instead. +- The Refine.refine function and its variants now have the unsafe flag turned + down by default. + ** Ltac API ** Many Ltac specific API has been moved in its own ltac/ folder. Amongst other -- cgit v1.2.3 From 0fad09306982a88ff8d633d36abdc440dd542ab3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 13 Jun 2017 10:33:56 +0200 Subject: Dualize the unsafe flag of refine into typecheck and make it mandatory. --- dev/doc/changes.txt | 4 ++-- dev/doc/proof-engine.md | 7 +++---- 2 files changed, 5 insertions(+), 6 deletions(-) (limited to 'dev/doc') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 8456195e6b..63c064d843 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -144,8 +144,8 @@ In Coqlib / reference location: - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase was very specific. Use tclPROGRESS instead. -- The Refine.refine function and its variants now have the unsafe flag turned - down by default. +- The unsafe flag of the Refine.refine function and its variants has been + renamed and dualized into typecheck and has been made mandatory. ** Ltac API ** diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md index db69b08a20..8f96ac223f 100644 --- a/dev/doc/proof-engine.md +++ b/dev/doc/proof-engine.md @@ -42,14 +42,13 @@ goal holes thanks to the `Refine` module, and in particular to the `Refine.refine` primitive. ```ocaml -val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic -(** In [refine ?unsafe t], [t] is a term with holes under some +val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic +(** In [refine typecheck t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions raised during the interpretation of [t] are caught and result in - tactic failures. If [unsafe] is [false] (default is [true]) [t] is - type-checked beforehand. *) + tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) ``` In a first approximation, we can think of `'a Sigma.run` as -- cgit v1.2.3 From d8874dd855d748aaaf504890487ab15ffd7a677d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 11:41:40 +0200 Subject: [ide] Add route_id parameter to query call. This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####. --- dev/doc/changes.txt | 4 ++++ dev/doc/xml-protocol.md | 9 +++++++-- 2 files changed, 11 insertions(+), 2 deletions(-) (limited to 'dev/doc') diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 0728608f31..159be9a582 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -288,6 +288,10 @@ document type". This allows for a more uniform handling of printing - The legacy `Interp` call has been turned into a noop. +- The `query` call has been modified, now it carries a mandatory + "route_id" integer parameter, that associated the result of such + query with its generated feedback. + ========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 2ff82c6888..127b4a6d2d 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -308,15 +308,20 @@ CoqIDE typically sets `force` to `false`. ------------------------------- +### **Query(route_id: integer, query: string, stateId: integer)** + +`routeId` can be used to distinguish the result of a particular query, +`stateId` should be set to the state the query should be run. -### **Query(query: string, stateId: integer)** -In practice, `stateId` is 0, but the effect is to perform the query on the currently-focused state. ```html + + ${query} + ``` #### *Returns* -- cgit v1.2.3