| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| | |
(e.g. with deprecated options such as -byte, etc.) since I guess this
is what we expect.
Was probably lost in 81eb133d64ac81cb.
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
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
|
| | |
| |
| |
| | |
This allows fatal_error to be used for printing anomalies at loading time.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
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.
|
| |\|
| |
| |
| |
| |
| |
| | |
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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).
|
| |
|
|
|
|
|
|
| |
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.
|
Pierre-Marie Pédrot
Hugo Herbelin
Maxime Dénès
Guillaume Melquiond
Matej Kosik
Enrico Tassi
Thomas Sibut-Pinote
Gabriel Scherer
Pierre Courtieu
Pierre Letouzey