| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
Used to replace the standard conversion by the VM. Not so useful, and
implemented using a bunch of references inside and outside the kernel.
|
| |
|
|
|
| |
Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
|
| |
|
|
|
|
| |
According to http://caml.inria.fr/mantis/view.php?id=5325
you can't use the same socket for both writing and reading.
The result is lockups (may be fixed in 4.03).
|
| |
|
|
|
|
|
|
|
| |
in the loadpath.
This patch causes a bit of code duplication (because of the .coq suffix
added to state files) but it makes it clear which part of the code is
looking up files in the loadpath and for what purpose. Also it makes the
interface of System.extern_intern and System.raw_extern_intern much saner.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The single remaining use is in library/states.ml. This use should be
reviewed, as it is most certainly broken.
The other uses of Loadpath.get_paths did not disappear by miracle though.
They were replaced by a new function Loadpath.locate_file which factors
all the uses of the function. This function should not be used as it is as
broken as Loadpath.get_paths, by definition.
Vernac.load_vernac now takes a complete path rather than looking up for
the file. That is the way it was used most of the time, so the lookup was
unnecessary. For instance, Vernac.compile was calling Library.start_library
which already expected a complete path.
Another consequence is that System.find_file_in_path is almost no longer
used (except for Loadpath.locate_file, obviously). The two remaining uses
are System.intern_state (used by States.intern_state, cf above) and
Mltop.dir_ml_load for dynamically loading compiled .ml files.
|
| |
|
|
|
|
|
|
|
|
| |
This command-line option was behaving like the old -require, except that
it did not do Import. In other words, it was loading files without
respecting the loadpath. Now it behaves exactly like Require, while
-require now behaves like Require Import.
This patch also removes Library.require_library_from_file and all its
dependencies, since they are no longer used inside Coq.
|
| | |
|
| |
|
|
|
| |
command line. Documenting only the former for simplicity and
uniformity with predating option -with-geoproof.
|
| |
|
|
|
|
|
|
|
|
| |
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
|
| |
|
|
| |
This allows fatal_error to be used for printing anomalies at loading time.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This interface is promoted by the operf-macro tool
https://github.com/OCamlPro/operf-macro
which allows to run benchmarks of time and memory usage
of various OCaml programs.
Coq already has two ways to get Gc infos:
- the -m|--memory command-line flag prints the total heap words allocated
- the "Print Debug Gc" command prints much more information,
but in a Coq-implementation-defined format that is not suitable
for across-programs comparison
(also an environment variable allows to profile Coq runs on any .v,
in an non-intrusive way)
Note to the Github Robot:
This closes #75
|
| | |
|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
| |
This disables colors in emacs compilation buffer, which does not
support ansi colors by default.
|
| | |
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
subdirectories.
Using Mltop.add_path instead of Mltop.add_rec_path causes the following
kind of behavior:
$ coqtop -nois
Coq < Require Import Coq.Init.Datatypes.
Error: Cannot find a physical path bound to logical path Coq.Init.
The only case where its use is still warranted is the implicit "." path. It
shall not be recursive because Coq might be called from about anywhere.
This patch also removes -I-as since its behavior is no longer the one from
8.4 so it is not worth keeping it around.
|
| | |
|
| |
|
|
|
|
| |
(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).
|
| |
|
|
|
|
|
|
| |
I know it seems wrong but if you call coq to get a path, you are likely
to pass it around, and this makes the dir separator of windows "\"
disappear immediately being interpreted as an escape character.
In cygwin "/" is also understood as a directory separator.
|
| |
|
|
| |
Solves an efficiency problem in Makefiles generated by coq_makefile.
|
| |
|
|
| |
This is a follow-up on Pierre's 5d80a385.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
With the options -async-queries-always-delegate queries are
always delegated to a worker process (Eval, Check, ...).
Users of PIDE based UIs (in Denmark) reported that the current
behavior of processing query synchronously is rather unexpected
when one is used to get proofs processed asynchronously.
Non instantaneous queries are part of many scripts and are there
as "tests" for testing the execution of recursive functions.
A standard proof script shape in an ongoing work by Appel and Bengtson
is made of blocks like:
- recursive function definition,
- some tests,
- some proofs
And one cannot quickly jump over the tests (only the proofs).
Enclosing the queries into dummy proofs to recover a reactive UI
is just annoying. Hence this patch.
Currently CoqIDE is not able to integrate the asynchronous feedback
of the query workers into the document, hence if one passes the option
to CoqIDE one only gets a boolean out of queries (processed/error).
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
E.g.
Coq options are:
-I dir look for ML files in dir
-include dir (idem)
[...]
-h, --help print this list of options
With the flag '-toploop coqidetop' these extra option are also available:
--help-XML-protocol print the documentation of the XML protocol used by CoqIDE
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
par: distributes the goals among a number of workers given
by -async-proofs-tac-j (defaults to 2).
|
Maxime Dénès
Enrico Tassi
Guillaume Melquiond
Pierre-Marie Pédrot
Hugo Herbelin
Thomas Sibut-Pinote
Gabriel Scherer
Pierre Courtieu
Xavier Clerc