| Age | Commit message (Collapse) | Author |
|---|
|
We also get rid of ploc.ml, now useless, relying a priori on more
robust code in lStream.ml for location reporting (see
e.g. parse_parsable in grammar.ml).
|
|
Close #14074
|
|
This removes the need for the remote counter.
|
|
Fix #13930
|
|
We introduce a new package structure for Coq:
- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`
This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.
The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.
Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.
There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.
This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.
IMHO the plan should work fine.
|
|
This has been in the TODO queue for a long time, and indeed
I have recently seen some trouble with users passing two .v files to
Coq, which it isn't a) tested, b) supported.
Moreover, it doesn't even work correctly in 8.13 due to some other
changes in the toplevel related to auxiliary files.
(*) https://stackoverflow.com/questions/66261987/compiling-multiple-coq-files-does-not-work
|
|
them more stable.
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: silene
Ack-by: SkySkimmer
|
|
|
|
Contrarily to the comments, Coq_config.date was not the "release date" but
just another "compile date".
|
|
Deprecated since 6dd9e003c289a79b0656e7c6f2cc59935997370c (2014)
|
|
|
|
|
|
We also spill (some) non-generic arguments and initialization code
out of coqargs and to coqtop, namely colors for the terminal. There are
more of these, left to later commits.
|
|
This component holds the code for initializing Coq:
- parsing arguments not specific to the toplevel
- initializing all components from vernac downwards (no stm)
This commit moves stm specific arguments parsing to stm/stmargs.ml
|
|
|
|
coqide calls coqidetop -batch, if you are in -async-proof on then
coqidetop spawns a worker and passes -batch to it. At some point,
I could not find the commit, this made the worker die.
On linux it seems it works anyway, but on windows this death is
perceived by coqide which then does not start.
|
|
|
|
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
|
|
|
