| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Update doc/sphinx/addendum/micromega.rst
Co-authored-by: Jason Gross <jasongross9@gmail.com>
Update theories/micromega/ZifyInt63.v
Co-authored-by: Jason Gross <jasongross9@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.
|
|
|
|
In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in
1.10, see
https://github.com/ocaml/Zarith/issues/58
|
|
We still link num in `coqc` , that will be removed in a separate step.
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
This is necessary to support OCaml 4.11 in development.
|
|
Reviewed-by: vbgl
|
|
zify used to generate many syntactic positivity constraints when translating a goal
from nat to Z. For instance, to state that the product of 2 integers
is positive. Instead, lia performs an interval analysis that is more semantic.
The bug was that the interval analysis was performed after the
elimination of equations. The current workaround is to perform
interval analysis before and after eliminating equations.
bla
|
|
The elimination of let bindings is performing a convertibility check in
order to deal with type aliases.
|
|
Add Zify <X> are documented.
Add <X> is deprecated as it clashed with the standard Add command
|
|
|
|
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
- insert boolean constraint (b = true \/ b = false)
- add specs for b2z
- zify_post_hook performs a case-analysis over boolean constraints
- Stricter typing constraints for `zify` declared operators
The type is syntactically checked against the declaration of injections.
Some explicit casts may need to be inserted.
|
|
The syntax of formulae is extended to support boolean constants (true,
false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb,
Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and
Z.ltb.
|
|
Analysis by Jason Gross:
> The previous semantics was to reset the file offset to 0 during the
> unlock operation, unless it fails, in which case you'd roll back the
> file offset to it's present position (and very dubiously not report
> any issues). The new semantics say to always roll the file offset
> back to it's initial position, meaning that the position is at the
> end of the file after unlocking. As far as I can tell, this results
> in appending marshelled blobs to the cache file on every call to
> add, rather than overwriting the cache file with the marshelled blob
> of the updated table. Presumably unmarshelling the concatenation of
> marshelled data can result in segfaults somehow? This also explains
> why the bug only shows up sometimes; you need to get the system into
> a state where it writes to the cache in a way that concatenates
> blobs in the right way, but once you have such a cache you'll
> segfault every time you read from it.
>
> I think we should probably assert false in the with block, or just
> remove it entirely http://man7.org/linux/man-pages/man3/lockf.3.html
> doesn't say anything about lockf erroring on unlocking). If we start
> seeing errors, we can turn it into a warning.
Closes: #12072
|
|
Reviewed-by: vbgl
|
|
Reviewed-by: maximedenes
|
|
|
|
This completes a pure Dune bootstrap of Coq.
There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.
TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.
Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?
|
|
Reviewed-by: ppedrot
|
|
- 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`.
|
|
|
|
in favor of the one in the OCaml standard library.
|
|
Using disable=true in .ocamlformat and disable=false in sub
.ocamlformat works fine.
Note that disable=true must be after the `profile` setting otherwise
it gets reset
|
|
IMHO it is a bit more logical, WDYT?
|
|
|
|
|
|
|
|
This enforces monomorphism everywhere possible.
|
|
Add headers to a few files which were missing them.
|
|
Only significant change is in gcd / lcm which now are typed in `Z.t`
|
|
- zify_iter_specs is entirely in OCaml
- zify_op has been improved
* The generation of proof-terms is more direct
* It does not `rewrite` but instead either performs
a `pose proof` or a `change`
* The support for `and`, `or`, `not`, arrow is hardcoded
* Avoid generating duplicate hypotheses such as 0 <= Z.of_nat x
- zify_elim_let is entirely in OCaml (no Ltac callback)
[micromega] fix stack overflow
Less naive computation of bounds (online elimination of duplicates)
|
|
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
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
- The cutting plane has been (sometimes) improved to generate stronger
cuts.
- There is now some support for profiling the Simplex
see documentation for Show Lia Profile.
|
|
Reviewed-by: maximedenes
|
|
|
|
- Add an instance to ZifyInst to instruct zify that
0 < x -> 0 < y -> 0 < Z.pow x y
- More aggressive interval analysis to bound non-linear monomials.
|
|
PR #9725 fixes completness bugs introduces some inefficiency. The
current PR intends to fix the inefficiency while retaining
completness. The fix removes a pre-processing step and instead relies
on a more elaborate proof format introducing positivity constraints on
the fly.
Solve bootstrapping issues: RMicromega <-> Rbase <-> lia.
Fixes #11063 and fixes #11242 and fixes #11270
|
|
|
|
|
|
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
```
|
|
Add missing zify class instances for `Pos.pred_double`, `Pos.pred_N`,
`Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`,
`Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, `Z.quot2`, `isZero`, and
`isLeZero`. Instances for `isZero` and `isLeZero` are useful to provide new
zify instances by using Micromega tactics.
|
|
|
|
|
|
|
|
|
|
|
|
- Fix reification of overloaded operators
(triggers convertibility checks with existing terms)
- Zify instances need not be in hnf
- Fix specification of bool operators
- Add (limited) support for comparison
fixes #10779
|
