aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.ml
Commit message (Collapse)AuthorAge
...
* Tentative heuristic fix to handle lexer failures from CoqIDE whenGravatar ppedrot2013-02-22
| | | | | | cutting XML phrases carelessly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16238 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monadification of coqtop queries in CoqIDEGravatar ppedrot2013-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16150 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformization of Coq tasksGravatar ppedrot2013-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16149 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: avoid potentially blocking read on coqtop channelGravatar letouzey2013-01-22
| | | | | | | | | | | | | | | | | | 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
* Coqide: cleaner Coq.PrintOpt and session creationGravatar letouzey2012-12-19
| | | | | | | | | | | 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
* Coqide: handle possible fragmentation in xml answersGravatar letouzey2012-12-08
| | | | | | | | | 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
* Coqide: get rid of threads, use gtk asynchronous i/o insteadGravatar letouzey2012-12-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Coqide : allow properly closing communication pipes with coqtopGravatar letouzey2012-11-12
| | | | | | | | | | | | | 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
* More type-safe interface to Coq XML API.Gravatar ppedrot2012-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15813 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various small display improvementGravatar ppedrot2012-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Now CoqIDE separates answer and messages. This should hopefullyGravatar ppedrot2012-06-29
| | | | | | be backward compatible... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15501 85f007b7-540e-0410-9357-904b9bb8a0f7
* Now CoqIDE auto-sets the printing width of the goal display.Gravatar ppedrot2012-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15494 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaned prerr_endline use.Gravatar ppedrot2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15354 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: minor formatting improvement of an error messageGravatar letouzey2012-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15329 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: in win32 command given to cmd.exe should be more quotedGravatar letouzey2012-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15328 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: display initial connection errors in popups instead of on stderrGravatar letouzey2012-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added semantic completion in CoqIDE. (Should also add an option for that...)Gravatar ppedrot2012-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15317 85f007b7-540e-0410-9357-904b9bb8a0f7
* Heavily rewritten the coqtop management process of coqide. The coqtopGravatar ppedrot2012-05-13
| | | | | | | | | | 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
* Coqide awful coqtop options parsing fixupGravatar pboutill2012-05-11
| | | | | | (back to the future) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15301 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed the useless use of a reference in preference handling.Gravatar ppedrot2012-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15271 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: the coqtop to launch is a preference.Gravatar pboutill2012-04-17
| | | | | | | 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
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
| | | | | | | | | | | | | | | - 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
* CoqIde files position is freedesktop compliant.Gravatar pboutill2011-12-18
| | | | | | | 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
* Cleaned up a bit goal handling in Coqtop interface. Now we have two queries ↵Gravatar ppedrot2011-12-15
| | | | | | : 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
* Fixed a bug introduced in r12755. CoqIDE would ignore the Printing ↵Gravatar ppedrot2011-11-30
| | | | | | 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
* Now CoqIDE relies on the option query mechanism to set printing options. ↵Gravatar ppedrot2011-11-30
| | | | | | Still a bit hackish. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14754 85f007b7-540e-0410-9357-904b9bb8a0f7
* Separated the toplevel interface into a purely declarative module with ↵Gravatar ppedrot2011-11-25
| | | | | | 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
* Return of the tactic hints features in CoqIDE.Gravatar ppedrot2011-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14687 85f007b7-540e-0410-9357-904b9bb8a0f7
* Also sprach CoqIDE (in XML)Gravatar ppedrot2011-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14637 85f007b7-540e-0410-9357-904b9bb8a0f7
* In Coq_config: get rid of coqsrc and make coqlib optionalGravatar glondu2011-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Ide_intf: slight reorganisation of the IDE apiGravatar letouzey2011-09-05
| | | | | | | | - 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
* safe_prerr_endline in MinilibGravatar pboutill2011-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14442 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: try to properly send interrupts to coqtop on Win32Gravatar letouzey2011-04-28
| | | | | | | | | | | | | | | 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
* Coqide: let's try to be synchronuous when killing coqtopGravatar letouzey2011-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqlib: avoid deadlock under win32 with force_reset_initialGravatar letouzey2011-04-21
| | | | | | | | | | | | 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
* Coqide: back to using Unix.stderr in create_processGravatar letouzey2011-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14048 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: better handling of stdout/stderr in win32Gravatar letouzey2011-04-21
| | | | | | | | | | | | | | | | | | 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
* Coqide: quote coqtop filename if necessaryGravatar letouzey2011-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14045 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: a special kill function for win32Gravatar letouzey2011-04-21
| | | | | | | | | | | | 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
* Coqide: try to avoid displaying error messages on coqide's consoleGravatar letouzey2011-04-21
| | | | | | | | | 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
* Win32: if we make coqide console-free, then stderr/stdout/sdtin shouldn't be ↵Gravatar letouzey2011-04-21
| | | | | | | | | | | | | | | | | | | | | | 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
* Coqide: avoid confusion of process when restarting coqtop + cosmeticGravatar letouzey2011-03-30
| | | | | | | | | | | | | | | | | | | 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
* Ide_slave: better handling of Ctrl-CGravatar letouzey2011-03-30
| | | | | | | | | - 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
* Ide: misc (nicer message than End_of_file, a useless try removedGravatar letouzey2011-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13935 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: new option -coqtop <mycoqtop> + remove wrong quoting of argsGravatar letouzey2011-03-28
| | | | | | | | | | | | | * Run "coqide -coqtop someothercoqtop" if you want to use a toplevel which isn't the one coming alongside coqide. To be documented, to be improved (maybe an field in coqide's preferences ?). coqide -h should display this kind of ide-specific option. * Since we now use create_process instead of open_process, we don't use /bin/sh, hence running Filename.quote on args was actually wrong. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13932 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: more reorganisation and cleanupGravatar letouzey2011-03-25
| | | | | | | | | | | | | | | | | | | - Avoid using Util which depends on Compat and hence Camlp4 - Instead, a small Minilib module specific to coqide, which duplicate 5 functions from Util (50 lines) - some dead code removal - the coqlib variable is asked to coqtop - remove obsolete Util.check_for_interrupt This way, coqide only depends on 3 files outside ide/ : Coq_config, Flags, Ide_intf. Makefile and ocamlbuild are adapted accordingly. TODO: how should we signal coqide error, warnings, etc ? For the moment, some Printf.eprintf, some failwith. To uniformize later... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide_intf : change type of location in ideGravatar letouzey2011-03-25
| | | | | | | We use (int * int) option instead of Loc.t, it's easier to use later in coqide, and this way we do not depend on camlp4,5 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13929 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: stronger separation from coqtopGravatar letouzey2011-03-23
| | | | | | | | | | | | | | | Former module Ide_blob is now divided in Ide_intf (linked both by coqtop and coqide) and Ide_slave (now only in coqtop). Ide_intf has almost no dependencies, we can now compile coqide with only coq_config.cm* and lib.cm(x)a TODO: - Devise a better way to display whether coqide is byte or opt in the about message (instead of Mltop.is_native, I display now the executable name, which hopefully contains opt or byte) - Check the late error handling in ide/coq.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13927 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: experimentally allow coqide to interrupt or kill coqtopGravatar letouzey2011-03-23
| | | | | | | | | | | | | | | | | | | | | | | - We now use create_process instead of open_process, and stores the answered pid. - The "Stop" button now sends a Sigint signal to this coqtop pid. - The "Goto Start" button now works even if a computation is ongoing, a new process is spawned and the previous one is killed -9, and then a waitpid is done to avoid having zombies around. Note that currently a vm_compute won't be stopped by a "Stop", but only by a "Goto Start". This can be quite confusing. How to properly document that "Goto Start" has the side effect of being a kill ? Maybe we could check someday if the Ctrl-C has been successful, and kill -9 if not ? Or maybe make coqide aware of a flag "we_are_vm_computing" and then kill -9 instead of Ctrl-C in this case ? TODO: - for the moment a forced "Goto Start" displays an unfriendly anomaly - check if all this works under Windows (probably but not sure). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13926 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 04:24:02 +0000