| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: SkySkimmer
Ack-by: gadmm
|
|
We introduce the `with_lock` combinator that locks a mutex in an atomic fashion.
This ensures that exceptions thrown by signals will not leave the system in a
deadlocked state.
|
|
|
|
As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.
It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.
We thus remove all bitrotten dead code.
|
|
This tends to confuse the OCaml compiler, for good reasons. Indeed, if
there are mutable fields, the generated code cannot wait for the function
to be fully applied. It needs to recover the value of the mutable fields
as early as possible, and thus to create a closure.
Example:
let foo {bar} x = ...
is compiled as
let foo y = match y with {bar} -> fun x -> ...
|
|
|
|
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.
|
|
|
|
|
|
|
|
Also added a generic way of temporarily disabling a warning.
Also added try_finalize un lib/utils.ml.
|
|
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
|
|
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
We represent entries in the graph with integers instead of levels and
add a table remembering the corresponding association in the graph.
|
|
We expose the representation function in UGraph and change the printer
signature to work over the representation instead of the abstract type.
Similarly, the topological sorting algorithm is moved to Vernacentries.
It is now even simpler.
|
|
Instead we export a representation function that gives a high-level view
of the data structure in terms of constraints.
|
|
|
|
On windows we provide a way to set environment variables
local to a coq installation by providing a file
named "coq_environment.txt" containing KEY="value" pairs.
No space between KEY and = is allowed, values are in
quotes according to OCaml's escaping conventions.
The file is line-directed, illformed lines are skipped.
|
|
|
|
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
|
|
erroneously caught
Reviewed-by: ppedrot
|
|
Fixes #7430 and fixes #10968
This commit makes the following changes:
- Add an exception `Signal` used to convert OCaml signals to exceptions.
`Signal` is registered as critical in `CErrors` to avoid being caught in the
wrong `with` clauses.
- Make `Control.timeout` into a safer interface based on `option` instead of
exceptions.
- Modify `tclTIMEOUT` to fail with `CErrors.Timeout` instead of
`Logic_monad.Tac_timeout`, as was already advertised in the ocamldoc documentation.
- Removes `Logic_monad.Tac_timeout` altogether because it no longer has a use.
|
|
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
We do not have to increase the step counter when out of the threaded mode since
this counter is only relevant when in that mode.
|
|
Reviewed-by: herbelin
Ack-by: gares
Ack-by: ejgallego
|
|
Add menu item that uses this
|
|
An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.
We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
|
|
We try to avoid reallocating the map in two different ways.
- We only add a value when actually needed.
- We compute the union of maps with the first element as a starting point.
|
|
A set was created only to be folded over. Since the list is ensured to
be duplicate-free, there is no point in creating the former, we just
fold over the list directly.
|
|
|
|
In the current proof save path, the kernel can raise an exception when
checking a proof wrapped into a future.
However, in this case, the future itself will "fix" the produced
exception, with the mandatory handler set at the future's creation
time.
Thus, there is no need for the declare layer to mess with exceptions
anymore, if my logic is correct. Note that the `fix_exn` parameter to
the `Declare` API was not used anymore.
This undoes 77cf18eb844b45776b2ec67be9f71e8dd4ca002c which comes from
pre-github times, so unfortunately I didn't have access to the
discussion.
We need to be careful in `perform_buildp` as to catch the `Qed` error
and properly notify the STM about it with `State.exn_on`; this was
previously done by the declare layer using a hack [grabbing internal
state of the future, that the future itself was not using as it was
already forced], but we now do it in the caller in a more principled
way.
This has been tested in the case that tactics succeed but Qed fails
asynchronously.
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
|
We tweak the message a bit.
|
|
|
|
|
|
|
|
See CEP#44 for futher details.
|
|
This is useful as witnessed by #11829 , as some errors printers do
still fail, so it costs little to have both backtraces.
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
Add headers to a few files which were missing them.
|
|
|
|
Reviewed-by: ppedrot
|
