| Age | Commit message (Collapse) | Author |
|---|
|
This has no effect anymore, verbose printing is controlled now by
the regular, common `quiet` flag.
|
|
|
|
This removes the Flags.univ_print in the kernel, making it possible to
put the univ printing flag ownership back in Detyping.
The lazyness is because getting an explanation may be costly and we
may discard it without printing.
See benches
- with lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/406/console
- without lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/405/console
Notably without lazy mathcomp odd_order is +1.26% with some lines
showing significant changes, eg PFsection11 line 874 goes from 11.76s
to 13.23s (+12%).
(with lazy the same development has -1% overall and the same line goes
from 11.76s to 11.23s (-4%) which may be within noise range)
|
|
Recent commits introduced global flags, but these should be
module-specific so relocating.
Global flags are deprecated, and for 8.9 `Lib.Flags` will be reduced
to the truly global stuff.
|
|
|
|
|
|
|
|
|
|
This intermediate representation serves two purposes:
1- It is a preliminary step for primitive machine integers, as iterators
will be compiled to Clambda.
2- It makes the VM compilation passes closer to the ones of
native_compute. Once we unifiy the representation of values, we should
be able to factorize the lambda-code generation between the two
compilers, as well as the reification code.
This code was written by Benjamin Grégoire and myself.
|
|
|
|
The old semantics of `with/without_option` allowed the called function
to modify the value of the option. This is an issue mainly with the
`silently/verbose` combinators, as `Set Silent` can be executed under
one of them and thus the modification will be lost in the updated code
introduced in a554519874c15d0a790082e5f15f3dc2419c6c38
IMHO these kind of semantics are quite messy but we have to preserve
them in order for the `Silent` system to work. In fact, note that in
the previous code, `with_options` was not consistent with
`with_option` [maybe that got me confused?]
Ideally we could restore the saner semantics once we clean up the
`Silent` system [that is, we remove the flag altogether], but that'll
have to wait.
Fixes #6645.
|
|
|
|
Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.
|
|
One less global flag.
|
|
|
|
|
|
|
|
And some code simplification.
|
|
We move the main async flags to the STM in preparation for
more state encapsulation.
There is still more work to do, in particular we should make some of
the defaults a parameter instead of a flag.
|
|
We remove coqmktop in favor of a couple of simple makefile rules using
ocamlfind. In order to do that, we introduce a new top-level file that
calls the coqtop main entry.
This is very convenient in order to use other builds systems such as
`ocamlbuild` or `jbuilder`.
An additional consideration is that we must perform a side-effect on
init depending on whether we have an OCaml toplevel available [byte]
or not. We do that by using two different object files, one for the
bytecode version other for the native one, but we may want to review
our choice.
We also perform some smaller cleanups taking profit from ocamlfind.
|
|
The patch has three parts:
- Introduction of a configure flag `-bytecode-compiler (yes|no)`
(due to static initialization this is a configure-time option)
- Installing the hooks that register the VM with the pretyper and the
kernel conditionally on the flag.
- Replacing the normalization function in `Redexpr` by compute if the
VM is disabled.
We also rename `Coq_config.no_native_compiler` to `native_compiler`
and `Flags.native_compiler` to `output_native_objects` [see #4607].
|
|
While we are at it we refactor a few special cases of the helper.
|
|
|
|
We move delicate library/module instillation code to the STM so the
API guarantees that the first state snapshot is correct. That was not
the case in the past, which meant that the STM cache was unsound in
batch mode, however we never used its contents due to not backtracking
to the first state.
This provides quite an improvement in the API, however more work is
needed until the codepath is fully polished.
This is a critical step towards handling the STM functionally.
|
|
We move toplevel/STM flags from `Flags` to their proper components;
this ensures that low-level code doesn't depend on them, which was
incorrect and source of many problems wrt the interfaces.
Lower-level components should not be aware whether they are running in
batch or interactive mode, but instead provide a functional interface.
In particular:
== Added flags ==
- `Safe_typing.allow_delayed_constants`
Allow delayed constants in the kernel.
- `Flags.record_aux_file`
Output `Proof using` information from the kernel.
- `System.trust_file_cache`
Assume that the file system won't change during our run.
== Deleted flags ==
- `Flags.compilation_mode`
- `Flags.batch_mode`
Additionally, we modify the STM entry point and `coqtop` to account
for the needed state. Note that testing may be necessary and the
number of combinations possible exceeds what the test-suite / regular
use does.
The next step is to fix the initialization problems [c.f. Bugzilla],
which will require a larger rework of the STM interface.
|
|
|
|
This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.
It is also not included in the API, so it should either be included in
it or this PR be applied.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
versions.
|
|
We remove the emacs-specific printing code from the core of Coq, now
`-emacs` is a printing flag controlled by the toplevel.
|
|
We allow for a dynamic setting of the STM debug flag, and we print
some more information about the result of `process_transaction`.
We also fix a printing bug due to mixing `Printf` and `Format`, which
are not compatible.
|
|
Today, both modes are controlled by a single flag, however this is a
bit misleading as is_silent really means "quiet", that is to say `coqc
-q` whereas "verbose" is Coq normal operation.
We also restore proper behavior of goal printing in coqtop on quiet
mode, thanks to @Matafou for the report.
|
|
Mostly documentation and making a couple of local flags, local.
|
|
- We clean-up `Vernac` and make it use the STM API.
- Now functions in `Vernac` for use in the toplevel and compiler take
an starting `Stateid.t`.
- Duplicated `Stm.interp` entry point is removed.
- The XML protocol call `interp` is disabled.
|
|
|
|
|
|
|
|
Given the current style in flags.mli no reason to have a function.
A deeper question is why a global flag is needed, in particular the use
in `interp/constrextern.ml` seems strange, the condition in the lexer
should be looked at and I'm not sure about `printing/`.
|
|
|
|
This was the original value from Tobias' code. When a user passes
-profile-ltac on the command line, or inserts [Show Ltac Profile] in the
document, the most useful default behavior is to not overload them with
useless information. When GUI clients want to display fancier profiling
information, there is no cost to the user to requiring them to specify
what cutoff they want. If the GUI client does not have any special
LtacProf handling, the most useful presentation is again the one that
cuts off the display at 2% total time.
|
|
This is a quick fix. The Metasyntax module should be thoroughly revised
in trunk, because it starts featuring a lot of spaghetti code and redundant
data.
|
|
With this command line flag one can profile ltac in files
/and/ trim the results without actually touching the files.
|
|
|
|
|
