aboutsummaryrefslogtreecommitdiff
path: root/tools
AgeCommit message (Collapse)Author
2014-01-06Adding a -dumpgraph option to Coqdep that output the graph dependency of thePierre-Marie Pédrot
considered files. Original patch by Guillaume Allais.
2014-01-05Paral-ITP: cleanup of command line flags and more conservative defaultEnrico Tassi
-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).
2014-01-05coqtop: -check-vi-tasks and -schedule-vi-checkingEnrico Tassi
The command `coqtop -check-vi-tasks 1,4,2 a` checks tasks 1 4 2, in this precise order, stored in a.vi. The command `coqtop -schedule-vi-checking 4 a b c` reads {a,b,c}.vi and .{a,b,c}.aux and spits 4 command lines to check all the tasks in {a,b,c}.vi trying to equally partition the job between the 4 workers, that can indeed be run in parallel. The aux file contains the time that it took to check the proofs stored in the .vi files last time the file was fully checked. This user interface is still very rough, it should probably run the workers instead of just printing their command line.
2014-01-04.vi files: .vo files without proofsEnrico Tassi
File format: The .vo file format changed: - after the magic number there are 3 segments. A segment is made of 3 components: bynary int, an ocaml value, a digest. The binary int is the position of the digest, so that one can skip the value without unmarshalling it - the first segment is the library, as before - the second segment is the STM task list - the third segment is the opaque table, as before A .vo file has a complete opaque table (all proof terms are there). A .vi file follows the same format of a .vo file, but some entries in the opaque table are missing. A proof task is stocked instead. Utilities: coqc: option -quick generates a .vi insted of a .vo coq_makefile: target quick to generate all .vi coqdep: generate deps for .vi files too votour: can browse .vi files too, the first question is which segment should be read coqchk: rejects .vi files
2013-12-22Adding -bt to coqc.Pierre-Marie Pédrot
2013-12-20coqc: execvp is now available even on win32Pierre Letouzey
2013-12-20coqmktop without Unix (simpler all_subdirs)Pierre Letouzey
2013-12-20Warning removalPierre Boutillier
2013-12-20Coqdep always uses / as dir_sepPierre Boutillier
2013-12-17Fix make install after 3e972b3ff8e532be233f70567c87512324c99b4ePierre Boutillier
Attempt to adapt .el files too. doc/refman/RefMan-uti.tex has still to be fixed.
2013-12-10Renaming elisp files to avoid conflict with pg in distribs.Pierre Courtieu
2013-10-29Revert the two last commits. My bad, I messed up git-svn commands...ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16951 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-29Printing heap on every processed sentence.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16949 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-14Avoid polymorphic comparison (coqdoc).xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16884 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-14Getting rid of the use of deprecated elements (from the OCaml standard library).xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-10Document: undoing inside a focused zone does not require unfocusinggareuselesinge
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
2013-10-10fake_ide: ported to Document + 2 tests for editing a proof (locally)gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16871 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07fake_ide: speak the new protocolgareuselesinge
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
2013-09-30fake_ide: call Coq.init as the first actiongareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16819 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30fake_ide ported to the new protocol (FIXME tests fail)gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16813 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵xclerc
with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Misc changes around coqtop.ml :letouzey
- 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
2013-08-19Modulification and removing of structural equality in Stateid.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08State Transaction Machinegareuselesinge
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 07:47:41 +0000