aboutsummaryrefslogtreecommitdiff
path: root/tools
AgeCommit message (Collapse)Author
2013-05-06fake_ide: xml parser does not check for EOFgareuselesinge
Exactly as Coqide's parser does. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16481 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-06New module Xml_printer (dual to Xml_parser)gareuselesinge
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
2013-04-25Coqide: new feedback mechanism for structured contentgareuselesinge
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
2013-04-19Fix compilation of fake_idegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16439 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-18coqc and coqmktop migrated in tools/, get rid of scripts/ subdirletouzey
No need to place these binaries apart, and anyway they aren't (shell) scripts since ages. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16432 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-18Coqdep: add an -exclude-dir option (wish mentionned in #3025)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16431 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
I hope I did not forget any place to change. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 15)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16292 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18use List.rev_map whenever possibleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22Revert "remove -rectypes except for term.ml"mdenes
Preparing landing of the native compiler, which requires -rectypes flag. This reverts commit f975575187d0a19e7cc1afc43459a92eeb12b3f1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16135 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-18I forget to use git log before git svn dcommit ...pboutill
Revert "Revert "coq_makefile: use coqdep instead of ocamldep on .ml4 files"" This reverts commit 7b9856f2eae3bd652d99864c9901f7c4af290323. The reason for my private revert is that coqdep does not find the dependencies of .ml4 files in AACTactics user-contrib correctly but it is a coqdep bug not a coq_makefile one ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16131 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-18Revert "coq_makefile: use coqdep instead of ocamldep on .ml4 files"pboutill
This reverts commit d14b9f6a017347e59cf037ff576f282785105080. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16128 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-07Coq_makefile: quoting pathspboutill
Global paths (binaries & install dir) are quoted, local paths are never ! From a patch by Jason Gross. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16119 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-07Coq_makefile: -extra & -phony-extra for user defined makefile rulepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16118 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-10Coq_makefile: Better rule for subdirs when the subdir does not existpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16056 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07Revert "* tools/Coq_makefile:"regisgia
This reverts commit 9a2f43eca179436f0581751b93c989fd30a5c13c. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16029 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07* tools/Coq_makefileregisgia
Export $(COQMKTOP) in generated Makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16028 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07* tools/Coq_makefile:regisgia
Add '-I config' in the options of the ocaml compilers. This is useful to reuse site configuration in plugins. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16027 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13coq_makefile: use coqdep instead of ocamldep on .ml4 filesgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15967 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-12Xml_parser: detect immediate EOF + disable check_eof by defaultletouzey
Without this immediate EOF detection, coqtop -ideslave loops when its input channel is closed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15959 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-29coqdep: honor dependencies of "Load"ed filesgareuselesinge
Imagine A.v "Load"s B.v and that B.v "Require"s C. Before this commit we get: A.vo: A.v B.v After this commit we get: A.vo: A.v B.v C.vo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15939 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-29Allow running coq-tex in win32 (fix #2921)letouzey
Yes, it seems that < and > and even 2>&1 are legal under windows :-) Btw, the only function using streams has been rewritten, so coq_tex is now a standard .ml file, not a .ml4 anymore (beware during upgrade!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15938 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Continuing r15885 fixing coqdoc index bugs introduced in r14624 and r15053.herbelin
Indeed r15885 still had problems (index contained referenced objects and not only defined objects, sorry). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15893 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Removed dead code about linking Module names in coqdoc.herbelin
Code was probably unused since scan_file made obsolete in r11024. See also r12890. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15892 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Coq_makefile: easier compilation with timings info (from r15850)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15888 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Fixing coqdoc index bugs introduced in r14624 and r15053. Revision r14624 ↵pboutill
introduced bug #2709 on duplicate entries in index and tentative fix of it in r15053 mixed up names of files and names of constants in index (as reported by P. Castéran on coqdev). Patch by Hugo Herbelin :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15885 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-08fix r15860 : no slash after $(COQLIB)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15882 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06still some more dead code removalletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06remove -rectypes except for term.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-05Repair the configure after Hugo's last "repair" ;-)letouzey
Ok, I wasn't aware of the funny behavior of cd in presence of $CDPATH. But the last "repair" was worse, trying to write into non-existing file theories/config/coq_config.ml Things should be better now: * no more Coq_config.theories_dirs at all, since it was completely unused :-) * concerning Coq_config.plugins_dirs, we list them without any "cd" into plugins, hence keeping the "plugins/" part in their paths, and adapt accordingly the only use (!) of plugins_dirs, in coq_makefile Please run ./configure again after upgrading to this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15860 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-22Fix use of $(HASNATDYNLINK) in coq_makefile outputglondu
Generated makefiles were broken because $(if ifeq '$(HASNATDYNLINK)' 'true',X) always returns X. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15826 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-18Coq_makefile fixupspboutill
- put %.cmxs rule from %.cmxa before the one from %.cmx. - erase \r in included output of commands for windows git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15820 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-17More type-safe interface to Coq XML API.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15813 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-07Coqdoc: fix --utf8 bug for pretty printingpboutill
Author: Francois Ripault <francois.ripault@epita.fr> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15782 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No more states/initial.coq, instead coqtop now requires Prelude.voletouzey
For starting a bare coqtop, the recommended option is now "-noinit" that skips the load of Prelude.vo. Option "-nois" is kept for compatibility, it is now an alias to "-noinit". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Revert "when cross-compiling with mingw32, let's fix the Filename.dir_sep"letouzey
This was merely cosmetic after all, since recent Windows versions do tolerate paths with /. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15750 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-06Coqdoc inlined verbatim_char in latexpboutill
Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15690 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-06Add inline verbatim (<</>>), quotes (") and urls ({{url} name}) ↵pboutill
markup/typesetting to coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15689 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-05Coqdoc: More keywords, better special char escape, special case for "in *"pboutill
Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15680 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-05More entries in the indexpboutill
Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15678 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-18Various minor fixes to coqdoc from A. Chlipala.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15624 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-09Fixed fake_ide test-suite.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15564 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-29Fixing fake_ideppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15502 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Coq_makefile: make uninstall targetpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15480 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22Install is rather beautifulpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15479 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 21:58:45 +0000