Revisions of coq
Ana Guerrero (anag+factory)
accepted
request 1156169
from
Aaron Puchert (aaronpuchert)
(revision 27)
- Update to version 8.19.1. * Fixed incorrect abstraction of sort variables for opaque constants leading to an inconsistency. * Fixed memory corruption with `vm_compute` (rare but more likely with OCaml 5.1). * "Found no matching notation to enable or disable" is now a warning instead of an error. * Fixed undeclared universe with multiple uses of `abstract`. * Fixed incorrect printing of constructor values with multiple arguments, and over-parenthesizing of constructor printing. * Fixed incorrect declared type for Ltac2.FMap.fold.
Ana Guerrero (anag+factory)
accepted
request 1142140
from
Aaron Puchert (aaronpuchert)
(revision 26)
- Update to version 8.19.0. The most impactful changes: * Sort polymorphism makes it possible to share common constructs over `Type`, `Prop` and `SProp`. * The notation `term%_scope` to set a scope only temporarily (in addition to `term%scope` for opening a scope applying to all subterms). * `lazy`, `simpl`, `cbn` and `cbv` and the associated `Eval` and `eval` reductions learned to do head reduction when given flag `head`. * New Ltac2 APIs, improved Ltac2 `exact` and dynamic building of Ltac2 term patterns. * New performance evaluation facilities: `Instructions` to count CPU instructions used by a command and Profiling system to produce trace files. * New command `Attributes` to assign attributes such as `deprecated` to a library file. - Notable breaking changes: * `replace` with `by tac` does not automatically attempt to solve the generated equality subgoal using the hypotheses. Use `by first [assumption | symmetry;assumption | tac]` if you need the previous behaviour. * Removed old deprecated files from the standard library. - Use %fdupes in the documentation package.
Ana Guerrero (anag+factory)
accepted
request 1125372
from
Aaron Puchert (aaronpuchert)
(revision 25)
- Revert last change: this is now set in ocaml-rpm-macros. - Increase stack size limit in QEMU user space builds. Here ulimit has no effect, so we add a wrapper around ocamlopt.opt to PATH that adds "-s ..." to the qemu-<arch> command line.
Ana Guerrero (anag+factory)
accepted
request 1121332
from
Aaron Puchert (aaronpuchert)
(revision 24)
- Increase stack size limit to fix build on riscv64.
Dominique Leuenberger (dimstar_suse)
accepted
request 1111685
from
Aaron Puchert (aaronpuchert)
(revision 23)
- Update to version 8.18.0. * The default locality of `Hint` and `Instance` commands was switched to `export`. * The universe unification algorithm can now delay the commitment to a sort (the algorithm used to pick `Type`). Thanks to this feature many `Prop` and `SProp` annotations can be now omitted. * Ltac2 supports array literals, maps and sets of primitive datatypes such as names (of constants, inductive types, etc) and fine-grained control over profiling. * The warning system offers new categories, enabling finer (de)activation of specific warnings. This should be particularly useful to handle deprecations. * Many new lemmas useful for teaching analysis with Coq are now part of the standard library about real numbers. * The `#[deprecated]` attribute can now be applied to definitions.
Dominique Leuenberger (dimstar_suse)
accepted
request 1095883
from
Aaron Puchert (aaronpuchert)
(revision 22)
- Update to version 8.17.1. * Fixed incorrect paths emitted by coqdep in some cases for META files which prevented dune builds for plugins from working correctly. * Fixed shadowing of record fields in extraction to OCaml. * Fixed an impossible-to-turn-off debug message "backtracking and redoing byextend on ...". * Fixed a major memory regression affecting MathComp 2. - Classify desktop entry under Science instead of Education. - Add screenshot URL to AppStream metadata.
Dominique Leuenberger (dimstar_suse)
accepted
request 1075082
from
Aaron Puchert (aaronpuchert)
(revision 21)
- Update to version 8.17.0. * Fixed a logical inconsistency due to `vm_compute` in presence of side-effects in the enviroment (e.g. using Back or Fail). * It is now possible to dynamically enable or disable notations. * Support multiple scopes in `Arguments` and `Bind Scope`. * The tactics chapter of the manual has many improvements in presentation and wording. The documented grammar is semi- automatically checked for consistency with the implementation. * Fixes to the `auto` and `eauto` tactics, to respect hint priorities and the documented use of simple apply. This is a potentially breaking change. * New Ltac2 APIs, deep pattern-matching with `as` clauses and handling of literals, support for record types and preterms. * Move from :> to :: syntax for declaring typeclass fields as instances, fixing a confusion with declaration of coercions. * Standard library improvements.
Dominique Leuenberger (dimstar_suse)
accepted
request 1061434
from
Aaron Puchert (aaronpuchert)
(revision 20)
- Build with ocaml-rpm-macros to get proper Requires and Provides for coq-devel. This should prevent incompatibilities with other Ocaml libraries when building native objects against coq-devel.
Dominique Leuenberger (dimstar_suse)
accepted
request 1038367
from
Aaron Puchert (aaronpuchert)
(revision 19)
- Update to version 8.16.1. * Fixed the conversion of `Prod` values in the native compiler. * Added `SProp` check for opaque names in conversion. * Pass the correct environment to compute η-expansion of cofixpoints in VM and native compilation. * Fixed an inconsistency with conversion of primitive arrays, and associated incomplete strong normalization of primitive arrays with `lazy`. * `Print Assumptions` treats opaque definitions with missing proofs (as found in .vos files, produced using -vos) as axioms instead of ignoring them.
Dominique Leuenberger (dimstar_suse)
accepted
request 1002206
from
Aaron Puchert (aaronpuchert)
(revision 18)
- Update to version 8.16.0. * The guard checker (see `Guarded`) now ensures strong normalization under any reduction strategy. * Irrelevant terms (in the `SProp` sort) are now squashed to a dummy value during conversion, fixing a subject reduction issue and making proof conversion faster. * Introduction of reversible coercions, which allow coercions relying on meta-level resolution such as type-classes or canonical structures. Also allow coercions that do not fullfill the uniform inheritance condition. * Generalized rewriting support for rewriting with `Type`-valued relations and in `Type` contexts, using the `Classes.CMorphisms` library. * Added the boolean equality scheme command for decidable inductive types. * Added a `Print Notation` command. * Incompatibilities in name generation for Program obligations, `eauto` treatment of tactic failure levels, use of `ident` in notations, parsing of module expressions. * Standard library reorganization and deprecations. * Improve the treatment of standard library numbers by `Extraction`. - Coq requires ocamlfind at runtime now.
Dominique Leuenberger (dimstar_suse)
accepted
request 980409
from
Aaron Puchert (aaronpuchert)
(revision 17)
- Update to version 8.15.2. * Tactics `intuition` and `dintuition` use `Tauto.intuition_solver` (defined as `auto with *`) instead of hardcoding `auto with *`. This makes it possible to change the default solver with `Ltac Tauto.intuition_solver ::= ...`. * Fixed an uncaught exception `UnableToUnify` with bidirectionality hints. * Fixed multiple CoqIDE bugs. * Fixed an incorrect implementation of `SFClassify`, allowing for a proof of `False` since 8.11.0, due to Axioms present in `Float.Axioms`. - Rename coq.desktop to fr.inria.coq.coqide.desktop as the documentation suggests, add an accompanying metainfo file. - Declare documentation as noarch.
Dominique Leuenberger (dimstar_suse)
accepted
request 964734
from
Aaron Puchert (aaronpuchert)
(revision 16)
- Update to version 8.15.1. * Fixes an inconsistency when using module subtyping with inductive types. * Speeds up CoqIDE on large files. * Fixes a bug where `coqc -vok` was not creating a .vok file. * Fixes a regression in `cbn`. * Improves usability of schemes with `elim foo using scheme with (P0 := ...)` (the `P0` name was not accessible in 8.15.0).
Dominique Leuenberger (dimstar_suse)
accepted
request 946708
from
Aaron Puchert (aaronpuchert)
(revision 15)
- Update to version 8.15.0. * The `apply with` tactic no longer renames arguments unless the compatibility flag `Apply With Renaming` is set. * Improvements to the `auto` tactic family, fixing `Hint Unfold` behavior, and generalizing the use of discrimination nets. * The `typeclasses eauto` tactic has a new `best_effort` option allowing it to return partial solutions to a proof search problem, depending on the mode declarations associated to each constraint. This mode is used by typeclass resolution during type inference to provide more precise error messages. * Many commands and options were deprecated or removed after deprecation and more consistently support locality attributes. * The `Import` command is extended with `import_categories` to select the components of a module to import or not, including features such as hints, coercions, and notations. * A visual Ltac debugger is now available in CoqIDE. * For more details, see refman/changes.html in coq-doc.
Dominique Leuenberger (dimstar_suse)
accepted
request 940115
from
Aaron Puchert (aaronpuchert)
(revision 14)
- Update to version 8.14.1. * Fixed the implementation of persistent arrays used by the VM and native compute so that it uses a uniform representation. Previously, storing primitive floats inside primitive arrays could cause memory corruption. * Fixed missing registration of universe constraints in Module Type elaboration. * Made `abstract` more robust with respect to Ltac `constr` bindings containing existential variables. * Correct support of trailing `let` by tactic `specialize`. * Fixed an anomaly with `Extraction Conservative Types` when extracting pattern-matching on singleton types. * Regular error instead of an anomaly when calling `Separate Extraction` in a module.
Dominique Leuenberger (dimstar_suse)
accepted
request 926632
from
Aaron Puchert (aaronpuchert)
(revision 13)
- Update to version 8.14.0. * The internal representation of match has changed to a more space-efficient and cleaner structure, allowing the fix of a completeness issue with cumulative inductive types in the type- checker. The internal representation is now closer to the user- level view of match, where the argument context of branches and the inductive binders in and as do not carry type annotations. * A new coqnative binary performs separate native compilation of libraries, starting from a .vo file. It is supported by coq_makefile. * Improvements to typeclasses and canonical structure resolution, allowing more terms to be considered as classes or keys. * More control over notations declarations and support for primitive types in string and number notations. * Removal of deprecated tactics, notably omega, which has been replaced by a greatly improved lia, along with many bug fixes. * New Ltac2 APIs for interaction with Ltac1, manipulation of inductive types and printing. * Many changes and additions to the standard library in the numbers, vectors and lists libraries. A new signed primitive integers library Sint63 is available in addition to the unsigned Uint63 library. * For more details, see refman/changes.html in coq-doc.
Dominique Leuenberger (dimstar_suse)
accepted
request 916845
from
Aaron Puchert (aaronpuchert)
(revision 12)
- Add documentation package based on github.com/coq/doc until we can build the documentation directly in OBS.
Dominique Leuenberger (dimstar_suse)
accepted
request 889764
from
Aaron Puchert (aaronpuchert)
(revision 11)
- Update to version 8.13.2. * Fix crash when using vm_compute on an irreducible PArray.set. * Fix crash when loading .vo files containing a vm_compute normalized primitive array. * Fix Ltac2.Array.init computational complexity.
Dominique Leuenberger (dimstar_suse)
accepted
request 875244
from
Aaron Puchert (aaronpuchert)
(revision 10)
- Update to version 8.13.1. * Fix arities of VM opcodes for some floating-point operations that could cause memory corruption.
Dominique Leuenberger (dimstar_suse)
accepted
request 870152
from
Aaron Puchert (aaronpuchert)
(revision 9)
Dominique Leuenberger (dimstar_suse)
accepted
request 855595
from
Aaron Puchert (aaronpuchert)
(revision 8)
- Update to version 8.12.2.
Displaying revisions 1 - 20 of 27