aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/ide
Commit message (Collapse)AuthorAge
* Introduce an option to allow nested lemma, and turn it off by default.Gravatar Théo Zimmermann2018-05-17
|
* Merge PR #7090: stm: don't propagate side effects when editing a proofGravatar Emilio Jesus Gallego Arias2018-03-28
|\
| * stm: don't propagate side effects when editing a proofGravatar Enrico Tassi2018-03-27
| |
* | [test-suite] Add backtracking test for `Load`.Gravatar Emilio Jesus Gallego Arias2018-03-10
|/ | | | Closes #6793.
* Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
* Farewell decl_modeGravatar Enrico Tassi2017-03-07
| | | | | This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
* Moving the parsing of the Ltac proof mode to G_ltac.Gravatar Pierre-Marie Pédrot2016-03-19
|
* STM: states coming from workers have no proof terminators (Close #4246)Gravatar Enrico Tassi2015-06-09
| | | | Hence we reuse the ones in master.
* STM: silly mistake in jumping back to an old state (Close #4249)Gravatar Enrico Tassi2015-06-09
|
* STM: preserve branch name on edit (Close: #4245, #4246)Gravatar Enrico Tassi2015-05-28
|
* Test for 4159Gravatar Enrico Tassi2015-05-28
|
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
| | | | | | | | | | | | | | | - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
* Future: blocking by defaultGravatar Enrico Tassi2014-12-17
| | | | | | This makes queries like Print or Extraction block and not raise the error "the value is not ready". This should make CoqIDE work for every kind of script.
* fake_ide: ported to spawnGravatar Enrico Tassi2014-02-10
|
* Document: undoing inside a focused zone does not require unfocusingGravatar gareuselesinge2013-10-10
| | | | | | | | | | | | | To test this fake_ide has also been improved with the GOALS command. As for CoqIDE, ADDing a sentence does not force its evaluation. The "advance 1 sentence" button is an ADD + GOALS. If one of the ADDed sentences is wrong, GOALS receives the error. The GUI then backtracks to a safe state id (sent by Coq). fake_ide has GOALS (asserts that the goals call was OK) and FAILGOALS to assert it fails and backtrack to a valid state. see unfdo022.fake. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16873 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide: ported to Document + 2 tests for editing a proof (locally)Gravatar gareuselesinge2013-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16871 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide: speak the new protocolGravatar gareuselesinge2013-10-07
| | | | | | | | | A new syntax for .fake files, allowing multi line phrases and labeled script points (to go back to them). Test 7 fails because of a bug in STM (in a very spaghetti-like script). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16860 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide ported to STMGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | Main changes for STM: 1) protocol changed to carry edit/state ids 2) colouring reflects the actual status of every span (evaluated or not) 3) button to force the evaluation of the whole buffer 4) cmd_stack and backtracking completely changed to use state numbers instead of counting sentences 5) feedback messages are completely asynchronous, and the whole protocol could be made so with a minor effort, but there is little point in it right now. Left as a future improvement. Missing bit: add sentence-id to responses of interp command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7
* test-suite/ide: misc improvementGravatar letouzey2011-09-06
| | | | | | | - make clean really erases *.log - some missing \n at end of files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14460 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide: a short program to mimic an ide talking to coqtop -ideslaveGravatar letouzey2011-09-05
| | | | | | | | This way, we can test each night that coqtop -ideslave handles correctly some specific sequences of API calls. For the moment, we add a few tests of the backtracking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14456 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introducing strong typing for IDE - toplevel IPCGravatar vgross2010-05-31
| | | | | | Obj.magic in toplevel/ide_blob.ml is the only way to simulate GADT. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13041 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in backtracking.Gravatar vgross2010-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12876 85f007b7-540e-0410-9357-904b9bb8a0f7
* New backtracking code + fix bug #2082.Gravatar vgross2010-02-26
| | | | | | Previous code checkings were too lax, and information was lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12823 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction bug highlighting "Module" dans CoqideGravatar herbelin2008-05-28
| | | | | | | | | - Divers code mort (evarutil.ml, Bvector.v) - MAJ perf-analysis git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11004 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bugs ide undo et highlight (suite à typos)Gravatar herbelin2008-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Léger backtrack sur commit coqide précédent (si la commande à annulerGravatar herbelin2008-05-20
| | | | | | | | | à potentiellement modifié l'état, on ne peut se contenter d'un Abort : il faut revenir au dernier état connu). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10951 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed coqide bug #1856 that was introduced in revision 10915.Gravatar herbelin2008-05-20
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10950 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 12:52:04 +0000