rpm/coq
SHA256
1
0
Fork 0
forked from pool/coq
Code Pull Requests Activity

Commit Graph

  • ea92abb9c6 Accepting request 1199381 from science factory Ana Guerrero 2024-09-09 12:44:11 +0000
  • 9c22c89df3 - Update to version 8.20.0. The most impactful changes are: * A mechanism to add user-defined rewrite rules to Coq's reduction mechanisms; see chapter "User-defined rewrite rules". * Support for primitive strings in terms. * Reduction of the bytecode segment size, which in turn means that .vo files might now be considerably smaller. - Notable breaking changes: * Syntactic global references passed through the using clauses of auto-like tactics are now handled as plain references rather than interpreted terms. In particular, their typeclass arguments will not be inferred. In general, the previous behaviour can be emulated by replacing auto using foo with pose proof foo; auto. * Argument order for the Ltac2 combinators List.fold_left2 and List.fold_right2 changed to be the same as in OCaml. * Importing a module containing a mutable Ltac2 definition does not undo its mutations. Replace Ltac2 mutable foo := some_expr. with Ltac2 mutable foo := some_expr. Ltac2 Set foo := some_expr. to recover the previous behaviour. * Some renaming in the standard library. Deprecations are provided for a smooth transition. - For more details, see the change log in coq-doc. devel Aaron Puchert 2024-09-07 15:01:23 +0000
  • 516fd9bf5c Accepting request 1184115 from science Dominique Leuenberger 2024-07-01 09:21:23 +0000
  • 4fddaa2fa7 - Update to version 8.19.2. * Fixed a regression from Coq 8.18 in the presence of a defined field in a primitive Record. * Fixed an issue where the printer was sometimes failing to use a prefix or infix custom notation whose right-hand side refers to a different custom entry. * Fixed abstract failure in the presence of admitted goals in the surrounding proof. * Fixed issues when using Ltac2 in VsCoq due to incorrect state handling of Ltac2 notations. * Fixed Include on a module containing a record declared with Primitive Projections. * Fixed an issue in Fixpoint with no arguments. * Position error/warning tooltips correctly when multibyte UTF-8 characters are present. Aaron Puchert 2024-06-30 17:29:40 +0000
  • 2c5836b4d9 Accepting request 1156169 from science Ana Guerrero 2024-03-08 17:09:09 +0000
  • 8870b507b6 - 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. Aaron Puchert 2024-03-07 23:33:38 +0000
  • 4a9b6a9784 Accepting request 1142140 from science Ana Guerrero 2024-01-29 21:28:51 +0000
  • 10555467e2 - Cover stdlib with %fdupes. Aaron Puchert 2024-01-28 20:56:18 +0000
  • 042203acb7 - 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). * Tactics 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 (Linux only) 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. Aaron Puchert 2024-01-28 20:41:21 +0000
  • 53f3b27cea Accepting request 1125372 from science Ana Guerrero 2023-11-13 21:21:57 +0000
  • 37bbcb7cbf - Do the right thing if qemu_user_space_build is defined as 0. Aaron Puchert 2023-11-12 23:14:09 +0000
  • 669ef86008 - 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. Aaron Puchert 2023-11-12 22:55:08 +0000
  • d5b741161a - Revert last change: this is now set in ocaml-rpm-macros. Aaron Puchert 2023-11-11 00:35:56 +0000
  • 36d9e6cc14 Accepting request 1121332 from science Ana Guerrero 2023-10-31 19:25:29 +0000
  • ad9d18ea83 - Increase stack size limit to fix build on riscv64. Aaron Puchert 2023-10-30 22:28:37 +0000
  • b65f8cd660 Accepting request 1111685 from science Dominique Leuenberger 2023-09-20 11:25:12 +0000
  • 111d6555f8 - 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. Aaron Puchert 2023-09-17 00:40:53 +0000
  • 01c47874b8 Accepting request 1095883 from science Dominique Leuenberger 2023-06-29 15:28:52 +0000
  • edfae7dd86 - 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. Aaron Puchert 2023-06-28 23:04:37 +0000
  • 46ec0e01a2 Accepting request 1075082 from science Dominique Leuenberger 2023-03-29 21:27:14 +0000
  • 312f3c055e - 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. Aaron Puchert 2023-03-29 01:36:33 +0000
  • 0236a47897 Accepting request 1061434 from science Dominique Leuenberger 2023-01-27 09:16:34 +0000
  • 02f83d6668 - 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. Aaron Puchert 2023-01-26 23:03:52 +0000
  • 2cf283a0cb Accepting request 1038367 from science Dominique Leuenberger 2022-11-27 11:53:03 +0000
  • 44fe8f3492 - 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. Aaron Puchert 2022-11-26 22:51:51 +0000
  • fe1a6bfdf5 Accepting request 1002206 from science Dominique Leuenberger 2022-09-09 16:28:00 +0000
  • 6dee5e36dc - 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. Aaron Puchert 2022-09-08 21:21:24 +0000
  • da554d4f31 Accepting request 980409 from science Dominique Leuenberger 2022-06-02 19:54:19 +0000
  • 9b2016e937 - 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. Aaron Puchert 2022-06-01 21:48:29 +0000
  • 018f3b6c32 Accepting request 964734 from science Dominique Leuenberger 2022-03-25 20:54:34 +0000
  • 660b7caabf - 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). Aaron Puchert 2022-03-24 22:47:19 +0000
  • c2d62a169f Accepting request 946708 from science Dominique Leuenberger 2022-01-16 22:18:05 +0000
  • da8ddfc177 - 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. Aaron Puchert 2022-01-15 19:42:50 +0000
  • 9ba52e1735 Accepting request 940115 from science Dominique Leuenberger 2021-12-13 19:44:29 +0000
  • 4e1d685c4c - 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. Aaron Puchert 2021-12-12 21:22:34 +0000
  • 14545c8f27 Accepting request 926632 from science Dominique Leuenberger 2021-10-21 21:55:25 +0000
  • 96b9f456bb - Fix typo in condition. Aaron Puchert 2021-10-21 00:03:26 +0000
  • f595c547f2 OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=34 Aaron Puchert 2021-10-20 23:30:38 +0000
  • fc4ca13aa9 Accepting request 916845 from science Dominique Leuenberger 2021-09-04 20:35:26 +0000
  • eed432c976 - Add documentation package based on github.com/coq/doc until we can build the documentation directly in OBS. Aaron Puchert 2021-09-04 12:54:51 +0000
  • c2dbf14392 Accepting request 889764 from science Dominique Leuenberger 2021-05-02 16:36:08 +0000
  • d0636cc204 Accepting request 889763 from home:aaronpuchert Aaron Puchert 2021-05-01 21:33:33 +0000
  • 8afc5fda0d Accepting request 875244 from science Dominique Leuenberger 2021-02-26 20:59:54 +0000
  • 7777299bac - Update to version 8.13.1. * Fix arities of VM opcodes for some floating-point operations that could cause memory corruption. Aaron Puchert 2021-02-25 23:36:41 +0000
  • f8c1a8965d Accepting request 870152 from science Dominique Leuenberger 2021-02-08 10:47:41 +0000
  • 2b13e5c237 Accepting request 870151 from home:aaronpuchert Aaron Puchert 2021-02-07 23:06:30 +0000
  • cd33483f40 Accepting request 855595 from science Dominique Leuenberger 2020-12-14 17:09:33 +0000
  • e78df31e71 - Update to version 8.12.2. Fixes two impacting 8.12 regressions: * Fixed a regression causing notations mentioning a coercion to be ignored. * Fixed a regression causing incomplete inference of implicit arguments in exists. Aaron Puchert 2020-12-13 17:13:48 +0000
  • e01d1ee19a Accepting request 849178 from science Dominique Leuenberger 2020-12-04 20:27:53 +0000
  • c3225375ef - Update to version 8.12.1. This contains mostly bug fixes: * Polymorphic side-effects inside monomorphic definitions were incorrectly handled as not inlined. This allowed deriving an inconsistency. * Regression in error reporting after SSReflect's case tactic. A generic error message "Could not fill dependent hole in apply" was reported for any error following case or elim. * Several bugs with Search. * The details environment introduced in coqdoc in Coq 8.12 can now be used as advertised in the reference manual. * View menu "Display parentheses" introduced in CoqIDE in Coq 8.12 now works correctly. Aaron Puchert 2020-11-17 22:12:19 +0000
  • 2cfc0855cf Accepting request 828043 from home:marxin:memory-constraint Aaron Puchert 2020-08-20 12:25:06 +0000
  • da3c57af9f Accepting request 824553 from science Dominique Leuenberger 2020-08-06 08:42:44 +0000
  • 226481272d - Update to version 8.12.0. * New binder notation for non-maximal implicit arguments using [] allowing to set and see the implicit status of arguments immediately. * New notation Inductive "I A | x : s := ..." to distinguish the uniform from the non-uniform parameters in inductive definitions. * More robust and expressive treatment of implicit inductive parameters in inductive declarations. * Improvements in the treatment of implicit arguments and partially applied constants in notations, parsing of hexadecimal number notation and better handling of scopes and coercions for printing. * A correct and efficient coercion coherence checking algorithm, avoiding spurious or duplicate warnings. * An improved Search command which accepts complex queries. This takes precedence over the now deprecated ssreflect search. * Many additions and improvements of the standard library. * Improvements to the reference manual include a more logical organization of chapters along with updated syntax descriptions that match Coq's grammar in most but not all chapters. Aaron Puchert 2020-08-05 21:55:19 +0000
  • b413004247 Accepting request 812064 from science Dominique Leuenberger 2020-06-07 19:37:49 +0000
  • de34c223a6 - Update to version 8.11.2. * Fixed a kernel issue where using Require inside a section caused an anomaly when closing the section. * Fixed normalization in conclusion of custom induction scheme. * Fixed a loss of location of some tactic errors. * Ignore -native-compiler option when built without native compute support. * Fixed a segfault issue with CoqIDE completion. * Highlighting style is now consistently applied to all three buffers of CoqIDE. Aaron Puchert 2020-06-06 12:12:35 +0000
  • 7aa2118d49 Accepting request 792575 from science Dominique Leuenberger 2020-04-09 21:17:16 +0000
  • 402a945db4 - Update to version 8.11.1, with upstream support for OCaml 4.10. * Allow more inductive types in Unset Positivity Checking mode. * Fixed bugs in dealing with precedence of notations in custom entries. * In primitive floats, print a warning when parsing a decimal value that is not exactly a binary64 floating-point number. For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't. * Fixed an issue in CoqIDE about compiling file paths containing spaces. * Fixed an issue where Extraction Implicit on the constructor of a record was leading to an anomaly. - Remove now obsolete ocaml-410-build.patch. Aaron Puchert 2020-04-08 23:19:34 +0000
  • 81797fca28 Accepting request 789593 from science Dominique Leuenberger 2020-03-30 21:02:48 +0000
  • 9476266733 - Add patch tag. Aaron Puchert 2020-03-29 22:22:42 +0000
  • c327875f86 - Always require ocamlfind(num), seems we can't use %pkg_vcmp here. Aaron Puchert 2020-03-29 22:17:57 +0000
  • 504ea95368 - The num library is required for OCaml 4.06 or later. - Add ocaml-410-build.patch: fix build with OCaml 4.10. Aaron Puchert 2020-03-29 22:08:07 +0000
  • d261ad0795 Accepting request 774603 from science Dominique Leuenberger 2020-02-15 21:26:16 +0000
  • fcdc0a168f Accepting request 774600 from home:aaronpuchert Aaron Puchert 2020-02-15 19:32:26 +0000
  • cac1a7f4c9 Accepting request 747961 from science Dominique Leuenberger 2019-11-30 09:36:53 +0000
  • f2a34ee4a1 - Fix findlib build dependency. Aaron Puchert 2019-11-13 01:44:06 +0000
  • bc5f5c08e6 - Use memory-constraints package to limit number of threads. - Add dependencies to fix installation issues. Aaron Puchert 2019-11-03 18:30:53 +0000
  • c14d724bca - Fix typo. Aaron Puchert 2019-09-25 21:33:11 +0000
  • ded928ac6b - Adjust number of jobs manually. Aaron Puchert 2019-09-25 21:30:35 +0000
  • a6698df172 - Remove line break, apparently that doesn't work. Aaron Puchert 2019-09-25 20:43:30 +0000
  • 057e1be183 - Prevent OOM by limiting the number of threads. Aaron Puchert 2019-09-25 20:17:00 +0000
  • 928f86c4f8 Accepting request 733035 from home:aaronpuchert Christian Goll 2019-09-25 09:10:33 +0000