| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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),
- uniformly expecting paths in Unix format and warning otherwise.
|
| | |
| |
| |
| |
| |
| | |
(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.
|
| |
|
|
|
| |
Since it displays together with the goal, it is better (for pg and
other interfaces probably) that they are in a different message.
|
| | |
|
Guillaume Melquiond
Pierre-Marie Pédrot
Clément Pit--Claudel
Arnaud Spiwack
Enrico Tassi
Hugo Herbelin
Maxime Dénès
Pierre Letouzey
Pierre Courtieu
Pierre Boutillier