aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2013-10-03CoqIDE: when jumping to an error also move the cursorgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16842 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: add options to disable fallbacks to ease regression testinggareuselesinge
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
2013-10-03Regression test suite for STMgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16840 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: number of slaves passed by the command linegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16839 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: avoid "kill 9 pid" if we know the slave diedgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16838 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: delegate proofs to slaves only if they are not trivialgareuselesinge
Still too simple and not configurable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16837 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: take a shallow snapshot for the first proof stepgareuselesinge
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
2013-10-01CoqIDE: when checking the whole document, center script view on errorgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16835 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: fixed advance_until wrt unfocusinggareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16834 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01typogareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16833 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01demo file for paral-itpgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16832 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: do not print cmd_stack too oftengareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16831 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: fully force a proof ourput before sending it back to the mastergareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16830 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: better error messages in case of marshal failuregareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16829 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: fix reporting of ongoing tasksgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16828 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: exceptions caming from slaves are now localizedgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16827 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: do not fail hard if a message is asynchronousgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16826 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: Unix.kill can failgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16825 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: fix reset initialgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16824 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE: use #present to raise error windowgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16823 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30Backtrace.record_backtrace in CoqIDE toogareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16822 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE: wg_Tooltip removed, new tooltip handlinggareuselesinge
- tooltips are attached to sentences - to find the tooltip text one goes back until the first start of sentence mark, finds the corresponding sentence and displays the tooltip - focused editing does not invalidate tooltips this way, since the text, its tags and marks is moved around consistently git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16821 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30STM: better handle proof modesgareuselesinge
Proof modes are really spaghetti code. It is a global state that you can't access (held by G_vernac). We stick it to the branches... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16820 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30fake_ide: call Coq.init as the first actiongareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16819 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30ideutils: stock_to_widget was ignoring the ~size argumentgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16818 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30wg_Command: detachable, less "from the 80s", query panegareuselesinge
- Tabs have labels derived from the query (e.g. "About eq_ind" will have "eq_ind" as its label, that is better than "Page 1" ;-) - Tabs have a [x] close icon - Icon to create a new tab in in the notebook - Dispotically grab the F1 key to open/close the query pane (alt-esc is grabbed by windows managers these days) - Esc hides the query pane (like the search pane) - F1 puts a detached query pane in front - Tab switches from the combo-box to the entry on its right - Detaching is taken-over, and the query pane is reparented in a regular window that can be resized - A detached query pane can be put back by closing the window git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16817 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30wg_Session: fix copy/paste of tagged textgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16816 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30STM: some refactoring, support revised CoqIDE protocolgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16815 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE ported to the revides protocolgareuselesinge
- the zone to be edited is now between the marks start_of_input and stop_of_input - when -debug is given, the edit zone is underlined - the cmd_stack is focused/unfocused according to the new protocol - read only tag resurrected and used to block the "Qed" ending a focused zone git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16814 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30fake_ide ported to the new protocol (FIXME tests fail)gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16813 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE protocol/serialization revisedgareuselesinge
- both requests and responses are serialized using the same generic code - no more interp message. Replaced by: - query: performs a query (Search/Check...) at a given state - add: adds to the document a new sentence at the current edit point - edit_at: changes the edit point. the result could be a rewind _or_ a focus to a specific zone that can be edited without rewinding the whole document git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16812 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30lib/cstack: various improvementsgareuselesinge
- renaming reflecting the semantic of functions - ability to edit the stack at the top of a _focused_zone_ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16811 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30lib/vcs: various improvementsgareuselesinge
- gc function to clear unreferenced nodes - utility function to get the ancestors of a commit - utility function to edit a merge commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16810 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30lib/dag: various improvementsgareuselesinge
- clusters can hold some data - edges and nodes can be deleted git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16809 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30lib/future: computations that are Exn can be replacedgareuselesinge
A computation that is an exception morally holds no value hence can be replaced by an type-equivalent computation. This mechanism is used to edit broken proofs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16808 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-28Made rewrite tactic strategies pure. They were using quite uglilyppedrot
references. Now they carry around their state explicitly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16807 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-27Removing a bunch of generic equalities.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-26Opacifying the type of strategies.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16805 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-26Splitting Rewrite into a code part and a CAMLP4-dependent one.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16804 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-25Removing useless evar-related stuff.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16803 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-24Adding evar printing to debugger.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16802 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-24Fixing ocamldebug compilation by adding thread linking.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16801 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Fix name clash in "failure/inductive.v".xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16800 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16799 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-20Merge "inductive?.v" tests into a single "inductive.v" test.xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16798 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 06:50:34 +0000