aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
A future always carries a fix_exn with it: a function that enriches an exception with the state in which the error occurs and also a safe state close to it where one could backtrack. A future can be in two states: Ongoing or Finished. The latter state is obtained by Future.join and after that the future can be safely marshalled. An Ongoing future can be marshalled, but its value is lost. This makes it possible to send the environment to a slave process without pre-processing it to drop all unfinished proofs (they are dropped automatically in some sense). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-18Ephemeron: marshaling friendly keysgareuselesinge
Ideally all unmarshallable content in the state should be stocked using Ephemeron keys. In this way the state becomes always marshallable (because the unmarshallable content is magically dropped). The mli contains more detailed doc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16891 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-18Summary: if an unfreeze function fails, print an error messagegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16890 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-18STM: not optimize proofs containing an Undogareuselesinge
Actually we could, but we should check the state one jumps to is inside the proof... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16889 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-16Reintroduce "or" instead of "||" as the latter is redifined in "sos_lib.ml" ↵xclerc
with a different semantics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16888 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-14Some more hand-written comparison functions to avoid polymorphic comparison.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16887 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-14Avoid polymorphic comparison (plugins/rtauto).xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16886 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-14Avoid polymorphic comparison (plugins/cc).xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16885 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-14Avoid polymorphic comparison (coqdoc).xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16884 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-14Remove some uses of local modules (some were unused, some were costly).xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16883 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-14Getting rid of the use of deprecated elements (from the OCaml standard library).xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-11CoqIDE: make error background configurablegareuselesinge
#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
2013-10-11STM: prefix debug messages with slave-idgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16880 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-11More comments in ide_slavegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16879 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-11STM: cancel slaves working on outdated jobsgareuselesinge
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
2013-10-11Vcs: the gc method returns the set of nodes that were collectedgareuselesinge
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
2013-10-11Dag: some comments on the concept of clustergareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16876 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-11CoqIDE: single underline for errorsgareuselesinge
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
2013-10-10CoqIDE: error reporting fixedgareuselesinge
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
2013-10-10Document: undoing inside a focused zone does not require unfocusinggareuselesinge
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
2013-10-10CoqIDE: ported to Documentgareuselesinge
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
2013-10-10fake_ide: ported to Document + 2 tests for editing a proof (locally)gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16871 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-10CoqIDE: move cmd_stack to a separate module: Documentgareuselesinge
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
2013-10-10STM: a proof with nested proofs cannot be delegatedgareuselesinge
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
2013-10-10STM: add "Stm Wait" to wait for the slaves to complete their jobsgareuselesinge
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
2013-10-10Clib: fold_left_until added to CListgareuselesinge
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
2013-10-10CoqIDE: a comment is not a sentencegareuselesinge
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
2013-10-09Fixing CAMLP4 compilation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16865 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-08Small code cleaning in Evarutil.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16864 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-08Fixing 2 output test-suites.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16863 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07STM: new command "Stm PrintDag" to force printing the dag to /tmpgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16862 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07STM: fix verbosity of queriesgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16861 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07fake_ide: speak the new protocolgareuselesinge
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
2013-10-07STM: spit a warning if an out of bound Back* command is issuedgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16859 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07coqtop: init STM before loading rcfilegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16858 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07CoqIDE: fix jumpig out of a focused proofgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16857 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07CoqIDE: cStack -> Documentgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16856 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07cStack: make it just a Stack with some extra APIgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16855 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-06Removing useless evar code.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16854 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-06Added a [modify] function to maps.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16853 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-06Removing uses of Evar.add in class-related functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16852 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-05Removing dubious use of evarmap manipulating functions in printingppedrot
related code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16851 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
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
2013-10-05Fixing potential evar leak in Rewrite, and removing dead code.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16849 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-05Fixing potential evar leak in Equality.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16848 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-04Splitting Class_tactics between code and CAMLP4/5 declarations.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16847 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-04Fix comment for new string syntax (OCaml trunk).xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16846 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03A shallow copy of a pre_env does not contain the vm cachegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16845 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: understand -coq-slaves-opts extra-env=VAR=valgareuselesinge
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
2013-10-03STM: if -coq-slaves off really imitate the old CoqIDEgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16843 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:43:56 +0000