| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
Instead of relaunching the coqtop process and then open the warning window,
we rather fire the warning and wait for the user to press the OK button before
doing anything.
|
| |
|
| |
|
| |
|
|
|
|
| |
reports errors also from stderr.
|
|
|
|
| |
coqide --help.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
lib/interface split into:
- lib/feedback
subscribe-based feedback bus (also used by coqidetop)
- ide/interface
definition of coqide protocol messages
lib/pp
structured info/err/warn messages
lib/serialize split into:
- lib/serialize
generic xml serialization (list, pairs, int, loc, ...)
used by coqide but potentially useful to other interfaces
- ide/xmlprotocol
serialization of protocol messages as in ide/interface
the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Stm used to delegate every proof when it was possible, but this may
be a bad idea. Small proofs may take less time than the overhead
delegation implies (marshalling, etc...).
Now it delegates only proofs that take >= 1 second.
By default a proof takes 1 second (that may be wrong).
If the file was compiled before, it reuses the data stored in the .aux
file and assumes the timings are still valid.
After a proof is checked, Coq knows how long it takes for real, so it
wont predict it wrong again (when the user goes up and down in the
file for example).
CoqIDE now sends to Coq, as part of the init message, the file name
so that Coq can load the .aux file.
|
| |
|
| |
|
| |
|
|
|
|
| |
Like the socket for the OCaml debugger
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
-async-proofs off
the system behaves as in 8.4
-async-proofs lazy
proofs are delayed (when possible) but never processed in parallel
-async-proofs on
proofs are processed in parallel (when possible). The number of
workers is 1, can be changed with -async-proofs-j. Extra options to
the worker process can be given with -async-proofs-worker-flags.
The default for batch compilation used to be "lazy", now it is "off".
The "lazy" default was there to test the machinery, but it makes very
little sense in a batch scenario. If you process things sequentially,
you'd better do them immediately instead of accumulating everything in
memory until the end of the file and only then force all lazy computations.
The default for -ideslave was and still is "on". It becomes dynamically
"lazy" on a per task (proof) basis if the worker dies badly.
Note that by passing "-async-proofs on" to coqc one can produce a .vo
exploiting multiple workers. But this is rarely profitable given
that master-to-worker communication is inefficient (i.e. it really
depends on the size of proofs v.s. size of system state).
|
|
|
|
| |
We use the win32 specific function only if WIN32 is defined
|
| |
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16826 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
|
|
| |
arguments.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16761 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Stm contains many TODO items to improve the thing, but it should
be already possible to play with it (but not use it in production).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16684 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16636 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Code for printing XML moved from xml_utils.ml to xml_printer.ml
and improved to generate less garbage using Buffer.t systematically.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16480 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This amounts to a new type of message called "feedback" and defined in
Interface to hold structured data. Coq sends feedback messages
asynchronously (they are all fetched, like regular messages, together
with the main response to a call) and they are related to a specific
sentence by an id.
Other changes:
- CoqOps pushes the sentence to be processed onto the cmd_stack
before processing it and pulls it back if Coq.intep fails, in this way
the handler for feedback messages can just look at the cmd_stack
to find the offset of the sentence to eventually apply the new Gtk.tag.
- The class coqops takes in input a coqtop to set its feedback_handle.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16451 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
With this commit the types involved in the protocol between Coq and
Coqide are written once and for all in interface.mli
serialize.ml is monkey code that contains a reified version of these
types and the related machinery needed to marshal values in these types
to/from xml in a modular way. This file should be automatically
generated from the spec of the protocol in an ideal world.
Phantom types are used to statically check that the reified form
of the types is in sync with the one declared in interface.mli
The benefit of this commit is that changing the protocol is easier:
one changes the types in interface.mli and lets ocamlc spot all the
places that needs to be modified.
This is a necessity if one plays with the protocol very often, like
in my Paral-ITP branch.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16438 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
cutting XML phrases carelessly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16238 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16150 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16149 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
With Pierre-Marie, we discovered the hard way that Glib.Io reads
are *not* non-blocking by default as I thought. My bad...
This was causing nasty freezes of coqide in the rare cases where
the final read was exactly filling the buffer (which was of size 1024).
Now:
- the input channels from coqtop (and various other external commands)
are given to Unix.set_nonblock
- Exceptions in our io_read_all (typically a kind of EAGAIN) terminate
the read
- We can now switch to Glib.Io.read_chars instead of the deprecated
Glib.Io.read.
- Btw, we use a larger buffer (8192).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16138 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
PrintOpt.set now only updates the state Hashtbl of options,
a PrintOpt.enforce is mandatory to transmit them to coqtop.
This enforce is done for instance by Coq.goals.
The various signal handlers about coqide's buffer are now installed
in session creation, and not anymore via the coqops initializer.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16105 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
Experimentally, this occurs at least in win32 when sending commands
quickly enough: one handle_input callback received only a part of an xml
answer, the rest was available only during the next handle_input.
So we store unterminated xml fragments across handle_input invocations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16050 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Threads were only there to handle blocking dialogs with the different
coqtops. But programming with threads have drawbacks : complex mutex
infrastructure, possible deadlocks, etc. In particular gtk functions
are not meant to be called from a thread which isn't the gtk main loop,
(unless some gtk mutex have been taken). This seem to pose problem
specifically in win32 (and macosx ?), hence the use of the
GtkThread.(a)sync hack for scheduling code for execution in the gtk
main loop.
Instead, we now use the Glib.Io module to install a callback that will
be runned when some answer of coqtop is available on the channel.
This implies using now a continuation-passing style: for instance,
instead of two sequential requests to coqtop, we'll now have the
2nd request inside the callback handling the answer to the 1st request.
Remarks:
- Also use asynchronous i/o for external commands (editor, coqc, make...).
Launching an external editor or browser won't freeze coqide anymore.
- Reworked handling of coqtop process, especially when closing them.
A responsive coqtop should now hara-kiri immediatly when its input
channel is closed. Otherwise we try later a soft kill, then some
hard kills if necessary. If nothing work we warns the user.
When quitting coqide, all this might induce a small delay (2s at worse).
- Be careful now to avoid "long" computations (or blocking i/o) in
a coqide function. Experimentally, it seems that loading/saving a .v
file is quick enough. If necessary, we could use asynchronous i/o
also for writing the .v, but for loading I've no clue.
- In the Coqide module, we ensure that the current continuation k
will indeed be run at the end thanks to an abstract return type
(void = opaque copy of unit).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16049 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
NB: it's important to close coqide's descriptors (ide2top_w and top2ide_r)
in coqtop. We do this indirectly via [Unix.set_close_on_exec].
This way, coqide has the only remaining copies of these descriptors,
and closing them later will have visible effects in coqtop. Cf man 7 pipe
for more details.
This should avoid the need for Unix.kill on coqtop clients (at least
when they aren't inside a long computation).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15961 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15813 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15505 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
be backward compatible...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15501 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15494 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15354 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15329 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15328 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15325 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15317 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
object is now responsible for restarting itself, and handles unexpected
crashes. Fixes a lot of errors in file descriptor management, but may
introduce lurking deadlocks and nasty bugs waiting to be discovered.
Only (quickly) tested under Linux, any callbacks from Windows are welcome.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15314 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
(back to the future)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15301 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15271 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
If it is AUTO then we keep the heuristic to change coqide by coqtop in Sys.executable_name.
If it fails coqtop location must be given by the users.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15188 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Clib that does not depend on camlpX and is made to be shared by all coq
tools/scripts/...
- Lib that is Coqtop specific
As a side effect for the build system :
- Coq_config is in Clib and does not appears in makefiles
- only the BEST version of coqc and coqmktop is made
- ocamlbuild build system fails latter but is still broken
(ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
|