| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
extraction.
Reviewed-by: maximedenes
|
|
|
|
Performance bug of PrimFLoat.compare with native_compute
When adapting Coq.Interval with @erikmd and @silene, we noticed that
PrimFLoat.compare is taking a lot of time with native_compute (much
more than with vm_compute).
This comes from the implementation using the OCaml polymorphic
comparison instead of the float comparison.
|
|
Instead, we export in Safe_typing the current module declaration.
|
|
Not sure if it's possible to see it without a plugin.
|
|
- allow viewing the internal representation of uglobal and universe
(with universe, this replaces the "map" function. I kept exists and
for_all as they felt somewhat convenient)
- add universe set and map modules (currently unused but they're natural)
|
|
|
|
|
|
|
|
preparation for direct discharge
|
|
|
|
We make a temporary directory for these files and cleanup at process
exit. The temporary directory means we don't have to guess what
extensions ocaml will produce, we can just delete everything there.
We use Lazy to avoid spamming unused directories when ahead-of-time
compiling without actually using native casts / nativenorm (typically
stdlib files).
Sadly ocaml has "create temp file" but not "create temp dir", so we
have to copy the name generation code.
Fix #10495
|
|
This doesn't actually have anything to do with positivity AFAICT, we
just want the number of non-parameter arguments.
|
|
|
|
|
|
|
|
(Fixes #11321)
It has the added advantage of performing 6 less 64-bit operations per
long multiplication.
|
|
The sign bit is supposed to be zero, so no need to mask it out. If it was
not zero, most of the algorithms in this file would fail horribly.
|
|
|
|
~strict flag
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
Issue #10603
|
|
|
|
It gets thrown away if the inductive is declared in a section anyway,
and there is no user syntax to specify it.
|
|
One should generally push contexts with ~strict:true when the context is a monomorphic one (all univs > Set) except for template polymorphic inductives (>= Prop) and ~strict:false for universe polymorphic ones (>= Set). Includes fixes from Gaëtan's and Emilio's reviews
|
|
This is a follow up of #11010 ; I've realized that for example in #11123
a large part of the patch is detabification as indeed the files are
mixed in tabs/space style so developers are forced to do the cleanup
each time they work on them.
Command used:
```
for i in `find . -name '*.c' -or -name '*.h'; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
Checked empty diff with `git diff --ignore-all-space`
|
|
This approach using `type t = { sec_prev: t option; sec_... }` makes
it easy to update sections using the record update syntax, but
impossible to statically ensure that an operation only affects the
current section.
We may instead consider using `type t = section * section list` which
needs some boilerplate to update.
|
|
This is the minimal set of changes requires for Coq to build under 2.0
mode. We may likely take advantage of some more new features.
Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune
in older versions as it will install a secondary compiler.
|
|
and do not run template_candidate in the upper layers when the
template attribute is given.
This means we can use an over-approximation in the upper layer
implementation of template_candidate (returning false even in cases
which the kernel may accept) if we ever want to.
|
|
Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.
A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.
Also fixes #10504.
|
|
Rels that exist inside the environment at the time of the closure creation
are fetched in the global environment, while we only use the local list of
relevance for FRels. All the infrastructure was implicitly relying on this
kind of behaviour before the introduction of SProp.
Fixes #11150: pattern is 10x slower in Coq 8.10.0
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
|
|
* Fix the implementations and add tests
* Change shift from int63 to Z (was always used as a Z)
* Update FloatLemmas.v accordingly
Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
|
|
* Add a related test-suite in compare.v (generated by a bash script)
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
|
|
|
|
is_float was relying on Obj.tag triggering a check that we are in the
OCaml heap which is expensive. On extreme examples, this can lead to a
global 2x speedup.
Thanks to Maxime Dénès and Jacques-Henri Jourdan for their help in
diagnosing this.
|
|
Flag -fexcess-precision=standard is not enough on x86_32
where -msse2 -mfpmath=sse is required (-msse is not enough)
to avoid double rounding issues in the VM.
Most floating-point operation are now implemented in C because OCaml
is suffering double rounding issues on x86_32 with 80 bits extended
precision registers used for floating-point values, causing double
rounding making floating-point arithmetic incorrect with respect to
its specification.
Add a runtime test for double roundings.
|
|
* map special floats to registered CRef's
* kernel/float64.mli: add {is_infinity, is_neg_infinity} functions
* kernel/float64.ml: Replace string_of_float with a safe pretty-printing function
Namely:
let to_string_raw f = Printf.sprintf "%.17g" f
let to_string f = if is_nan f then "nan" else to_string_raw f
Summary:
* printing a binary64 float in 17 decimal places and parsing it again
will yield the same float, e.g.:
let f1 = 1. +. (0x1p-53 +. 0x1p-105)
let f2 = float_of_string (to_string f1)
f1 = f2
* OCaml's string_of_float gives a sign to nan values which shouldn't be
displayed as all NaNs are considered equal here.
|
|
|
