aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
Commit message (Collapse)AuthorAge
* Revert the two last commits. My bad, I messed up git-svn commands...Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16951 85f007b7-540e-0410-9357-904b9bb8a0f7
* Printing heap on every processed sentence.Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16949 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid polymorphic comparison (coqdoc).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16884 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of the use of deprecated elements (from the OCaml standard library).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document: undoing inside a focused zone does not require unfocusingGravatar gareuselesinge2013-10-10
| | | | | | | | | | | | | To test this fake_ide has also been improved with the GOALS command. As for CoqIDE, ADDing a sentence does not force its evaluation. The "advance 1 sentence" button is an ADD + GOALS. If one of the ADDed sentences is wrong, GOALS receives the error. The GUI then backtracks to a safe state id (sent by Coq). fake_ide has GOALS (asserts that the goals call was OK) and FAILGOALS to assert it fails and backtrack to a valid state. see unfdo022.fake. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16873 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide: ported to Document + 2 tests for editing a proof (locally)Gravatar gareuselesinge2013-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16871 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide: speak the new protocolGravatar gareuselesinge2013-10-07
| | | | | | | | | A new syntax for .fake files, allowing multi line phrases and labeled script points (to go back to them). Test 7 fails because of a bug in STM (in a very spaghetti-like script). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16860 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide: call Coq.init as the first actionGravatar gareuselesinge2013-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16819 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide ported to the new protocol (FIXME tests fail)Gravatar gareuselesinge2013-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16813 85f007b7-540e-0410-9357-904b9bb8a0f7
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵Gravatar xclerc2013-09-19
| | | | | | with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
| | | | | | | | | | | | | | | | | | | - Revised Coqtop.parse_args in a cleaner and lighter style - Improved error message in case of argument parse failure: * tell which option is expecting a related argument * in case of unknown options, warn about them all at once * do not hide the previous error messages by filling the screen with usage(). Instead, suggest the use of --help. - Specialized boolean config field Coq_config.arch_is_win32 - Faster Envars.coqlib, which is back to (unit->string), and just access Flags.coqlib. Caveat: it must be initialized once via Envars.set_coqlib - Avoid keeping an opened channel to the "revision" file - Direct load of theories/init/prelude.vo, no detour via Loadpath Beware : ./configure must be runned after this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification and removing of structural equality in Stateid.Gravatar ppedrot2013-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
* State Transaction MachineGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | | | | | | | The process_transaction function adds a new edge to the Dag without executing the transaction (when possible). The observe id function runs the transactions necessary to reach to the state id. Transaction being on a merged branch are not executed but stored into a future. The finish function calls observe on the tip of the current branch. Imperative modifications to the environment made by some tactics are now explicitly declared by the tactic and modeled as let-in/beta-redexes at the root of the proof term. An example is the abstract tactic. This is the work described in the Coq Workshop 2012 paper. Coq is compile with thread support from now on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide: xml parser does not check for EOFGravatar gareuselesinge2013-05-06
| | | | | | Exactly as Coqide's parser does. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16481 85f007b7-540e-0410-9357-904b9bb8a0f7
* New module Xml_printer (dual to Xml_parser)Gravatar gareuselesinge2013-05-06
| | | | | | | 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
* Coqide: new feedback mechanism for structured contentGravatar gareuselesinge2013-04-25
| | | | | | | | | | | | | | | | | 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
* Fix compilation of fake_ideGravatar gareuselesinge2013-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16439 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqc and coqmktop migrated in tools/, get rid of scripts/ subdirGravatar letouzey2013-04-18
| | | | | | | 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
* Coqdep: add an -exclude-dir option (wish mentionned in #3025)Gravatar letouzey2013-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16431 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renaming SearchAbout into Search and Search into SearchHead.Gravatar herbelin2013-04-17
| | | | | | 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
* Restrict (try...with...) to avoid catching critical exn (part 15)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16292 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "remove -rectypes except for term.ml"Gravatar mdenes2013-01-22
| | | | | | | | | | 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
* I forget to use git log before git svn dcommit ...Gravatar pboutill2013-01-18
| | | | | | | | | | | | 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
* Revert "coq_makefile: use coqdep instead of ocamldep on .ml4 files"Gravatar pboutill2013-01-18
| | | | | | This reverts commit d14b9f6a017347e59cf037ff576f282785105080. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16128 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: quoting pathsGravatar pboutill2013-01-07
| | | | | | | | 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
* Coq_makefile: -extra & -phony-extra for user defined makefile ruleGravatar pboutill2013-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16118 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: Better rule for subdirs when the subdir does not existGravatar pboutill2012-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16056 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "* tools/Coq_makefile:"Gravatar regisgia2012-12-07
| | | | | | This reverts commit 9a2f43eca179436f0581751b93c989fd30a5c13c. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16029 85f007b7-540e-0410-9357-904b9bb8a0f7
* * tools/Coq_makefileGravatar regisgia2012-12-07
| | | | | | Export $(COQMKTOP) in generated Makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16028 85f007b7-540e-0410-9357-904b9bb8a0f7
* * tools/Coq_makefile:Gravatar regisgia2012-12-07
| | | | | | | 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
* coq_makefile: use coqdep instead of ocamldep on .ml4 filesGravatar gareuselesinge2012-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15967 85f007b7-540e-0410-9357-904b9bb8a0f7
* Xml_parser: detect immediate EOF + disable check_eof by defaultGravatar letouzey2012-11-12
| | | | | | | 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
* coqdep: honor dependencies of "Load"ed filesGravatar gareuselesinge2012-10-29
| | | | | | | | | | | | | 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
* Allow running coq-tex in win32 (fix #2921)Gravatar letouzey2012-10-29
| | | | | | | | | 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
* Continuing r15885 fixing coqdoc index bugs introduced in r14624 and r15053.Gravatar herbelin2012-10-16
| | | | | | | 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
* Removed dead code about linking Module names in coqdoc.Gravatar herbelin2012-10-16
| | | | | | | 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
* Coq_makefile: easier compilation with timings info (from r15850)Gravatar pboutill2012-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15888 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing coqdoc index bugs introduced in r14624 and r15053. Revision r14624 ↵Gravatar pboutill2012-10-15
| | | | | | | | 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
* fix r15860 : no slash after $(COQLIB)Gravatar letouzey2012-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15882 85f007b7-540e-0410-9357-904b9bb8a0f7
* still some more dead code removalGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove -rectypes except for term.mlGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
* Repair the configure after Hugo's last "repair" ;-)Gravatar letouzey2012-10-05
| | | | | | | | | | | | | | | | | | 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
* Fix use of $(HASNATDYNLINK) in coq_makefile outputGravatar glondu2012-09-22
| | | | | | | | 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
* Coq_makefile fixupsGravatar pboutill2012-09-18
| | | | | | | - 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
* 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
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
| | | | | | | | | 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
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 20:08:40 +0000