| Age | Commit message (Collapse) | Author |
|---|
|
This allows fatal_error to be used for printing anomalies at loading time.
|
|
Prints the VM bytecode produced by compilation of a constant or a call to
vm_compute.
|
|
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.
|
|
Thanks to Vadim Zaliva for testing.
|
|
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.
|
|
when printing width extend).
|
|
found in the file system have the expected lowercase/uppercase
spelling)
|
|
|
|
expected lowercase/uppercase spelling (based on a patch by Pierre B.).
This should fix #2554 (and see also discussion on coq-club, May 2015).
|
|
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
|
|
Was made incorrect by 98a710caf5e907344329ee9e9f7b5fd87c50836f .
|
|
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
|
|
|
|
|
|
|
|
[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.
|
|
|
|
|
|
(Sorry, was not intended to be pushed)
This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
|
|
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).
|
|
|
|
We only allow color output under Unix OSes.
|
|
We build the rich XML at once without generating the printed string.
|
|
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).
|
|
Instead of constructing the XML string and parsing it afterwards,
we build it by hijacking the formatting output.
|
|
|
|
|
|
|
|
|
|
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).
|
|
|
|
|
|
|
|
|
|
removing the need of thread creation in the interface.
|
|
I added a emacs_logger.
Still need to cleanup std_logger.
|
|
|
|
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.
|
|
|
|
|
|
|
|
A Dyn.t boxes a type tag with the original object, so calling
== on the Dyn.t does not work, hence this extra API.
|
|
Fixes the idtac "string" not appearing in proofgeneral because
printined *before* the goal.
|
|
This is the second part of the Exninfo patch. It introduces dependency in
the Thread library in all Coq files.
|
|
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.
|
