aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
Commit message (Collapse)AuthorAge
* Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
| | | | This allows fatal_error to be used for printing anomalies at loading time.
* Add a Set Dump Bytecode command for debugging purposes.Gravatar Maxime Dénès2015-06-23
| | | | | Prints the VM bytecode produced by compilation of a constant or a call to vm_compute.
* Flag -test-mode intended to be used for ad-hoc prints in test-suiteGravatar Enrico Tassi2015-05-29
| | | | | | | Of course there is an exception to the previous commit. Fail used to print even if silenced but loading a vernac file. This behavior is useful only in tests, hence this flag.
* Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X.Gravatar Hugo Herbelin2015-05-22
| | | | Thanks to Vadim Zaliva for testing.
* Changing the heuristic fixing bug #4241.Gravatar Pierre Courtieu2015-05-21
| | | | | | | | | | Fixed #4241 correlates Printing Width and max_indent, this patch changes the correlation to the following one: max_indent = max ((wdth*80)/100) (wdth-30) i.e. the right column defined by max_indent is 20% of the global width, but capped to 30 characters.
* Answering report #4241 (formatting of boxes not behaving regularlyGravatar Hugo Herbelin2015-05-20
| | | | when printing width extend).
* Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that filesGravatar Hugo Herbelin2015-05-20
| | | | | found in the file system have the expected lowercase/uppercase spelling)
* The Fail command does not catch uncaught exception anomalies anymore.Gravatar Pierre-Marie Pédrot2015-05-18
|
* On MacOS X, ensuring that files found in the file system have theGravatar Hugo Herbelin2015-05-15
| | | | | expected lowercase/uppercase spelling (based on a patch by Pierre B.). This should fix #2554 (and see also discussion on coq-club, May 2015).
* The -list-tag options now prints the corresponding COQ_COLORS value.Gravatar Pierre-Marie Pédrot2015-05-14
|
* Adding an option -w to control Coq warning output.Gravatar Pierre-Marie Pédrot2015-05-14
| | | | | | | For now, warnings are still ignored by default, but this may change. This commit at least allows to print them whenever desired. The -w syntax is also opened to future additions to further control the display of warnings.
* Disable precompilation for native_compute by default.Gravatar Guillaume Melquiond2015-05-14
| | | | | | | | | | | | | | Note that this does not prevent using native_compute, but it will force on-the-fly recompilation of dependencies whenever it is used. Precompilation is enabled for the standard library, assuming native compilation was enabled at configuration time. If native compilation was disabled at configuration time, native_compute falls back to vm_compute. Failure to precompile is a hard error, since it is now explicitly required by the user.
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
| | | | | | | The command [Redirect "filename" (...)] redirects all the output of [(...)] to file "filename.out". This is useful for storing the results of an [Eval compute], for redirecting the results of a large search, for automatically generating traces of interesting developments, and so on.
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
| | | | | | Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure.
* Removing dead code in Pp.Gravatar Pierre-Marie Pédrot2015-04-23
|
* Pp: obsolete comment.Gravatar Arnaud Spiwack2015-04-22
| | | Was made incorrect by 98a710caf5e907344329ee9e9f7b5fd87c50836f .
* Do not use list concatenation when gluing streams together, just mark them ↵Gravatar Guillaume Melquiond2015-04-22
| | | | | | | | | | | | as glued. Possible improvement: rotate using the left children in the glue function, so that the iter function becomes mostly tail-recursive. Drawback: two allocations per glue instead of a single one. This commit makes the following command go from 7.9s to 3.0s: coqtop <<< "Require Import BigZ ZBinary Reals OrdersEx. Time SearchPattern _." | tail -n 1
* STM: print trace on "anomaly, no safe id attached"Gravatar Enrico Tassi2015-04-21
|
* Adding a primitive to dump the current association table of dynamic types.Gravatar Pierre-Marie Pédrot2015-03-16
|
* Fixing printing of ordinals.Gravatar Pierre-Marie Pédrot2015-02-26
|
* New function [Constr.equal_with] to compare terms up to variants of ↵Gravatar Arnaud Spiwack2015-02-24
| | | | | | | | [kind_of_term]. To be able to write equality up to evar instantiation instantiation. Generalises the main function of [eq] constr over the variant of [kind_of_term] it uses. It prevents some optimisation of [Array.equal] where two physically equal arrays are considered (less or) equal. But it does not seem to have appreciable effects on efficiency.
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
|
* Future: human readable name for delegated (Close #4065)Gravatar Enrico Tassi2015-02-21
|
* Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
| | | | | | (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
* Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
| | | | | | | In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error).
* Adding a statistic function on hashconsing tables.Gravatar Pierre-Marie Pédrot2015-02-11
|
* Fixing bug #4009.Gravatar Pierre-Marie Pédrot2015-02-07
| | | | We only allow color output under Unix OSes.
* More efficient Richpp.Gravatar Pierre-Marie Pédrot2015-02-06
| | | | We build the rich XML at once without generating the printed string.
* Marshal.from_string on 32 bit systems use tmpfile if needed (Close: 3968)Gravatar Enrico Tassi2015-02-05
| | | | | | | | Strings are at most 16M on 32 bit OCaml, and the system state may be bigger. In this case we write to tmp file and Marshal.from_channel. We can't directly use the channel interface because of badly designed non blocking API (available only on fds and not channels).
* More efficient implementation of Richpp.Gravatar Pierre-Marie Pédrot2015-02-04
| | | | | Instead of constructing the XML string and parsing it afterwards, we build it by hijacking the formatting output.
* CThread: workaround for threads lockup on windwos made more aggressiveGravatar Enrico Tassi2015-02-04
|
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Fix a few typos.Gravatar Maxime Dénès2015-01-12
|
* Extraction: no more ascii blob in type variables (fix #3227)Gravatar Pierre Letouzey2015-01-11
| | | | | | Since type variables are local to the definition, we simply rename them in case of unicode chars. We also get rid of any ' to avoid Ocaml illegal 'a' type var (clash with char litteral).
* Adding more sharing in Map.udpate and Map.modify.Gravatar Pierre-Marie Pédrot2015-01-10
|
* Safer version of the implementation of stores.Gravatar Pierre-Marie Pédrot2015-01-06
|
* remove unused iArrayGravatar Enrico Tassi2015-01-06
|
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
|
* Inlining Spawn.kill_if in the one place were it was actually used, thusGravatar Pierre-Marie Pédrot2014-12-25
| | | | removing the need of thread creation in the interface.
* Fixed bad newlines in output for std output and emacs.Gravatar Pierre Courtieu2014-12-18
| | | | | I added a emacs_logger. Still need to cleanup std_logger.
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
|
* Future: blocking by defaultGravatar Enrico Tassi2014-12-17
| | | | | | This makes queries like Print or Extraction block and not raise the error "the value is not ready". This should make CoqIDE work for every kind of script.
* STM: rename and simplify flagsGravatar Enrico Tassi2014-12-17
|
* Spawn: fix request of Gc statisticsGravatar Enrico Tassi2014-12-17
|
* CThread: use a different type for thread friendly in_channelsGravatar Enrico Tassi2014-12-17
|
* Dyn: add API to check of two Dyn.t are ==Gravatar Enrico Tassi2014-12-17
| | | | | A Dyn.t boxes a type tag with the original object, so calling == on the Dyn.t does not work, hence this extra API.
* msg_info now puts infomsg tag in emacs mode.Gravatar Pierre Courtieu2014-12-16
| | | | | Fixes the idtac "string" not appearing in proofgeneral because printined *before* the goal.
* Proper thread-safe implementation for Exninfo.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | This is the second part of the Exninfo patch. It introduces dependency in the Thread library in all Coq files.
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | | | | | | | | | | | | | | | | Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 21:19:52 +0000