Up to [cvs.NetBSD.org] / pkgsrc / lang / coq
Request diff between arbitrary revisions
Default branch: MAIN
Revision 1.11 / (download) - annotate - [select for diffs], Tue Feb 9 22:37:43 2021 UTC (4 months, 1 week ago) by dholland
CVS Tags: pkgsrc-2021Q1-base, pkgsrc-2021Q1, HEAD
Changes since 1.10: +26 -7 lines
Diff to previous 1.10 (colored)
Update lang/coq to 8.12.2. Fixes build with current ocaml. Note: this update includes the import semantics fixes from 8.11 that break a lot of developments. pkgsrc change: docs build now works. Summary of changes in 8.12: Coq version 8.12 integrates many usability improvements, in particular with respect to notations, scopes and implicit arguments, along with many bug fixes and major improvements to the reference manual. The main changes include: 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. Note that 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. Additionally, the omega tactic is deprecated in this version of Coq, and we recommend users to switch to lia in new proof scripts (see also the warning message in the corresponding chapter). Summary of changes in 8.11: The main changes brought by Coq version 8.11 are: Ltac2, a new tactic language for writing more robust larger scale tactics, with built-in support for datatypes and the multi-goal tactic monad. Primitive floats are integrated in terms and follow the binary64 format of the IEEE 754 standard, as specified in the Coq.Float.Floats library. Cleanups of the section mechanism, delayed proofs and further restrictions of template polymorphism to fix soundness issues related to universes. New unsafe flags to disable locally guard, positivity and universe checking. Reliance on these flags is always printed by Print Assumptions. Fixed bugs of Export and Import that can have a significant impact on user developments (common source of incompatibility!). New interactive development method based on vos interface files, allowing to work on a file without recompiling the proof parts of their dependencies. New Arguments annotation for bidirectional type inference configuration for reference (e.g. constants, inductive) applications. New refine attribute for Instance can be used instead of the removed Refine Instance Mode. Generalization of the under and over tactics of SSReflect to arbitrary relations. Revision of the Coq.Reals library, its axiomatisation and instances of the constructive and classical real numbers. Additionally, while the omega tactic is not yet deprecated in this version of Coq, it should soon be the case and we already recommend users to switch to lia in new proof scripts (see also the warning message in the corresponding chapter). The full (huge) changelog is here: https://coq.inria.fr/distrib/V8.12.2/refman/changes.html
Revision 1.10 / (download) - annotate - [select for diffs], Sun Mar 1 05:25:13 2020 UTC (15 months, 2 weeks ago) by dholland
CVS Tags: pkgsrc-2020Q4-base, pkgsrc-2020Q4, pkgsrc-2020Q3-base, pkgsrc-2020Q3, pkgsrc-2020Q2-base, pkgsrc-2020Q2, pkgsrc-2020Q1-base, pkgsrc-2020Q1
Changes since 1.9: +2 -1 lines
Diff to previous 1.9 (colored)
lang/coq now needs adwaita-icon-theme. (without it the new coqide is missing things, and it seems to specifically refer to adwaita-icon-theme by name) Bump PKGREVISION to 1, since coqide is a default-on option.
Revision 1.9 / (download) - annotate - [select for diffs], Fri Jan 24 15:54:48 2020 UTC (16 months, 3 weeks ago) by jaapb
Changes since 1.8: +4 -3 lines
Diff to previous 1.8 (colored)
Updated lang/coq to version 8.10.2. Changes include: - native 63-bit machine integers; - a new sort of definitionally proof-irrelevant propositons: SProp; - private universes for opaque polymorphic constants; - string notations and numeral notations; - a new simplex-based proof engine for the tactics lia, nia, lra and nra; - new introduction patterns for SSReflect; - a tactic to rewrite under binders: under; - easy input of non-ASCII symbols in CoqIDE, which now uses GTK3. and many small improvements and bugfixes.
Revision 1.8 / (download) - annotate - [select for diffs], Sun Nov 3 19:03:57 2019 UTC (19 months, 2 weeks ago) by rillig
CVS Tags: pkgsrc-2019Q4-base, pkgsrc-2019Q4
Changes since 1.7: +43 -43 lines
Diff to previous 1.7 (colored)
lang: align variable assignments pkglint -Wall -F --only aligned --only indent -r No manual corrections.
Revision 1.7 / (download) - annotate - [select for diffs], Mon Sep 2 13:33:23 2019 UTC (21 months, 2 weeks ago) by adam
CVS Tags: pkgsrc-2019Q3-base, pkgsrc-2019Q3
Changes since 1.6: +2 -2 lines
Diff to previous 1.6 (colored)
Rewrite PYTHON_VERSIONS_ACCEPTED to PYTHON_VERSIONS_INCOMPATIBLE
Revision 1.6 / (download) - annotate - [select for diffs], Fri Apr 26 12:44:43 2019 UTC (2 years, 1 month ago) by roy
CVS Tags: pkgsrc-2019Q2-base, pkgsrc-2019Q2
Changes since 1.5: +2 -2 lines
Diff to previous 1.5 (colored)
More packages wave bye-bye to python34 and python35
Revision 1.5 / (download) - annotate - [select for diffs], Wed Mar 6 09:28:23 2019 UTC (2 years, 3 months ago) by jaapb
CVS Tags: pkgsrc-2019Q1-base, pkgsrc-2019Q1
Changes since 1.4: +27 -23 lines
Diff to previous 1.4 (colored)
Updated lang/coq to version 8.9.0. Many improvements and fixes, but none that appear to break compatibility. For more details see the CHANGES file.
Revision 1.4 / (download) - annotate - [select for diffs], Thu Aug 2 12:57:03 2018 UTC (2 years, 10 months ago) by jaapb
CVS Tags: pkgsrc-2018Q4-base, pkgsrc-2018Q4, pkgsrc-2018Q3-base, pkgsrc-2018Q3
Changes since 1.3: +31 -23 lines
Diff to previous 1.3 (colored)
Updated package lang/coq to version 8.8.1. The list of improvements, additions, bugfixes and so on is quite large; those interested can refer to the CHANGES file in the distribution. The reference manual has been fully ported to Sphinx.
Revision 1.3 / (download) - annotate - [select for diffs], Wed Jan 10 16:26:53 2018 UTC (3 years, 5 months ago) by jaapb
CVS Tags: pkgsrc-2018Q2-base, pkgsrc-2018Q2, pkgsrc-2018Q1-base, pkgsrc-2018Q1
Changes since 1.2: +6 -1 lines
Diff to previous 1.2 (colored)
Updated package lang/coq to version 8.7.1. This is a compatibility release with OCaml 4.06.0. It also contains many bugfixes, documentation improvements and user message improvements.
Revision 1.2 / (download) - annotate - [select for diffs], Fri Oct 10 08:39:08 2014 UTC (6 years, 8 months ago) by jaapb
CVS Tags: pkgsrc-2017Q4-base, pkgsrc-2017Q4, pkgsrc-2017Q3-base, pkgsrc-2017Q3, pkgsrc-2017Q2-base, pkgsrc-2017Q2, pkgsrc-2017Q1-base, pkgsrc-2017Q1, pkgsrc-2016Q4-base, pkgsrc-2016Q4, pkgsrc-2016Q3-base, pkgsrc-2016Q3, pkgsrc-2016Q2-base, pkgsrc-2016Q2, pkgsrc-2016Q1-base, pkgsrc-2016Q1, pkgsrc-2015Q4-base, pkgsrc-2015Q4, pkgsrc-2015Q3-base, pkgsrc-2015Q3, pkgsrc-2015Q2-base, pkgsrc-2015Q2, pkgsrc-2015Q1-base, pkgsrc-2015Q1, pkgsrc-2014Q4-base, pkgsrc-2014Q4
Changes since 1.1: +2 -2 lines
Diff to previous 1.1 (colored)
Changed package dependencies to reflect lablgtk name change.
Revision 1.1 / (download) - annotate - [select for diffs], Fri Nov 16 14:44:22 2012 UTC (8 years, 7 months ago) by jaapb
CVS Tags: pkgsrc-2014Q3-base, pkgsrc-2014Q3, pkgsrc-2014Q2-base, pkgsrc-2014Q2, pkgsrc-2014Q1-base, pkgsrc-2014Q1, pkgsrc-2013Q4-base, pkgsrc-2013Q4, pkgsrc-2013Q3-base, pkgsrc-2013Q3, pkgsrc-2013Q2-base, pkgsrc-2013Q2, pkgsrc-2013Q1-base, pkgsrc-2013Q1, pkgsrc-2012Q4-base, pkgsrc-2012Q4
Updated package to add 'doc' option and (if given) build documentation, as requested in PR pkg/47152. Bumped PKGREVISION.
This form allows you to request diff's between any two revisions of a file. You may select a symbolic revision name using the selection box or you may type in a numeric name using the type-in text box.