| Commit message (Collapse) | Author | Age |
|
|
|
| |
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
|
|
|
|
|
|
|
| |
Beware, it means that files position is not relative to coqtop position
but is given by XDG_DATA_DIRS and XDG_CONFIG_DIRS.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14822 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
: goal description, with focused and unfocused goals, and list of currently declared evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14793 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Existential Instances options because it was ill-formed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14756 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Still a bit hackish.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14754 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
associated types (interface.mli), and an applicative part processing the calls (previous ide_intf).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14730 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14687 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14637 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
I assume that once Coq is installed in non-local mode and run from its
installed path, sources are no longer available. The coqsrc variable
doesn't make any sense, then, and its intended value can always be
inferred from Sys.executable_name. Moving it to Envars.coqroot.
Make coqlib optional. Currently, it is set to None only in -local mode
or with ocamlbuild. When set to None, -local layout is assumed
(binaries in ./bin, library in .). The behaviour should not be changed
when an explicit coqlib has been given to ./configure.
This commit should make it possible to run a Coq compiled with -local
from anywhere (no hard-coded absolute path embedded in the
executables, intermediary step to bug #2565). It WILL BREAK settings
re-using source trees after installation in non-local mode (are there
actual use cases for that?).
Hard-coded absolute paths still remain:
- in the build system, so the need to re-run ./configure after moving
the source tree is still expected for now;
- in coqrunbyteflags, I think we are limited by ocaml itself;
- docdir.
All absolute paths should be removed, ultimately.
As a side-effect, simplify computing of Envars.coqbin. I don't see any
good reason to keep it as a function.
Disclaimers:
- initialization of Sys.executable_name is not consistent across all
architectures; relying so much on it might trigger bugs. I'm pretty
sure something will explode if one adds arbitrary symlinks on top of
that;
- ocamlbuild stuff not tested.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
- merge raw_interp with interp (with one more flag)
- merge read_stdout with interp, which now return a string
- shorter command names
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14454 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14442 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We use GenerateConsoleCtrlEvent(CTRL_C_EVENT,...) after having
attached coqide to the console of the coqtop we want to interrupt.
Two caveats:
- This code isn't compatible with Windows < XP SP1.
- It relies on the fact that coqide is now a true GUI app, without
console by default. If for some reason the console of coqide is
restored (for instance via mkwinapp -unset), strange behavior
of the interrupt button is to be expected, at the very least all
instances of coqtop will get Ctrl-C instead of a precise one.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14077 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14051 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
The force_reset_initial starts by killing coqtop, then it tries
to acquire the lock on coq_computing. If it works, no jobs are
pending, we do the real reset_initial (launch of a new coqtop +
removal of buffer coloring) ourself.
Otherwise, the function do_if_not_computing is running, the death
of coqtop will raise a RestartCoqtop exception there, triggering
a reset_initial.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14049 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14048 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Now that coqide is a console-free win32 app, writing to
nonexistent stdout/stderr lead to Sys_error. To avoid that:
- We reroute coqide's stdout/stderr to either a pipe that will stay
unread (by default), or to a temp log file (in debug mode).
- When doing create_process, avoid referring to Unix.stderr:
anything printed by coqtop to its stderr will be merged in the
regular channel.
- On the coqtop side, remove the awkward fix consisting in a \r printed
on stderr apparently to fix coqide.byte. This fix is probably obsolete
since the separation of coqide and coqtop as distinct processes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14047 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14045 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is implemented as a C external launching the TerminateProcess
of the Win32 API. This should be considered as quite experimental
(cf. the way we handle pid in the comment of ide_win32_stubs.c).
I don't know how to emulate an interrupt (Ctrl-C), for now the two
button "Restart" and "Interrupt" have the same semantics on win32
(kill the subprocess and start at top).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14044 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
In Win32, these messages may trigger some Sys_error if we try to
turn coqide into a true windows app (no console). To be continued...
The best way would be probably to re-route the whole stdout and stderr
to something else via dup2, but to what ? A log file ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14043 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
used
This is an adaptation of commit r13751 of branch 8.3
Even if coqide.exe keeps its console by default for the moment,
we try to allow turning it off (for instance via the mkwinapp tool) :
for that we need to be cautious about the use of functions
like prerr_endline. Since stderr doesn't exists in this settings,
such functions trigger a Sys_error "bad file descriptor".
This patch protects many access to std** by a (try ... with _ ->()).
Nota: with camlp5 < 6.02.1, Print Grammar was also generating
such a Sys_error.
TODO: we should try to figure a way of displaying messages (both
debug and early/late error message). A log file ? A popup ?
diplay in the response buffer ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When using "Goto start" while many phrases are evaluated,
it's frequent with earlier code that the restart occurs
between two phrases, and hence the second is sent to the new
coqtop, triggering things like "Anomaly: NoCurrentProof".
To avoid that, Coq.coqtop is now immutable (no silent switch
of channels). In Coqide, toplvl and mycoqtop are now references,
that are updated when using reset_coqtop.
We organize things in order to have only one access to mycoqtop
during code that does many sequential calls to coqtop. This way,
when coqtop changes, the code speaks to the old one, and gets
some exception when writing/reading on a close channel.
By the way, some documentation, cleanup, etc etc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13942 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- During input and output to coqide, we postpone Ctrl-C instead of ignoring
them. For that we use Util.interrupt and Util.check_for_interrupt.
- During evaluation of coqide requests, a Ctrl-C directly raises Sys.break,
which is more reliable than waiting for the next Util.check_for_interrupt
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13935 85f007b7-540e-0410-9357-904b9bb8a0f7
|