| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
This essentially means storing the abstract universe context in the typeclass
data, and abstracting it when necessary.
|
|
We aditionally return the abstract universe context inside the option. This
is relatively painless as most uses were using the option as a boolean.
|
|
We return the abstract context instead of an arbitrary instantiation.
|
|
|
|
|
|
|
|
|
|
|
|
eval thunks once in prlist_sep_lastsep, make code clearer
add typeclass debug output test
|
|
|
|
|
|
|
|
This is made necessary by the fact that the displayed commit in the header
of the build can be outdated if the build was restarted or took a long time
to start. Sometimes, it is so old that the link to GitHub is a 404.
|
|
As per @JasonGross's request who described a use case for this option in
https://coq.inria.fr/bugs/show_bug.cgi?id=5633 and pending an alternative
solution for this use case.
|
|
|
|
|
|
|
|
|
|
The function turning a side-effect declaration into the corresponding
entry was crazily wrong, as it used a named universe context quantifying
over DeBruijn universe indices. Declaring such entries resulted
in random anomalies.
This fixes bug #5641.
|
|
This is the followup of the previous commit, this time implementing the
correct algorithm in the checker.
|
|
Before this patch, inductive subtyping was enforcing syntactic equality
of the variable instance, instead of reasoning up to alpha-renaming.
|
|
We export a function in UGraph to check that a polymorphic instance is
a subtype of another, instead of rolling up our own in module code.
We also add a few tests for module subtyping in presence of polymorphic
constants.
|
|
Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
|
|
This function was lurking around, waiting to bite anybody willing to use it.
We use instead a better API, correct and much less error-prone.
|
|
|
|
This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
|
|
|
|
|
|
compute.
|
|
|
|
We document the most useful timing targets and variables, how to invoke
them, and what the output looks like.
|
|
|
|
|
|
This commit adds timing scripts from
https://github.com/JasonGross/coq-scripts/tree/master/timing into the
tools folder, and integrates them into coq_makefile and Coq's makefile.
The main added makefile targets are:
- the `TIMING` variable - when non-empty, this creates for each built
`.v` file a `.v.timing` variable (or `.v.before-timing` or
`.v.after-timing` for `TIMING=before` and `TIMING=after`, respectively)
- `pretty-timed TGTS=...` - runs `make $(TGTS)` and prints a table of
sorted timings at the end, saving it to `time-of-build-pretty.log`
- `make-pretty-timed-before TGTS=...`, `make-pretty-timed-after
TGTS=...` - runs `make $(TGTS)`, and saves the timing data to the file
`time-of-build-before.log` or `time-of-build-after.log`, respectively
- `print-pretty-timed-diff` - prints a table with the difference between
the logs recorded by `make-pretty-timed-before` and
`make-pretty-timed-after`, saving the table to
`time-of-build-both.log`
- `print-pretty-single-time-diff BEFORE=... AFTER=...` - this prints a
table with the differences between two `.v.timing` files, and saves
the output to `time-of-build-pretty.log`
- `*.v.timing.diff` - this saves the result of
`print-pretty-single-time-diff` for each target to the
`.v.timing.diff` file
- `all.timing.diff` (`world.timing.diff` and `coq.timing.diff` in Coq's
own Makefile) - makes all `*.v.timing.diff` targets
N.B. We need to make `make pretty-timed` fail if `make` fails. To do
this, we need to get around the fact that pipes swallow exit codes.
There are a few solutions in
https://stackoverflow.com/questions/23079651/equivalent-of-pipefail-in-gnu-make;
we choose the temporary file rather than requiring the shell of the
makefile to be bash.
|
|
Global declarations used to carry universe instances with them, but it
turns out this information is not used anywhere. Instead, instances were
already properly encoded as the first argument of polymorphic definitions.
|
|
|
|
This closes [bug #5596](https://coq.inria.fr/bugs/show_bug.cgi?id=5596).
|
|
This is usable for no-color terminal.
For instance, a typical application in mind is the Coq-generate names
marker which can be rendered with a color if the interface supports it
and a prefix "~" if the interface does not support colors.
|
|
|
|
constant".
|
|
|
|
the monad.
|
|
|
|
|
