| Age | Commit message (Collapse) | Author |
|---|
|
This an implementation of point 2 of CEP coq/ceps#48
https://github.com/coq/ceps/pull/48
Option -native-compiler of the configure script now impacts the
default value of the option -native-compiler of coqc. The
-native-compiler option of the configure script is added an ondemand
value, which becomes the default, thus preserving the previous default
behavior.
The stdlib is still precompiled when configuring with -native-compiler
yes. It is not precompiled otherwise.
|
|
Closes #11277 ; the `space_overhead` parameter has been selected for
maximum speedup, in some cases it could also increase memory
consumption. Please use `OCAMLRUNPARAM` to tune it and report back
your experiments.
|
|
Reviewed-by: gares
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
This fixes a regression introduced in #11618, where I didn't realize
that the order of ML includes would be important as users may want to
shadow it.
In general I do believe that shadowing is tricky and the build system
should handle it, but for now makes sense to preserver the behavior.
The fix is not very nice, but we cannot afford to tweak the API as
this should be backported to 8.12.1; there is a pending PR refactoring
a bit more the toplevel init that should clean this up.
Fixes #12771
|
|
Reviewed-by: herbelin
Ack-by: gares
Ack-by: ejgallego
|
|
Add menu item that uses this
|
|
As suggested in the PR review.
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
After #8743 we don't depend on `num` anymore in the codebase; thus we
drop the dependency.
This could create problems for plugins relying on this implicit
linking.
|
|
Before this patch, the proof engine had three notions of shelves:
- A local shelf in `proofview`
- A global shelf in `Proof.t`
- A future shelf in `evar_map`
This has lead to a lot of confusion and limitations or bugs, because
some components have only a partial view of the shelf: the pretyper can
see only the future shelf, tactics can see only the local and future
shelves. In particular, this refactoring is needed for #7825.
The solution we choose is to move shelf information to the evar map, as
a shelf stack (for nested `unshelve` tacticals).
Closes #8770.
Closes #6292.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.
We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.
We thus keep the num library linked for now until all plugins are
ported.
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
After #12504 , we can encapsulate and consolidate low-level state
logic in `Vernacstate`, removing `States` which is now a stub.
There is hope to clean up some stuff regarding the handling of
low-level proof state, by moving both `Evarutil.meta_counter` and
`Evd.evar_counter_summary` into the proof state itself [obligations
state is taken care in #11836] , but this will take some time.
|
|
This will ensure that we don't introduce problems as it has happened
in the past.
While we are at it, we fix one easy case of non-tail call.
|
|
|
|
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
|
|
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
This makes the API more orthogonal and allows better structure in
future code.
|
|
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
|
|
This actually gets `Pfedit` out of the dependency picture [can be
almost merged with `Proof` now, as it is what it manipulates] and
would allow to reduce the exported low-level API from `Proof_global`,
as `map_fold_proof` is not used anymore.
|
|
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
- Provide new helper functions in `Goptions` on the model of
`declare_bool_option_and_ref`;
- Use these helper functions in many parts of the code base
(encapsulates the corresponding references);
- Move almost all options from `declare_string_option` to
`declare_stringopt_option` (only "Warnings" continue to use the
former). This means that these options now support `Unset` to get
back to the default setting. Note that there is a naming
misalignment since `declare_int_option` is similar to
`declare_stringopt_option` and supports `Unset`. When "Warning" is
eventually migrated to support `Unset` as well, we can remove
`declare_string_option` and rename `declare_stringopt_option` to
`declare_string_option`.
- For some vernac options and flags that have an equivalent
command-line option or flag, implement it like the standard `-set`
and `-unset`.
|
|
This option is confusing because it does Require Import, not Require.
It was deprecated in 8.11. We remove it in 8.12 in order to
reintroduce it in 8.13 as a replacement for -load-vernac-object, which
is the option that does Require without Import as of today.
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
|
|
Latest refactorings allow us to make the signature Coq parser a
standard `Grammar.S` one; the only bit needed is to provide the extra
capabilities to the `Lexer` signature w.r.t. to comments state.
The handling of Lexer state is still a bit ad-hoc, in particular it is
global whereas it should be fully attached to the parsable. This may
work ok in batch mode but the current behavior may be buggy in the
interactive context.
This PR doesn't solve that but it is a step towards a more functional
solution.
|
|
There is not need to re-export Gramlib's API in a non-structured way
anymore. We thus expose the core Gramlib interface to users and remove
redundant functions.
A question about whether to move more parts of the API to `Gramlib` is
still open, as well as on naming.
|
|
Make sure that all initial load vernaculars that were specified on the command line are executed before processing the options set through -set on the command line.
The reason for this is that the load vernacular options can load plugins that define new Goptions. If these plugins are not loaded before the -set flags are processed,
then Goptions will emit a warning that the options of that plugin don't exist and ignore the flag.
|
|
Add headers to a few files which were missing them.
|
|
We refactor handling of `-boot` so the "coqlib" guessing routine,
`Envars.coqlib ()` is not called when bootstrapping.
In compositional builds involving Coq's prelude we don't want for this
guessing to happen, as the heuristics to locate the prelude will fail
due to different build layout choices.
Thus after this patch Coq does not do any guessing when `-boot` is
passed, leaving the location of libraries to the usual command line
parameters.
Note that some other tooling still calls `Envars.coqlib`, however this
should happen late enough as for it to be safe; we will fix that
eventually when we consolidate the library for library handling among
tools.
Ideally, we would also remove `Envars.coqlib` altogether, as we want
to avoid clients accessing the Coq filesystem in a non-controlled way.
|
|
Reviewed-by: Matafou
Reviewed-by: ppedrot
|
|
This PR refactors the handling of ML loadpaths to get it closer to
what (as of 2020) the standard OCaml toolchain (ocamlfind, dune) does.
This is motivated as I am leaning toward letting the standard OCaml
machinery handle OCaml includes; this has several benefits [for
example plugins become regular OCaml libs] It will also help in
improving dependency handling in plugin dynload.
The main change is that "recursive" ML loadpaths are no longer
supported, so Coq's `-I` option becomes closer to OCaml's semantics.
We still allow `-Q` to extend the OCaml path recursively, but this may
become deprecated in the future if we decide to install the ML parts
of plugins in the standard OCaml location.
Due to this `Loadpath` still hooks into `Mltop`, but other than that
`.v` location handling is actually very close to become fully
independent of Coq [thus it can be used in other tools such coqdep,
the build system, etc...]
In terms of vernaculars the changes are:
- The `Add Rec ML Path` command has been removed,
- The `Add Loadpath "foo".` has been removed. We now require that the
form with the explicit prefix `Add Loadpath "foo" as Prefix.` is used.
We did modify `fake_ide` as not to add a directory with the empty
`Prefix`, which was not used. This exposed some bugs in the
implementation of the document model, which relied on having an
initial sentence; we have workarounded them just by adding a dummy one
in the two relevant cases.
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
|
|
|
|
`Nativelib` currently assumes that objects are built in some
particular directories, but this is not true in some cases, for
example, when building with Dune.
We add a new option `-nI` to allow clients to specify the OCaml
include dirs.
|
|
This is useful in order to implement native support in Dune for
example, which as of today as strict target rules.
Hopefully this option could go away; it is really internal, but I've
chosen to document it.
|
|
This is useful when we want to have finer control of the location of
files in the bootstrap process, for example when building using Dune.
Also, this makes options consistent with what `coqdep` already uses
for bootstrap.
The main use case for `-boot` is to replace the hardcoded `add_load_path (coqlib () / theories)` with `-R dir Coq`, where dir is controlled by the build system. In particular, we use `-R . Coq` as we `cd` into the directory the package is, so without boot we'd have to hardcode the `theories` path in Dune itself. which seems less robust.
Notably after this change the only part of the build that uses `coqlib` is the micromega solver, but that can be tweaked so if coqlib is not set it will use the one in the path. IMO not having to set "coqlib" is a good property if we want a more compositional setup.
|
|
`theories` now never have `.ml` files inside.
|
|
Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.
This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.
We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.
Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.
This could also imply a performance gain as we now effectively
traverse less directories when locating a library.
See also discussion in #10003
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
|
|
In previous refactorings `vernac_loop` stopped being tail-recursive,
we refactor code a bit and make it back into tail-recursive form.
|
