aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Remove some uses of local modules (some were unused, some were costly).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16883 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of the use of deprecated elements (from the OCaml standard library).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: make error background configurableGravatar gareuselesinge2013-10-11
| | | | | | #FFCCCC is quite dark on some beamers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16881 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: prefix debug messages with slave-idGravatar gareuselesinge2013-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16880 85f007b7-540e-0410-9357-904b9bb8a0f7
* More comments in ide_slaveGravatar gareuselesinge2013-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16879 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: cancel slaves working on outdated jobsGravatar gareuselesinge2013-10-11
| | | | | | | | | | | | | | | | | | | | | | | | | I did not manage to make the slave manager use Unix.select to wait for a response from the slave for a limited time and check for cancellation. Hence the following semi-cooperative model: - The slave has a thread that sends a Tick every second when the thread is working - The slave_manager will then be unblocked periodically by this tick and check for cancellation - Cancellation is, for the moment, implemented using kill. To kill a process on windows one could bind TerminateProcess (>= WinXP) or RegisterWindowMessage + BroadcastSystemMessage (>= Win2k). See: http://msdn.microsoft.com/en-us/library/windows/desktop/ms686722%28v=vs.85%29.aspx Another option is to make the slave_manager send to the tick thread on the slave process a boolean answer to the Tick message, and the tick thread could eventually bail out. But to do that, it is way better to have a second channel, used only by this tick thread. This solution sound very like the one proposed for windows, but requires more work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16878 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vcs: the gc method returns the set of nodes that were collectedGravatar gareuselesinge2013-10-11
| | | | | | | In this way one can post-process them. Stm can for example cancel the ongoing jobs related to nodes that are no more there. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dag: some comments on the concept of clusterGravatar gareuselesinge2013-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16876 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: single underline for errorsGravatar gareuselesinge2013-10-11
| | | | | | | The double underline has some bugs, sometimes the lower line is not correctly cleared. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16875 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: error reporting fixedGravatar gareuselesinge2013-10-10
| | | | | | | | | Many things were wrong. Error tags were deleted by mistake, the screen was recentered on `INSERT using the wrong function (that cause some horizontal scrolling even if it was not needed), the cursor not advanced to the end of the wrong sentence. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16874 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* CoqIDE: ported to DocumentGravatar gareuselesinge2013-10-10
| | | | | | | | The code is simpler, but there is still room for improvement. In particular find_id (implemented in both coqOps and fake_id) should be part of Document. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16872 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
* CoqIDE: move cmd_stack to a separate module: DocumentGravatar gareuselesinge2013-10-10
| | | | | | | | The idea is to move the logic related to document handling to a separate module that can be tested by fake_ide too. CoqOps should "only" interface Document with the GtkTextBuffer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16870 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: a proof with nested proofs cannot be delegatedGravatar gareuselesinge2013-10-10
| | | | | | | | | The reason is that the state gets altered by side effects by the Qed of inner proofs. This kind of side effects cannot be reproduced in the slaves easily. And there is no point in working hard for this corner case. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16869 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: add "Stm Wait" to wait for the slaves to complete their jobsGravatar gareuselesinge2013-10-10
| | | | | | | Used by fake_ide, that before editing a broken proof has to be sure Coq known the proof is broken. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16868 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clib: fold_left_until added to CListGravatar gareuselesinge2013-10-10
| | | | | | | CStack just calls it to implement fold_until. CSig.seek renamed CSig.until, since there is no seek function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16867 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: a comment is not a sentenceGravatar gareuselesinge2013-10-10
| | | | | | | | | | | | | | | | | | | | | This simplifies the whole document business: the document on the Coq side has the very same nodes as the CoqIDE document, there are no "fake" nodes in the CoqIDE document to be skipped over. We keep the comment tag stamped by the coq_lexer module, since we may want to allow edits in there without telling Coq (as proof general does). Not implemented yet, but doable thanks to the comment tag. Pierre Boutillier suggested that this makes back-1-sentence ugly, since it moves the cursor far away if the sentence begins with a comment. While this is true, *today*, there is no need to undo the last sentence with the button to edit the text. One can just move the cursor where he likes and edit. In this case the sentence is backtracked automatically and the cursor is left where it is. Hence considering initial comments as part of the following sentence should not be an usability issue anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16866 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing CAMLP4 compilation.Gravatar ppedrot2013-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16865 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small code cleaning in Evarutil.Gravatar ppedrot2013-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16864 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing 2 output test-suites.Gravatar ppedrot2013-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16863 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: new command "Stm PrintDag" to force printing the dag to /tmpGravatar gareuselesinge2013-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16862 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: fix verbosity of queriesGravatar gareuselesinge2013-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16861 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
* STM: spit a warning if an out of bound Back* command is issuedGravatar gareuselesinge2013-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16859 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqtop: init STM before loading rcfileGravatar gareuselesinge2013-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16858 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: fix jumpig out of a focused proofGravatar gareuselesinge2013-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16857 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: cStack -> DocumentGravatar gareuselesinge2013-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16856 85f007b7-540e-0410-9357-904b9bb8a0f7
* cStack: make it just a Stack with some extra APIGravatar gareuselesinge2013-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16855 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless evar code.Gravatar ppedrot2013-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16854 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a [modify] function to maps.Gravatar ppedrot2013-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16853 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing uses of Evar.add in class-related functions.Gravatar ppedrot2013-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16852 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing dubious use of evarmap manipulating functions in printingGravatar ppedrot2013-10-05
| | | | | | related code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
| | | | | | | | | | | | | | | | | | | state out of one we were threading all the way along. This should be safer, as one cannot forego side effects accidentally by manipulating explicitly the [sigma] container. Still, this patch raised the issue of badly used evar maps. There is an ad-hoc workaround (i.e. a hack) in Rewrite to handle the fact it uses evar maps in an unorthodox way. Likewise, that mean we have to revert all contrib patches that added effect threading... There was also a dubious use of side effects in their toplevel handling, that duplicates them, leading to the need of a rather unsafe List.uniquize afterwards. It should be investigaged. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16850 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing potential evar leak in Rewrite, and removing dead code.Gravatar ppedrot2013-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16849 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing potential evar leak in Equality.Gravatar ppedrot2013-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16848 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitting Class_tactics between code and CAMLP4/5 declarations.Gravatar ppedrot2013-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16847 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix comment for new string syntax (OCaml trunk).Gravatar xclerc2013-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16846 85f007b7-540e-0410-9357-904b9bb8a0f7
* A shallow copy of a pre_env does not contain the vm cacheGravatar gareuselesinge2013-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16845 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: understand -coq-slaves-opts extra-env=VAR=valGravatar gareuselesinge2013-10-03
| | | | | | | In this way one can set an env variable for the slave, like the socket used by ocamldebug to talk remotely to a process git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16844 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: if -coq-slaves off really imitate the old CoqIDEGravatar gareuselesinge2013-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16843 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: when jumping to an error also move the cursorGravatar gareuselesinge2013-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16842 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: add options to disable fallbacks to ease regression testingGravatar gareuselesinge2013-10-03
| | | | | | | | | | STM falls back to local, lazy, evaluation if the slave dies badly or if there is a marshalling error. Both things should never occur, but is nice to have the system recover if a bug pops up. Nevertheless during regression testing these fallbacks should be disabled not to hide a new bug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16841 85f007b7-540e-0410-9357-904b9bb8a0f7
* Regression test suite for STMGravatar gareuselesinge2013-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16840 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: number of slaves passed by the command lineGravatar gareuselesinge2013-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16839 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: avoid "kill 9 pid" if we know the slave diedGravatar gareuselesinge2013-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16838 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: delegate proofs to slaves only if they are not trivialGravatar gareuselesinge2013-10-03
| | | | | | Still too simple and not configurable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16837 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: take a shallow snapshot for the first proof stepGravatar gareuselesinge2013-10-03
| | | | | | this way it can be directly sent to a slave with no further manipulation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16836 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: when checking the whole document, center script view on errorGravatar gareuselesinge2013-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16835 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: fixed advance_until wrt unfocusingGravatar gareuselesinge2013-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16834 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 19:08:40 +0000