![[BACK]](/icons/back.gif){kind=icon}
Up to [cvs.NetBSD.org] / pkgsrc / lang / coq
Request diff between arbitrary revisions
Default branch: MAIN
Revision 1.39 / (download) - annotate - [select for diffs], Tue Jun 21 02:21:22 2022 UTC (21 months, 4 weeks ago) by dholland
Branch: MAIN
CVS Tags: pkgsrc-2024Q1-base,
pkgsrc-2024Q1,
pkgsrc-2023Q4-base,
pkgsrc-2023Q4,
pkgsrc-2023Q3-base,
pkgsrc-2023Q3,
pkgsrc-2023Q2-base,
pkgsrc-2023Q2,
pkgsrc-2023Q1-base,
pkgsrc-2023Q1,
pkgsrc-2022Q4-base,
pkgsrc-2022Q4,
pkgsrc-2022Q3-base,
pkgsrc-2022Q3,
pkgsrc-2022Q2-base,
pkgsrc-2022Q2,
HEAD
Changes since 1.38: +8 -6
lines
Diff to previous 1.38 (colored) to selected 1.14 (colored)
lang/coq: update to 8.15.2 to make it work with current ocaml. (Update during freeze ok gdt@; even if this version might be broken, that beats definitely broken.) pkgsrc changes: use -native-compiler ondemand as recommended upstream. Now uses dune to build, and uses ocaml-zarith instead of ocaml-num. Upstream change summary: (see https://coq.github.io/doc/v8.15/refman/changes.html for the full change notes) Coq 8.15.2 fixes: - Added: 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 ::= ... (#15866, fixes #7725, by Gaëtan Gilbert). - Fixed: uncaught exception UnableToUnify with bidirectionality hints (#16066, fixes #16063, by Gaëtan Gilbert). - Fixed: multiple CoqIDE bugs (#15938, fixes #15861, #15939, fixes #15882, #15964, fixes #15799, #15984, partially fixes #15873, #15996, #15912, fixes #15903, all by Jim Fehrle). -Fixed: an incorrect implementation of SFClassify, allowing for a proof of False since 8.11.0, due to Axioms present in Float.Axioms. (#16101, fixes #16096, by Ali Caglayan). Coq 8.15.1 fixes: - Fixed: cases of incompletenesses in the guard condition for fixpoints in the presence of cofixpoints or primitive projections (#15498, fixes #15451, by Hugo Herbelin). - Fixed: inconsistency when using module subtyping with squashed inductives (#15839, fixes #15838 (reported by Pierre-Marie Pédrot), by Gaëtan Gilbert). - Fixed: Check for prior declaration of a custom entry was missing for notations in only printing mode (#15628, fixes #15619, by Hugo Herbelin). - Fixed: rewrite_strat regression in 8.15.0 related to Transitive instances (#15577, fixes #15568, by Gaëtan Gilbert). - Fixed: When setoid_rewrite succeeds in rewriting at some occurrence but the resulting equality is the identity, it now tries rewriting in subterms of that occurrence instead of giving up (#15612, fixes #8080, by Gaëtan Gilbert). - Fixed: Ill-typed goals created by clearbody in the presence of transitive dependencies in the body of a hypothesis (#15634, fixes #15606, by Hugo Herbelin). - Fixed: cbn knows to refold fixpoints when Arguments with / and ! was used (#15653, fixes #15567, by Gaëtan Gilbert). - Fixed a bug where coqc -vok was not creating an empty '.vok' file. (#15745, by Ramkumar Ramachandra). - Fixed: Line numbers shown in the Errors panel of CoqIDE were incorrect; they didn't match the error locations in the script panel (#15532, fixes #15531, by Jim Fehrle). - Fixed: anomaly when using proof diffs with no focused goal (#15633, fixes #15578, by Jim Fehrle). - Fixed: Attempted edits to the processed part of a buffer while Coq is busy processing a request are now ignored to ensure "processed" highlighting is accurate (#15714, fixes #15733 and #15675 and #15725, by Jim Fehrle). - Fixed: Ensure that the names of arguments of inductive schemes are distinct so that the new Coq 8.15 preservation of argument names in the with clause of tactics in #13837 works as in Coq 8.14 for these schemes (#15537, fixes #15420, by Hugo Herbelin). Coq 8.15.0 summary: - The apply with tactic no longer renames arguments unless compatibility flag Apply With Renaming is set. - Improvements to the auto tactic family, fixing the 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. Coq 8.14.2 fixes: - Instance warns about the default locality immediately rather than waiting until the instance is ready to be defined. This changes which command warns when the instance has a separate proof: the Instance command itself warns instead of the proof closing command (such as Defined). (#15243, fixes #14704, by Gaëtan Gilbert). Coq 8.14.1 fixes: - Fix 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 (#15081, closes #15070, by Pierre-Marie Pédrot). - Fixed missing registration of universe constraints in Module Type elaboration (#14666, fixes #14505, by Hugo Herbelin). - Fixed: abstract more robust with respect to Ltac constr bindings containing existential variables (#14671, fixes #10796, by Hugo Herbelin). - Fixed: correct support of trailing let by tactic specialize (#15046, fixes #15043, by Hugo Herbelin). - Fixed: anomaly with Extraction Conservative Types when extracting pattern-matching on singleton types (#14669, fixes #3527, by Hugo Herbelin). - Fixed: a regular error instead of an anomaly when calling Separate Extraction in a module (#14670, fixes #10796, by Hugo Herbelin). Coq 8.14.0 summary: - 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. Coq 8.13.2: - Fixed crash when using vm_compute on an irreducible PArray.set (#14005, fixes #13998, by Guillaume Melquiond). - Fix: Never store persistent arrays as VM / native structured values. This could be used to make vo marshalling crash, and probably breaking some other invariants of the kernel (#14007, fixes #14006, by Pierre-Marie Pédrot). - Fix: Ltac2 Array.init no longer incurs exponential overhead when used recursively (#14012, fixes #14011, by Jason Gross). Coq 8.13.1: - Fix arities of VM opcodes for some floating-point operations that could cause memory corruption (#13867, by Guillaume Melquiond). - Added options -v and --version to CoqIDE (#13870, by Guillaume Melquiond). Coq 8.13.0 summary: - Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays. - Introduction of definitional proof irrelevance for the equality type defined in the SProp sort. - Cumulative record and inductive type declarations can now specify the variance of their universes. - Various bugfixes and uniformization of behavior with respect to the use of implicit arguments and the handling of existential variables in declarations, unification and tactics. - New warning for unused variables in catch-all match branches that match multiple distinct patterns. - New warning for Hint commands outside sections without a locality attribute, whose goal is to eventually remove the fragile default behavior of importing hints only when using Require. The recommended fix is to declare hints as export, instead of the current default global, meaning that they are imported through Require Import only, not Require. See the following rationale and guidelines for details. - General support for boolean attributes. - Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior. - Tactic improvements in lia and its zify preprocessing step, now supporting reasoning on boolean operators such as Z.leb and supporting primitive integers Int63. - Typing flags can now be specified per-constant / inductive. - Improvements to the reference manual including updated syntax descriptions that match Coq's grammar in several chapters, and splitting parts of the tactics chapter to independent sections.
Revision 1.38 / (download) - annotate - [select for diffs], Tue Oct 26 10:51:32 2021 UTC (2 years, 5 months ago) by nia
Branch: MAIN
CVS Tags: pkgsrc-2022Q1-base,
pkgsrc-2022Q1,
pkgsrc-2021Q4-base,
pkgsrc-2021Q4
Changes since 1.37: +2 -2
lines
Diff to previous 1.37 (colored) to selected 1.14 (colored)
lang: Replace RMD160 checksums with BLAKE2s checksums All checksums have been double-checked against existing RMD160 and SHA512 hashes The following distfiles could not be fetched (possibly fetched conditionally?): ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-aarch64-unknown-linux-gnu.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-aarch64-unknown-linux-musl.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-aarch64-unknown-netbsd.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-armv7-unknown-netbsd-eabihf.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-i686-unknown-linux-gnu.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-powerpc-unknown-netbsd90.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-sparc64-unknown-netbsd.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-x86_64-apple-darwin.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-x86_64-unknown-freebsd.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-x86_64-unknown-linux-gnu.tar.gz ./lang/rust-bin/distinfo rust-bin-1.54.0/rust-1.54.0-x86_64-unknown-linux-musl.tar.gz ./lang/smlnj/distinfo smlnj-110.73/boot.ppc-unix.tgz ./lang/smlnj/distinfo smlnj-110.73/boot.sparc-unix.tgz ./lang/oracle-jre8/distinfo jce_policy-8.zip ./lang/oracle-jre8/distinfo jre-8u202-linux-i586.tar.gz ./lang/oracle-jre8/distinfo jre-8u202-linux-x64.tar.gz ./lang/oracle-jre8/distinfo jre-8u202-macosx-x64.tar.gz ./lang/oracle-jre8/distinfo jre-8u202-solaris-x64.tar.gz ./lang/oracle-jdk8/distinfo jdk-8u202-linux-i586.tar.gz ./lang/oracle-jdk8/distinfo jdk-8u202-linux-x64.tar.gz ./lang/oracle-jdk8/distinfo jdk-8u202-solaris-x64.tar.gz ./lang/ghc80/distinfo ghc-7.10.3-boot-x86_64-unknown-solaris2.tar.xz ./lang/ghc80/distinfo ghc-8.0.2-boot-i386-unknown-freebsd.tar.xz ./lang/ghc80/distinfo ghc-8.0.2-boot-x86_64-unknown-freebsd.tar.xz ./lang/gcc5-aux/distinfo ada-bootstrap.i386.freebsd.100B.tar.bz2 ./lang/gcc5-aux/distinfo ada-bootstrap.i386.freebsd.84.tar.bz2 ./lang/gcc5-aux/distinfo ada-bootstrap.x86_64.dragonfly.41.tar.bz2 ./lang/gcc5-aux/distinfo ada-bootstrap.x86_64.freebsd.100B.tar.bz2 ./lang/gcc5-aux/distinfo ada-bootstrap.x86_64.freebsd.84.tar.bz2 ./lang/gcc5-aux/distinfo ada-bootstrap.x86_64.solaris.511.tar.bz2 ./lang/rust/distinfo rust-1.53.0-aarch64-apple-darwin.tar.gz ./lang/rust/distinfo rust-1.53.0-aarch64-unknown-linux-gnu.tar.gz ./lang/rust/distinfo rust-1.53.0-aarch64-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-1.53.0-aarch64_be-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-1.53.0-arm-unknown-linux-gnueabihf.tar.gz ./lang/rust/distinfo rust-1.53.0-armv7-unknown-linux-gnueabihf.tar.gz ./lang/rust/distinfo rust-1.53.0-i686-unknown-linux-gnu.tar.gz ./lang/rust/distinfo rust-1.53.0-powerpc-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-1.53.0-powerpc-unknown-netbsd90.tar.gz ./lang/rust/distinfo rust-1.53.0-sparc64-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-1.53.0-x86_64-apple-darwin.tar.gz ./lang/rust/distinfo rust-1.53.0-x86_64-unknown-freebsd.tar.gz ./lang/rust/distinfo rust-1.53.0-x86_64-unknown-illumos.tar.gz ./lang/rust/distinfo rust-1.53.0-x86_64-unknown-linux-gnu.tar.gz ./lang/rust/distinfo rust-std-1.53.0-aarch64-apple-darwin.tar.gz ./lang/rust/distinfo rust-std-1.53.0-aarch64-unknown-linux-gnu.tar.gz ./lang/rust/distinfo rust-std-1.53.0-aarch64-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-std-1.53.0-aarch64_be-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-std-1.53.0-arm-unknown-linux-gnueabihf.tar.gz ./lang/rust/distinfo rust-std-1.53.0-armv7-unknown-linux-gnueabihf.tar.gz ./lang/rust/distinfo rust-std-1.53.0-i686-unknown-linux-gnu.tar.gz ./lang/rust/distinfo rust-std-1.53.0-powerpc-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-std-1.53.0-powerpc-unknown-netbsd90.tar.gz ./lang/rust/distinfo rust-std-1.53.0-sparc64-unknown-netbsd.tar.gz ./lang/rust/distinfo rust-std-1.53.0-x86_64-apple-darwin.tar.gz ./lang/rust/distinfo rust-std-1.53.0-x86_64-unknown-freebsd.tar.gz ./lang/rust/distinfo rust-std-1.53.0-x86_64-unknown-linux-gnu.tar.gz ./lang/smlnj11072/distinfo smlnj-110.72/boot.ppc-unix.tgz ./lang/smlnj11072/distinfo smlnj-110.72/boot.sparc-unix.tgz ./lang/ghc84/distinfo ghc-8.0.2-boot-x86_64-unknown-solaris2.tar.xz ./lang/ghc84/distinfo ghc-8.4.4-boot-i386-unknown-freebsd.tar.xz ./lang/ghc84/distinfo ghc-8.4.4-boot-x86_64-apple-darwin.tar.xz ./lang/ghc84/distinfo ghc-8.4.4-boot-x86_64-unknown-freebsd.tar.xz ./lang/ghc7/distinfo ghc-7.10.3-boot-i386-unknown-freebsd.tar.xz ./lang/ghc7/distinfo ghc-7.6.3-boot-i386-unknown-solaris2.tar.xz ./lang/ghc7/distinfo ghc-7.6.3-boot-powerpc-apple-darwin.tar.xz ./lang/ghc7/distinfo ghc-7.6.3-boot-x86_64-unknown-solaris2.tar.xz ./lang/ghc90/distinfo ghc-8.10.4-boot-x86_64-unknown-solaris2.tar.xz ./lang/ghc90/distinfo ghc-9.0.1-boot-aarch64-unknown-netbsd.tar.xz ./lang/ghc90/distinfo ghc-9.0.1-boot-i386-unknown-freebsd.tar.xz ./lang/ghc90/distinfo ghc-9.0.1-boot-x86_64-apple-darwin.tar.xz ./lang/ghc90/distinfo ghc-9.0.1-boot-x86_64-unknown-freebsd.tar.xz ./lang/openjdk8/distinfo openjdk7/bootstrap-jdk-1.7.76-freebsd-10-amd64-20150301.tar.xz ./lang/openjdk8/distinfo openjdk7/bootstrap-jdk-1.7.76-netbsd-7-sparc64-20150301.tar.xz ./lang/openjdk8/distinfo openjdk7/bootstrap-jdk-1.8.181-netbsd-8-aarch64-20180917.tar.xz ./lang/openjdk8/distinfo openjdk7/bootstrap-jdk7u60-bin-dragonfly-3.6-amd64-20140719.tar.bz2 ./lang/openjdk8/distinfo openjdk7/bootstrap-jdk7u60-bin-dragonfly-3.8-amd64-20140719.tar.bz2 ./lang/go-bin/distinfo go1.14.2.darwin-amd64.tar.gz ./lang/go-bin/distinfo go1.14.2.linux-386.tar.gz ./lang/go-bin/distinfo go1.14.2.linux-amd64.tar.gz ./lang/go-bin/distinfo go1.14.2.linux-arm64.tar.gz ./lang/go-bin/distinfo go1.14.2.linux-armv6l.tar.gz ./lang/go-bin/distinfo go1.14.2.netbsd-arm64.tar.gz ./lang/go-bin/distinfo go1.16beta1.darwin-arm64.tar.gz ./lang/gcc6-aux/distinfo ada-bootstrap.i386.freebsd.100B.tar.bz2 ./lang/gcc6-aux/distinfo ada-bootstrap.x86_64.dragonfly.41.tar.bz2 ./lang/gcc6-aux/distinfo ada-bootstrap.x86_64.freebsd.100B.tar.bz2 ./lang/gcc6-aux/distinfo ada-bootstrap.x86_64.freebsd.84.tar.bz2 ./lang/gcc6-aux/distinfo ada-bootstrap.x86_64.solaris.511.tar.bz2 ./lang/ghc810/distinfo ghc-8.8.4-boot-x86_64-unknown-solaris2.tar.xz ./lang/sun-jre7/distinfo UnlimitedJCEPolicyJDK7.zip ./lang/sun-jre7/distinfo jre-7u80-linux-x64.tar.gz ./lang/sun-jre7/distinfo jre-7u80-solaris-i586.tar.gz ./lang/sun-jre7/distinfo jre-7u80-solaris-x64.tar.gz ./lang/ghc88/distinfo ghc-8.4.4-boot-i386-unknown-freebsd.tar.xz ./lang/ghc88/distinfo ghc-8.4.4-boot-x86_64-apple-darwin.tar.xz ./lang/ghc88/distinfo ghc-8.4.4-boot-x86_64-unknown-freebsd.tar.xz ./lang/ghc88/distinfo ghc-8.4.4-boot-x86_64-unknown-solaris2.tar.xz ./lang/gcc-aux/distinfo ada-bootstrap.i386.dragonfly.36A.tar.bz2 ./lang/gcc-aux/distinfo ada-bootstrap.i386.freebsd.100B.tar.bz2 ./lang/gcc-aux/distinfo ada-bootstrap.i386.freebsd.84.tar.bz2 ./lang/gcc-aux/distinfo ada-bootstrap.x86_64.dragonfly.36A.tar.bz2 ./lang/gcc-aux/distinfo ada-bootstrap.x86_64.freebsd.100B.tar.bz2 ./lang/gcc-aux/distinfo ada-bootstrap.x86_64.freebsd.84.tar.bz2 ./lang/gcc-aux/distinfo ada-bootstrap.x86_64.solaris.511.tar.bz2 ./lang/gcc6/distinfo ecj-4.5.jar ./lang/openjdk11/distinfo bootstrap-jdk-1.11.0.7.10-netbsd-9-aarch64-20200509.tar.xz ./lang/sun-jdk7/distinfo jdk-7u80-linux-x64.tar.gz ./lang/sun-jdk7/distinfo jdk-7u80-solaris-i586.tar.gz ./lang/sun-jdk7/distinfo jdk-7u80-solaris-x64.tar.gz
Revision 1.37 / (download) - annotate - [select for diffs], Thu Oct 7 14:20:48 2021 UTC (2 years, 6 months ago) by nia
Branch: MAIN
Changes since 1.36: +1 -2
lines
Diff to previous 1.36 (colored) to selected 1.14 (colored)
lang: Remove SHA1 hashes for distfiles
Revision 1.36 / (download) - annotate - [select for diffs], Tue Feb 9 22:37:43 2021 UTC (3 years, 2 months ago) by dholland
Branch: MAIN
CVS Tags: pkgsrc-2021Q3-base,
pkgsrc-2021Q3,
pkgsrc-2021Q2-base,
pkgsrc-2021Q2,
pkgsrc-2021Q1-base,
pkgsrc-2021Q1
Changes since 1.35: +7 -6
lines
Diff to previous 1.35 (colored) to selected 1.14 (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.35 / (download) - annotate - [select for diffs], Fri Jan 24 15:54:48 2020 UTC (4 years, 2 months ago) by jaapb
Branch: MAIN
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.34: +6 -7
lines
Diff to previous 1.34 (colored) to selected 1.14 (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.34 / (download) - annotate - [select for diffs], Sun Sep 1 00:51:46 2019 UTC (4 years, 7 months ago) by markd
Branch: MAIN
CVS Tags: pkgsrc-2019Q4-base,
pkgsrc-2019Q4,
pkgsrc-2019Q3-base,
pkgsrc-2019Q3
Changes since 1.33: +2 -1
lines
Diff to previous 1.33 (colored) to selected 1.14 (colored)
coq: patch to build with ocaml 4.08
Revision 1.33 / (download) - annotate - [select for diffs], Thu May 23 10:55:07 2019 UTC (4 years, 10 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2019Q2-base,
pkgsrc-2019Q2
Changes since 1.32: +5 -5
lines
Diff to previous 1.32 (colored) to selected 1.14 (colored)
Updated lang/coq to version 8.9.1. Main changes: * some quality-of-life bug fixes, * many improvements to the documentation, * a critical bug fix related to primitive projections and native_compute, * several additional Coq libraries shipped with the Windows installer.
Revision 1.32 / (download) - annotate - [select for diffs], Wed Mar 6 09:28:23 2019 UTC (5 years, 1 month ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2019Q1-base,
pkgsrc-2019Q1
Changes since 1.31: +6 -6
lines
Diff to previous 1.31 (colored) to selected 1.14 (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.31 / (download) - annotate - [select for diffs], Thu Aug 2 12:57:03 2018 UTC (5 years, 8 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2018Q4-base,
pkgsrc-2018Q4,
pkgsrc-2018Q3-base,
pkgsrc-2018Q3
Changes since 1.30: +5 -5
lines
Diff to previous 1.30 (colored) to selected 1.14 (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.30 / (download) - annotate - [select for diffs], Mon Apr 9 11:29:23 2018 UTC (6 years ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2018Q2-base,
pkgsrc-2018Q2
Changes since 1.29: +5 -5
lines
Diff to previous 1.29 (colored) to selected 1.14 (colored)
Updated lang/coq to version 8.7.2. This fixes a critical bug in the VM handling of universes, and adds various other minor fixes and improvements.
Revision 1.29 / (download) - annotate - [select for diffs], Wed Jan 10 16:26:53 2018 UTC (6 years, 3 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2018Q1-base,
pkgsrc-2018Q1
Changes since 1.28: +5 -7
lines
Diff to previous 1.28 (colored) to selected 1.14 (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.28 / (download) - annotate - [select for diffs], Fri Nov 3 11:20:28 2017 UTC (6 years, 5 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2017Q4-base,
pkgsrc-2017Q4
Changes since 1.27: +7 -6
lines
Diff to previous 1.27 (colored) to selected 1.14 (colored)
Updated lang/coq to version 8.7.0. Includes many improvements and bugfixes (none that seem to be breaking backwards compatibility though), see the CHANGELOG. For packaging: - camlp4 support removed, package now uses camlp5 exclusively - fix for PR pkg/52651
Revision 1.27 / (download) - annotate - [select for diffs], Fri Sep 8 17:19:01 2017 UTC (6 years, 7 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2017Q3-base,
pkgsrc-2017Q3
Changes since 1.26: +5 -5
lines
Diff to previous 1.26 (colored) to selected 1.14 (colored)
Updated package to latest version, 8.6.1. Changes include: - Fix #5380: Default colors for CoqIDE are actually applied. - Fix plugin warnings - Document named evars (including Show ident) - Fix Bug #5574, document function scope - Adding a test case as requested in bug 5205. - Fix Bug #5568, no dup notation warnings on repeated module imports - Fix documentation of Typeclasses eauto := - Refactor documentation of records. - Protecting from warnings while compiling 8.6 - Fixing an inconsistency between configure and configure.ml - Add test-suite checks for coqchk with constraints - Fix bug #5019 (looping zify on dependent types) - Fix bug 5550: "typeclasses eauto with" does not work with section variables. - Bug 5546, qualify datatype constructors when needed in Show Match - Bug #5535, test for Show with -emacs - Fix bug #5486, don't reverse ids in tuples - Fixing #5522 (anomaly with free vars of pat) - Fix bug #5526, don't check for nonlinearity in notation if printing only - Fix bug #5255 - Fix bug #3659: -time should understand multibyte encodings. - FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print Assumptions". - Fix outdated description in RefMan. - Repairing `Set Rewriting Schemes` - Fixing #5487 (v8.5 regression on ltac-matching expressions with evars). - Fix description of command-line arguments for Add (Rec) LoadPath - Fix bug #5377: @? patterns broken. - add XML protocol doc - Fix anomaly when doing [all:Check _.] during a proof. - Correction of bug #4306 - Fix #5435: [Eval native_compute in] raises anomaly. - Instances should obey universe binders even when defined by tactics. - Intern names bound in match patterns - funind: Ignore missing info for current function - Do not typecheck twice the type of opaque constants. - show unused intro pattern warning - [future] Be eager when "chaining" already resolved future values. - Opaque side effects - Fix #5132: coq_makefile generates incorrect install goal - Run non-tactic comands without resilient_command - Univs: fix bug #5365, generation of u+k <= v constraints - make `emit' tail recursive - Don't require printing-only notation to be productive - Fix the way setoid_rewrite handles bindings. - Fix for bug 5244 - set printing width ignored when given enough space - Fix bug 4969, autoapply was not tagging shelved subgoals correctly
Revision 1.26 / (download) - annotate - [select for diffs], Fri Dec 30 13:23:06 2016 UTC (7 years, 3 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2017Q2-base,
pkgsrc-2017Q2,
pkgsrc-2017Q1-base,
pkgsrc-2017Q1
Changes since 1.25: +7 -8
lines
Diff to previous 1.25 (colored) to selected 1.14 (colored)
Updated coq to latest version, 8.6. Changes include:
Changes from V8.6beta1 to V8.6
==============================
Kernel
- Fixed critical bug #5248 in VM long multiplication on 32-bit
architectures. Was there only since 8.6beta1, so no stable release impacted.
Other bug fixes in universes, type class shelving,...
Changes from V8.5 to V8.6beta1
==============================
Kernel
- A new, faster state-of-the-art universe constraint checker.
Specification language
- Giving implicit arguments explicitly to a constant with multiple
choices of implicit arguments does not break any more insertion of
further maximal implicit arguments.
- Ability to put any pattern in binders, prefixed by quote, e.g.
"fun '(a,b) => ...", "λ '(a,(b,c)), ...", "Definition foo '(x,y) := ...".
It expands into a "let 'pattern := ..."
Tactics
- Flag "Bracketing Last Introduction Pattern" is now on by default.
- Flag "Regular Subst Tactic" is now on by default: it respects the
initial order of hypothesis, it contracts cycles, it unfolds no
local definitions (common source of incompatibilities, fixable by
"Unset Regular Subst Tactic").
- New flag "Refolding Reduction", now disabled by default, which turns
on refolding of constants/fixpoints (as in cbn) during the reductions
done during type inference and tactic retyping. Can be extremely
expensive. When set off, this recovers the 8.4 behaviour of unification
and type inference. Potential source of incompatibility with 8.5 developments
(the option is set on in Compat/Coq85.v).
- New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
tactical w.r.t. variables appearing in the body of the proof.
On by default and deprecated. Minor source of incompatibility
for code relying on the precise arguments of abstracted proofs.
- Serious bugs are fixed in tactic "double induction" (source of
incompatibilities as soon as the inductive types have dependencies in
the type of their constructors; "double induction" remains however
deprecated).
- In introduction patterns of the form (pat1,...,patn), n should match
the exact number of hypotheses introduced (except for local definitions
for which pattern can be omitted, as in regular pattern-matching).
- Tactic scopes in Ltac like constr: and ltac: now require parentheses around
their argument.
- Every generic argument type declares a tactic scope of the form "name:(...)"
where name is the name of the argument. This generalizes the constr: and ltac:
instances.
- When in strict mode (i.e. in a Ltac definition), if the "intro" tactic is
given a free identifier, it is not bound in subsequent tactics anymore.
In order to introduce a binding, use e.g. the "fresh" primitive instead
(potential source of incompatibilities).
- New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac.
- New goal selectors. Sets of goals can be selected by listing integers
ranges. Example: "1,4-7,24: tac" focuses "tac" on goals 1,4,5,6,7,24.
- For uniformity with "destruct"/"induction" and for a more natural
behavior, "injection" can now work in place by activating option
"Structural Injection". In this case, hypotheses are also put in the
context in the natural left-to-right order and the hypothesis on
which injection applies is cleared.
- Tactic "contradiction" (hence "easy") now also solve goals with
hypotheses of the form "~True" or "t<>t" (possible source of
incompatibilities because of more successes in automation, but
generally a more intuitive strategy).
- Option "Injection On Proofs" was renamed "Keep Proof Equalities". When
enabled, injection and inversion do not drop equalities between objects
in Prop. Still disabled by default.
- New tactics "notypeclasses refine" and "simple notypeclasses refine" that
disallow typeclass resolution when typechecking their argument, for use
in typeclass hints.
- Integration of LtacProf, a profiler for Ltac.
- Reduction tactics now accept more fine-grained flags: iota is now a shorthand
for the new flags match, fix and cofix.
- The ssreflect subterm selection algorithm is now accessible to tactic writers
through the ssrmatching plugin.
- When used as an argument of an ltac function, "auto" without "with"
nor "using" clause now correctly uses only the core hint database by
default.
Hints
- Revised the syntax of [Hint Cut] to follow standard notation for regexps.
- Hint Mode now accepts "!" which means that the mode matches only if the
argument's head is not an evar (it goes under applications, casts, and
scrutinees of matches and projections).
- Hints can now take an optional user-given pattern, used only by
[typeclasses eauto] with the [Filtered Unification] option on.
Typeclasses
- Many new options and new engine based on the proof monad. The
[typeclasses eauto] tactic is now a multi-goal, multi-success tactic.
See reference manual for more information. It is planned to
replace auto and eauto in the following version. The 8.5 resolution
engine is still available to help solve compatibility issues.
Program
- The "Shrink Obligations" flag now applies to all obligations, not only
those solved by the automatic tactic.
- "Shrink Obligations" is on by default and deprecated. Minor source of
incompatibility for code relying on the precise arguments of
obligations.
Notations
- "Bind Scope" can once again bind "Funclass" and "Sortclass".
General infrastructure
- New configurable warning system which can be controlled with the vernacular
command "Set Warnings", or, under coqc/coqtop, with the flag "-w". In
particular, the default is now that warnings are printed by coqc.
- In asynchronous mode, Coq is now capable of recovering from errors and
continue processing the document.
Tools
- coqc accepts a -o option to specify the output file name
- coqtop accepts --print-version to print Coq and OCaml versions in
easy to parse format
- Setting [Printing Dependent Evars Line] can be unset to disable the
computation associated with printing the "dependent evars: " line in
-emacs mode
- Removed the -verbose-compat-notations flag and the corresponding Set
Verbose Compat vernacular, since these warnings can now be silenced or
turned into errors using "-w".
XML protocol
- message format has changed, see dev/doc/changes.txt for more details.
Many bug fixes, minor changes and documentation improvements are not mentioned
here.
Changes from V8.5pl2 to V8.5pl3
===============================
Critical bugfix
- #4876: Guard checker incompleteness when using primitive projections
Other bugfixes
- #4780: Induction with universe polymorphism on was creating ill-typed terms.
- #4673: regression in setoid_rewrite, unfolding let-ins for type unification.
- #4754: Regression in setoid_rewrite, allow postponed unification problems to remain.
- #4769: Anomaly with universe polymorphic schemes defined inside sections.
- #3886: Program: duplicate obligations of mutual fixpoints.
- #4994: Documentation typo.
- #5008: Use the "md5" command on OpenBSD.
- #5007: Do not assume the "TERM" environment variable is always set.
- #4606: Output a break before a list only if there was an empty line.
- #5001: metas not cleaned properly in clenv_refine_in.
- #2336: incorrect glob data for module symbols (bug #2336).
- #4832: Remove extraneous dot in error message.
- Anomaly in printing a unification error message.
- #4947: Options which take string arguments are not backwards compatible.
- #4156: micromega cache files are now hidden files.
- #4871: interrupting par:abstract kills coqtop.
- #5043: [Admitted] lemmas pick up section variables.
- Fix name of internal refine ("simple refine").
- #5062: probably a typo in Strict Proofs mode.
- #5065: Anomaly: Not a proof by induction.
- Restore native compiler optimizations, they were disabled since 8.5!
- #5077: failure on typing a fixpoint with evars in its type.
- Fix recursive notation bug.
- #5095: non relevant too strict test in let-in abstraction.
- Ensuring that the evar name is preserved by "rename".
- #4887: confusion between using and with in documentation of firstorder.
- Bug in subst with let-ins.
- #4762: eauto weaker than auto.
- Remove if_then_else (was buggy). Use tryif instead.
- #4970: confusion between special "{" and non special "{{" in notations.
- #4529: primitive projections unfolding.
- #4416: Incorrect "Error: Incorrect number of goals".
- #4863: abstract in typeclass hint fails.
- #5123: unshelve can impact typeclass resolution
- Fix a collision about the meta-variable ".." in recursive notations.
- Fix printing of info_auto.
- #3209: Not_found due to an occur-check cycle.
- #5097: status of evars refined by "clear" in ltac: closed wrt evars.
- #5150: Missing dependency of the test-suite subsystems in prerequisite.
- Fix a bug in error printing of unif constraints
- #3941: Do not stop propagation of signals when Coq is busy.
- #4822: Incorrect assertion in cbn.
- #3479 parsing of "{" and "}" when a keyword starts with "{" or "}".
- #5127: Memory corruption with the VM.
- #5102: bullets parsing broken by calls to parse_entry.
Various documentation improvements
Changes from V8.5pl1 to V8.5pl2
===============================
Critical bugfix
- Checksums of .vo files dependencies were not correctly checked.
- Unicode-to-ASCII translation was not injective, leading in a soundness bug in
the native compiler.
Other bugfixes
- #4097: more efficient occur-check in presence of primitive projections
- #4398: type_scope used consistently in "match goal".
- #4450: eauto does not work with polymorphic lemmas
- #4677: fix alpha-conversion in notations needing eta-expansion.
- Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode.
- #4644: a regression in unification.
- #4725: Function (Error: Conversion test raised an anomaly) and Program
(Error: Cannot infer this placeholder of type)
- #4747: Problem building Coq 8.5pl1 with OCaml 4.03.0: Fatal warnings
- #4752: CoqIDE crash on files not ended by ".v".
- #4777: printing inefficiency with implicit arguments
- #4818: "Admitted" fails due to undefined universe anomaly after calling
"destruct"
- #4823: remote counter: avoid thread race on sockets
- #4841: -verbose flag changed semantics in 8.5, is much harder to use
- #4851: [nsatz] cannot handle duplicated hypotheses
- #4858: Anomaly: Uncaught exception Failure("hd"). Please report. in variant
of nsatz
- #4880: [nsatz_compute] generates invalid certificates if given redundant
hypotheses
- #4881: synchronizing "Declare Implicit Tactic" with backtrack.
- #4882: anomaly with Declare Implicit Tactic on hole of type with evars
- Fix use of "Declare Implicit Tactic" in refine.
triggered by CoqIDE
- #4069, #4718: congruence fails when universes are involved.
Universes
- Disallow silently dropping universe instances applied to variables
(forward compatible)
- Allow explicit universe instances on notations, when they can apply
to the head reference of their expansion.
Build infrastructure
- New update on how to find camlp5 binary and library at configure time.
Revision 1.25 / (download) - annotate - [select for diffs], Sat Jul 2 10:17:18 2016 UTC (7 years, 9 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2016Q4-base,
pkgsrc-2016Q4,
pkgsrc-2016Q3-base,
pkgsrc-2016Q3
Changes since 1.24: +6 -6
lines
Diff to previous 1.24 (colored) to selected 1.14 (colored)
Updated package to latest version, 8.5pl1. Also fixed a packaging bug
that had buildlink paths show up in the Coq_config module, and added a
patch from upstream to allow compilation with 4.03.
Changes:
Critical bugfix
- The subterm relation for the guard condition was incorrectly defined on
primitive projections (#4588)
Plugin development tools
- add a .merlin target to the makefile
Various performance improvements (time, space used by .vo files)
Other bugfixes
- Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v
- Added compatibility coercions from Specif.v which were present in Coq 8.4.
- Fixing a source of inefficiency and an artificial dependency in the printer in the congruence tactic.
- Allow to unset the refinement mode of Instance in ML
- Fixing an incorrect use of prod_appvect on a term which was not a product in setoid_rewrite.
- Add -compat 8.4 econstructor tactics, and tests
- Add compatibility Nonrecursive Elimination Schemes
- Fixing the "No applicable tactic" non informative error message regression on apply.
- Univs: fix get_current_context (bug #4603, part I)
- Fix a bug in Program coercion code
- Fix handling of arity of definitional classes.
- #4630: Some tactics are 20x slower in 8.5 than 8.4.
- #4627: records with no declared arity can be template polymorphic.
- #4623: set tactic too weak with universes (regression)
- Fix incorrect behavior of CS resolution
- #4591: Uncaught exception in directory browsing.
- CoqIDE is more resilient to initialization errors.
- #4614: "Fully check the document" is uninterruptable.
- Try eta-expansion of records only on non-recursive ones
- Fix bug when a sort is ascribed to a Record
- Primitive projections: protect kernel from erroneous definitions.
- Fixed bug #4533 with previous Keyed Unification commit
- Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)
- Fix strategy of Keyed Unification
- #4608: Anomaly "output_value: abstract value (outside heap)".
- #4607: do not read native code files if native compiler was disabled.
- #4105: poor escaping in the protocol between CoqIDE and coqtop.
- #4596: [rewrite] broke in the past few weeks.
- #4533 (partial): respect declared global transparency of projections in unification.ml
- #4544: Backtrack on using full betaiota reduction during keyed unification.
- #4540: CoqIDE bottom progress bar does not update.
- Fix regression from 8.4 in reflexivity
- #4580: [Set Refine Instance Mode] also used for Program Instance.
- #4582: cannot override notation [ x ]. MAY CREATE INCOMPATIBILITIES, see #4683.
- STM: Print/Extraction have to be skipped if -quick
- #4542: CoqIDE: STOP button also stops workers
- STM: classify some variants of Instance as regular `Fork nodes.
- #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").
- Do not give a name to anonymous evars anymore. See bug #4547.
- STM: always stock in vio files the first node (state) of a proof
- STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530
- Don't fail fatally if PATH is not set.
- #4537: Coq 8.5 is slower in typeclass resolution.
- #4522: Incorrect "Warning..." on windows.
- #4373: coqdep does not know about .vio files.
- #3826: "Incompatible module types" is uninformative.
- #4495: Failed assertion in metasyntax.ml.
- #4511: evar tactic can create non-typed evars.
- #4503: mixing universe polymorphic and monomorphic variables and definitions in sections is unsupported.
- #4519: oops, global shadowed local universe level bindings.
- #4506: Anomaly: File "pretyping/indrec.ml", line 169, characters 14-20: Assertion failed.
- #4548: Coqide crashes when going back one command
Revision 1.24 / (download) - annotate - [select for diffs], Sat Feb 6 16:08:36 2016 UTC (8 years, 2 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2016Q2-base,
pkgsrc-2016Q2,
pkgsrc-2016Q1-base,
pkgsrc-2016Q1
Changes since 1.23: +8 -6
lines
Diff to previous 1.23 (colored) to selected 1.14 (colored)
Updated package to latest version, 8.5. The changeset is over 500 lines long, so I will not include it here, but details can be found in the CHANGES file in the source. (the previous version was V8.4.)
Revision 1.23 / (download) - annotate - [select for diffs], Tue Dec 29 06:22:54 2015 UTC (8 years, 3 months ago) by dholland
Branch: MAIN
Changes since 1.22: +2 -2
lines
Diff to previous 1.22 (colored) to selected 1.14 (colored)
pkglint
Revision 1.22 / (download) - annotate - [select for diffs], Tue Nov 3 22:50:33 2015 UTC (8 years, 5 months ago) by agc
Branch: MAIN
CVS Tags: pkgsrc-2015Q4-base,
pkgsrc-2015Q4
Changes since 1.21: +2 -1
lines
Diff to previous 1.21 (colored) to selected 1.14 (colored)
Add SHA512 digests for distfiles for lang category Problems found with existing digests: Package nhc98 distfile nhc98src-1.22.tar.gz a8adc8f22371998ee0657bc0e01058a57d876abc [recorded] 81975fcb5f1dda5efeaabc30ce8c6dceae55e591 [calculated] Problems found locating distfiles: Package gcc-aux: missing distfile ada-bootstrap.i386.dragonfly.36A.tar.bz2 Package gcc-aux: missing distfile ada-bootstrap.i386.freebsd.84.tar.bz2 Package gcc-aux: missing distfile ada-bootstrap.x86_64.dragonfly.36A.tar.bz2 Package gcc-aux: missing distfile ada-bootstrap.x86_64.freebsd.84.tar.bz2 Package gcc-aux: missing distfile ada-bootstrap.x86_64.solaris.511.tar.bz2 Package gcc5-aux: missing distfile ada-bootstrap.i386.dragonfly.36A.tar.bz2 Package gcc5-aux: missing distfile ada-bootstrap.i386.freebsd.84.tar.bz2 Package gcc5-aux: missing distfile ada-bootstrap.x86_64.dragonfly.36A.tar.bz2 Package gcc5-aux: missing distfile ada-bootstrap.x86_64.freebsd.84.tar.bz2 Package gcc5-aux: missing distfile ada-bootstrap.x86_64.solaris.511.tar.bz2 Package ghc7: missing distfile ghc-7.6.3-boot-i386-unknown-freebsd.tar.xz Package icc11: missing distfile l_cproc_p_11.1.080.tgz Package jini: missing distfile jini-1_2_1_001-src.zip Package oo2c: missing distfile oo2c_32-2.0.11.tar.bz2 Package openjdk7: missing distfile openjdk7/bootstrap-jdk-1.7.76-freebsd-10-amd64-20150301.tar.xz Package openjdk7: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-5-i386-20150301.tar.xz Package openjdk7: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-6-i386-20150301.tar.xz Package openjdk7: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-7-earmv6hf-20150306.tar.xz Package openjdk7: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-7-sparc64-20150301.tar.xz Package openjdk7: missing distfile openjdk7/bootstrap-jdk7u60-bin-dragonfly-3.8-amd64-20140719.tar.bz2 Package openjdk8: missing distfile openjdk7/bootstrap-jdk-1.7.76-freebsd-10-amd64-20150301.tar.xz Package openjdk8: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-5-i386-20150301.tar.xz Package openjdk8: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-6-i386-20150301.tar.xz Package openjdk8: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-7-earmv6hf-20150306.tar.xz Package openjdk8: missing distfile openjdk7/bootstrap-jdk-1.7.76-netbsd-7-sparc64-20150301.tar.xz Package openjdk8: missing distfile openjdk7/bootstrap-jdk7u60-bin-dragonfly-3.8-amd64-20140719.tar.bz2 Package oracle-jdk8: missing distfile jdk-8u60-linux-i586.tar.gz Package oracle-jdk8: missing distfile jdk-8u60-solaris-x64.tar.gz Package oracle-jre8: missing distfile jre-8u60-linux-i586.tar.gz Package oracle-jre8: missing distfile jre-8u60-solaris-x64.tar.gz Package sun-jdk6: missing distfile jdk-6u45-linux-i586.bin Package sun-jdk6: missing distfile jdk-6u45-solaris-i586.sh Package sun-jdk7: missing distfile jdk-7u72-linux-i586.tar.gz Package sun-jdk7: missing distfile jdk-7u72-solaris-i586.tar.gz Package sun-jre6: missing distfile jce_policy-6.zip Package sun-jre6: missing distfile jre-6u45-linux-x64.bin Package sun-jre6: missing distfile jre-6u45-solaris-x64.sh Package sun-jre7: missing distfile jre-7u72-linux-i586.tar.gz Package sun-jre7: missing distfile jre-7u72-solaris-i586.tar.gz Otherwise, existing SHA1 digests verified and found to be the same on the machine holding the existing distfiles (morden). All existing SHA1 digests retained for now as an audit trail.
Revision 1.21 / (download) - annotate - [select for diffs], Sat Apr 25 13:41:18 2015 UTC (8 years, 11 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2015Q3-base,
pkgsrc-2015Q3,
pkgsrc-2015Q2-base,
pkgsrc-2015Q2
Changes since 1.20: +4 -5
lines
Diff to previous 1.20 (colored) to selected 1.14 (colored)
Updated coq to version 8.4pl6. Changes from previous version include (apart from bugfixes): - Coq compilation made possible with forthcoming ocaml 4.03. - command for locating exists notation in refman changed. - Various improvements of the Reference Manual (especially its html version) - implicit arguments of local definitions fixed (possible source of incompatibilities). - New command "Print Debug GC". - Function cannot define graph. - Optimizing compilation of pattern matching. - Better inference of impossible cases in pattern-matching. - Evar leak in pattern-matching compilation - ill-typed replacement in "change ... with ...". - unbound evars in "change ... with ...". - wrong return clause of a match pattern in Ltac. - cleared local hints for autounfold. - cleared local hints for autounfold. - lost evars in "change ... with ...". - supporting let-ins in constructors for vm_compute - unfortunate typo in compare_height. - unfortunate typos in absorption lemmas over bool. - Full support of utf8 Greek letters (block U0370) in coqdoc
Revision 1.20 / (download) - annotate - [select for diffs], Thu Oct 9 22:19:01 2014 UTC (9 years, 6 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2015Q1-base,
pkgsrc-2015Q1,
pkgsrc-2014Q4-base,
pkgsrc-2014Q4
Changes since 1.19: +2 -1
lines
Diff to previous 1.19 (colored) to selected 1.14 (colored)
Revbump because of ocaml 4.02, added compilation patch (already in repository upstream) and updated package to use ocaml.mk framework.
Revision 1.19 / (download) - annotate - [select for diffs], Tue May 13 14:52:28 2014 UTC (9 years, 11 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2014Q3-base,
pkgsrc-2014Q3,
pkgsrc-2014Q2-base,
pkgsrc-2014Q2
Changes since 1.18: +4 -5
lines
Diff to previous 1.18 (colored) to selected 1.14 (colored)
Update of package to version 8.4pl4. Changes include:
Changes from V8.4pl3 to V8.4pl4
===============================
WARNING:
The current logic of Coq is now known to be inconsistent with
Axiom prop_extensionality : forall A B:Prop, (A <-> B) -> A = B.
For more details, see:
https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm2.v;hb=HEAD
or
https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=coq/coq.git;a=blob_plain;f=test-suite/failure/subterm3.v;hb=HEAD
Kernel
- Unsound check of elimination sort.
- Fix guard condition for nested cofixpoints.
- Univ constraints of module subtyping were not propagated.
Tactics
- A new option "Set Stable Omega" ensures that repeated identical calls
to omega will produce identical proof terms. This option is off by default
for maximal compatibility, but should be pretty safe to activate.
- The interpretation of the open_constr tactic argument was erroneously
firing type classes resolution in some corner cases. This has been
fixed. The tactic argument type open_constr_wTC is provided for retro
compatibility purposes.
- Fixing bug (fixing precedence of ltac variables over variables in
env) introduces rare and justified tactic failure.
Bug fixes
- micromega: solved an ambiguous symbol resolution.
- Coq always uses / as separator between directories on all platforms.
- remove trailing '\r' from file names returned by coqtop.
- bug correction in proving inversion principles for Function.
- ocamlbuild: minor fixes related to camlp4 and cross-compilation.
Changes from V8.4pl2 to V8.4pl3
===============================
Ide_slave XML interface
- 20120712, 20130419 : Invalidated protocol versions
- From 20130419 extra datastructure : union
(Inl "" = <union val="in_l"><string></string></union>,
Inr _ = <union val="in_r">...)
- 20130419~1 : new toplevel entry : message, not send by coptop v8.4 and not
handle by coqide v8.4. A message has a level and a content (of string).
Message levels are Debug of string, Info, Notice, Warning and Error.
- 20130425 :
* new toplevel entry : feedback, once again not send by coqtop v8.4 and not
handle by coqide v8.4. A feedback gives the id of the sentence it provides info
about and a content. Feedback contents are Processed, AddedAxiom and
GlobRef of Util.loc * string * string * string * string
* <call val="interp"> must provide an attribute id of type int. It is OK in
coqtop v8.4 to alwais send <call val="interp" id="0">
Bug fixes
- Fixing a significant efficiency leak in the code of the field tactic.
- Fix caching of local hint database in typeclasses eauto which could
miss some hypotheses.
- Fix automatic solving of obligation in program, which was not trying
to solve obligations that had no undefined dependencies left.
Revision 1.18 / (download) - annotate - [select for diffs], Sun Oct 27 22:22:31 2013 UTC (10 years, 5 months ago) by joerg
Branch: MAIN
CVS Tags: pkgsrc-2014Q1-base,
pkgsrc-2014Q1,
pkgsrc-2013Q4-base,
pkgsrc-2013Q4
Changes since 1.17: +2 -2
lines
Diff to previous 1.17 (colored) to selected 1.14 (colored)
Don't use -fno-defer-pop.
Revision 1.17 / (download) - annotate - [select for diffs], Sat Oct 26 19:44:33 2013 UTC (10 years, 5 months ago) by asau
Branch: MAIN
Changes since 1.16: +2 -1
lines
Diff to previous 1.16 (colored) to selected 1.14 (colored)
Accept GNU Make 4 and later.
Revision 1.16 / (download) - annotate - [select for diffs], Sat Apr 20 08:21:49 2013 UTC (11 years ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2013Q3-base,
pkgsrc-2013Q3,
pkgsrc-2013Q2-base,
pkgsrc-2013Q2
Changes since 1.15: +4 -4
lines
Diff to previous 1.15 (colored) to selected 1.14 (colored)
Updated package to the latest version, 8.4pl2. Changes include: Bug fixes - Solved bugs : #2466 #2629 #2668 #2750 #2839 #2869 #2954 #2955 #2959 #2962 #2966 #2967 #2969 #2970 #2975 #2976 #2977 #2978 #2981 #2983 #2995 #3000 #3004 #3008 - Partially fixed bugs : #2830 #2949 - Coqtop should now react more reliably when receiving interrupt signals: all the "try...with" constructs have been protected against undue handling of the Sys.Break exception. Coqide - The Windows-specific code handling the interrupt button of Coqide had to be reworked (cf. bug #2869). Now, in Win32 this button does not target a specific coqtop client, but instead sends a Ctrl-C to any process sharing its console with Coqide. To avoid awkward effects, it is recommended to launch Coqide via its icon, its menu, or in a dedicated console window. Extraction - The option Extraction AccessOpaque is now set by default, restoring compatibility of older versions of Coq (cf bug #2952).
Revision 1.15 / (download) - annotate - [select for diffs], Tue Jan 22 15:32:03 2013 UTC (11 years, 2 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2013Q1-base,
pkgsrc-2013Q1
Changes since 1.14: +4 -6
lines
Diff to previous 1.14 (colored)
Updated lang/coq to the newest version, 8.4pl1. Changes include: Bug fixes - Solved bugs : #2851 #2863 #2865 #2893 #2895 #2892 #2905 #2906 #2907 #2917 #2921 #2930 #2941 #2878 - Partially fixed bug : #2904 - Various fixes concerning coq_makefile Optimizations - "Union by rank" optimization for universes contributed by J.H. Jourdan and G. Sherrer (see union-find-and-coq-universes on gagallium blog). Libraries - Internal organisation of some modular libraries have slightly changed due to bug #2904 (GenericMinMax, OrdersTac) - No more constant "int" in ZArith/Int.v to avoid name clash with OCaml (cf bug #2878). Coqide - Improved shutdown of coqtop processes spawned by coqide (in particular added a missing close_on_exec primitive before forking). - On windows, launching coqide with the -debug option now produces a log file in the user's temporary directory. The location of this log file is displayed in the "About" message.
Revision 1.14 / (download) - annotate - [selected], Mon Oct 29 11:33:17 2012 UTC (11 years, 5 months ago) by jaapb
Branch: MAIN
CVS Tags: pkgsrc-2012Q4-base,
pkgsrc-2012Q4
Changes since 1.13: +7 -5
lines
Diff to previous 1.13 (colored)
Taken over maintainership (as discussed with previous maintainer,
richards@cs.princeton.edu). Updated package to use PLIST_VARS and CONF_FILES.
Updated coq to version 8.4. Changes include:
Logic
- Standard eta-conversion now supported (dependent product only).
- Guard condition improvement: subterm property is propagated through beta-redex
blocked by pattern-matching, as in "(match v with C .. => fun x => u end) x";
this allows for instance to use "rewrite ... in ..." without breaking
the guard condition.
Vernacular commands
- The "Reset" command is now supported again in files given to coqc or Load.
- "Show Script" now indents again the displayed scripts. It can also work
correctly across Load'ed files if the option "Unset Atomic Load" is used.
- "Open Scope" can now be given the delimiter (e.g. Z) instead of the full
scope name (e.g. Z_scope).
- Commands "Back" and "BackTo" are now handling the proof states. They may
perform some extra steps of backtrack to avoid states where the proof
state is unavailable (typically a closed proof).
- The commands "Suspend" and "Resume" have been removed.
- A basic Show Script has been reintroduced (no indentation).
- New command "Set Parsing Explicit" for deactivating parsing (and printing)
of implicit arguments (useful for teaching).
- New command "Grab Existential Variables" to transform the unresolved evars
at the end of a proof into goals.
- It is now mandatory to have a space (or tabulation or newline or end-of-file)
after a "." ending a sentence.
- In SearchAbout, the [ ] delimiters are now optional.
- New command "Add/Remove Search Blacklist <substring> ...":
a Search or SearchAbout or similar query will never mention lemmas
whose qualified names contain any of the declared substrings.
The default blacklisted substrings are "_admitted" "_subproof" "Private_".
- When the output file of "Print Universes" ends in ".dot" or ".gv",
the universe graph is printed in the DOT language, and can be
processed by Graphviz tools.
- New command "Print Sorted Universes".
- The undocumented and obsolete option "Set/Unset Boxed Definitions" has
been removed, as well as syntaxes like "Boxed Fixpoint foo".
- A new option "Set Default Timeout n / Unset Default Timeout".
- Qed now uses information from the reduction tactics used in proof script
to avoid conversion at Qed time to go into a very long computation.
- New command "Show Goal ident" to display the statement of a goal, even
a closed one (available from Proof General).
- Command "Proof" accept a new modifier "using" to force generalization
over a given list of section variables at section ending.
- New command "Arguments" generalizing "Implicit Arguments" and
"Arguments Scope" and that also allows to rename the parameters of a
definition and to tune the behavior of the tactic "simpl".
Specification language and Notations
- Most compatibility notations of the standard library are now tagged as
(compat xyz), where xyz is a former Coq version, for instance "8.3".
These notations behave as (only parsing) notations, except that they may
triggers warnings (or errors) when used while Coq is not in a corresponding
-compat mode.
- To activate these compatibility warnings, use "Set Verbose Compat Notations"
or the command-line flag -verbose-compat-notations.
- For a strict mode without these compatibility notations, use
"Unset Compat Notations" or the command-line flag -no-compat-notations.
- Maximal implicit arguments can now be set locally by { }. The registration
traverses fixpoints and lambdas. Because there is conversion in types,
maximal implicit arguments are not taken into account in partial
applications (use eta expanded form with explicit { } instead).
- Added support for recursive notations with binders (allows for instance
to write "exists x y z, P").
- Structure/Record printing can be disable by "Unset Printing Records".
In addition, it can be controlled on type by type basis using
"Add Printing Record" or "Add Printing Constructor".
- Pattern-matching compilation algorithm: in "match x, y with ... end",
possible dependencies of x (or of the indices of its type) in the type
of y are now taken into account.
Tactics
- An annotation "eqn:H" or "eqn:?" can be added to a "destruct"
or "induction" to make it generate equations in the spirit of "case_eq".
The former syntax "_eqn" is discontinued.
- The name of the hypothesis introduced by tactic "remember" can be
set via the new syntax "remember t as x eqn:H" (wish #2489).
- Still no general "info" tactical, but new specific tactics info_auto,
info_eauto, info_trivial which provides information on the proofs found
by auto/eauto/trivial. Display of these details could also be activated by
"Set Info Auto"/"Set Info Eauto"/"Set Info Trivial".
- Details on everything tried by auto/eauto/trivial during a proof search
could be obtained by "debug auto", "debug eauto", "debug trivial" or by a
global "Set Debug Auto"/"Set Debug Eauto"/"Set Debug Trivial".
- New command "r string" in Ltac debugger that interprets "idtac
string" in Ltac code as a breakpoint and jumps to its next use.
- Tactics from the Dp plugin (simplify, ergo, yices, cvc3, z3, cvcl,
harvey, zenon, gwhy) have been removed, since Why2 has not been
maintained for the last few years. The Why3 plugin should be a suitable
replacement in most cases.
- New proof engine.
- Scripts can now be structured thanks to bullets - * + and to subgoal
delimitation via { }. Note: for use with Proof General, a cvs version of
Proof General no older than mid-July 2011 is currently required.
- Support for tactical "info" is suspended.
- Support for command "Show Script" is suspended.
- New tactics constr_eq, is_evar and has_evar for use in Ltac.
- Removed the two-argument variant of "decide equality".
- New experimental tactical "timeout <n> <tac>". Since <n> is a time
in second for the moment, this feature should rather be avoided
in scripts meant to be machine-independent.
- Fix in "destruct": removal of unexpected local definitions in context might
result in some rare incompatibilities (solvable by adapting name hypotheses).
- Introduction pattern "_" made more robust.
- Tactic (and Eval command) vm_compute can now be interrupted via Ctrl-C.
- Unification in "apply" supports unification of patterns of the form
?f x y = g(x,y) (compatibility ensured by using
"Unset Tactic Pattern Unification"). It also supports (full) betaiota.
- Tactic autorewrite does no longer instantiate pre-existing
existential variables (theoretical source of possible incompatibilities).
- Tactic "dependent rewrite" now supports equality in "sig".
- Tactic omega now understands Zpred (wish #1912) and can prove any goal
from a context containing an arithmetical contradiction (wish #2236).
- Using "auto with nocore" disables the use of the "core" database (wish #2188).
This pseudo-database "nocore" can also be used with trivial and eauto.
- Tactics "set", "destruct" and "induction" accepts incomplete terms and
use the goal to complete the pattern assuming it is non ambiguous.
- When used on arguments with a dependent type, tactics such as
"destruct", "induction", "case", "elim", etc. now try to abstract
automatically the dependencies over the arguments of the types
(based on initial ideas from Chung-Kil Hur, extension to nested
dependencies suggested by Dan Grayson)
- Tactic "injection" now failing on an equality showing no constructors while
it was formerly generalizing again the goal over the given equality.
- In Ltac, the "context [...]" syntax has now a variant "appcontext [...]"
allowing to match partial applications in larger applications.
- When applying destruct or inversion on a fixpoint hiding an inductive
type, recursive calls to the fixpoint now remain folded by default (rare
source of incompatibility generally solvable by adding a call to simpl).
- In an ltac pattern containing a "match", a final "| _ => _" branch could be
used now instead of enumerating all remaining constructors. Moreover, the
pattern "match _ with _ => _ end" now allows to match any "match". A "in"
annotation can also be added to restrict to a precise inductive type.
- The behavior of "simpl" can be tuned using the "Arguments" vernacular.
In particular constants can be marked so that they are always/never unfolded
by "simpl", or unfolded only when a set of arguments evaluates to a
constructor. Last one can mark a constant so that it is unfolded only if the
simplified term does not expose a match in head position.
Libraries
- Reals: changed definition of PI, no more axiom about sin(PI/2).
- SetoidPermutation: a notion of permutation for lists modulo a setoid equality.
- BigN: fixed the ocaml code doing the parsing/printing of big numbers.
- MSetRBT: a new implementation of MSets via Red-Black trees (initial
contribution by Andrew Appel).
- MSetAVL: for maximal sharing with the new MSetRBT, the argument order
of Node has changed (this should be transparent to regular MSets users).
- Extension of the abstract part of Numbers, which now provide axiomatizations
and results about many more integer functions, such as pow, gcd, lcm, sqrt,
log2 and bitwise functions. These functions are implemented for nat, N, BigN,
Z, BigZ. See in particular file NPeano for new functions about nat.
- The definition of types positive, N, Z is now in file BinNums.v
- Major reorganization of ZArith. The initial file ZArith/BinInt.v now contains
an internal module Z implementing the Numbers interface for integers.
This module Z regroups:
* all functions over type Z : Z.add, Z.mul, ...
* the minimal proofs of specifications for these functions : Z.add_0_l, ...
* an instantation of all derived properties proved generically in Numbers :
Z.add_comm, Z.add_assoc, ...
A large part of ZArith is now simply compatibility notations, for instance
Zplus_comm is an alias for Z.add_comm. The direct use of module Z is now
recommended instead of relying on these compatibility notations.
- Similar major reorganization of NArith, via a module N in NArith/BinNat.v
- Concerning the positive datatype, BinPos.v is now in a specific directory
PArith, and contains an internal submodule Pos. We regroup there functions
such as Pos.add Pos.mul etc as well as many results about them. These results
are here proved directly (no Number interface for strictly positive numbers).
- Note that in spite of the compatibility layers, all these reorganizations
may induce some marginal incompatibilies in scripts. In particular:
* the "?=" notation for positive now refers to a binary function Pos.compare,
instead of the infamous ternary Pcompare (now Pos.compare_cont).
* some hypothesis names generated by the system may changed (typically for
a "destruct Z_le_gt_dec") since naming is done after the short name of
the head predicate (here now "le" in module Z instead of "Zle", etc).
* the internals of Z.add has changed, now relying of Z.pos_sub.
- Also note these new notations:
* "<?" "<=?" "=?" for boolean tests such as Z.ltb Z.leb Z.eqb.
* "÷" for the alternative integer division Z.quot implementing the Truncate
convention (former ZOdiv), while the notation for the Coq usual division
Z.div implementing the Flooring convention remains "/". Their corresponding
modulo functions are Z.rem (no notations) for Z.quot and Z.modulo (infix
"mod" notation) for Z.div.
- Lemmas about conversions between these datatypes are also organized
in modules, see for instance modules Z2Nat, N2Z, etc.
- When creating BigN, the macro-generated part NMake_gen is much smaller.
The generic part NMake has been reworked and improved. Some changes
may introduce incompatibilities. In particular, the order of the arguments
for BigN.shiftl and BigN.shiftr is now reversed: the number to shift now
comes first. By default, the power function now takes two BigN.
- Creation of Vector, an independent library for lists indexed by their length.
Vectors' names overwrite lists' one so you should not "Import" the library.
All old names changed: function names follow the ocaml ones and, for example,
Vcons becomes Vector.cons. You can get [..;..;..]-style notations by importing
Vector.VectorNotations.
- Removal of TheoryList. Requiring List instead should work most of the time.
- New syntax "rew Heq in H" and "rew <- Heq in H" for eq_rect and
eq_rect_r (available by importing module EqNotations).
- Wf.iter_nat is now Peano.nat_iter (with an implicit type argument).
Module System
- The names of modules (and module types) are now in a fully separated
namespace from ordinary definitions: "Definition E:=0. Module E. End E."
is now accepted.
- During subtyping checks, an opaque constant in a module type could now
be implemented by anything of the right type, even if bodies differ.
Said otherwise, with respect to subtyping, an opaque constant behaves
just as a parameter. Coqchk was already implementing this, but not coqtop.
- The inlining done during application of functors can now be controlled
more precisely, by the annotations (no inline) or (inline at level XX).
With the latter annotation, only functor parameters whose levels
are lower or equal than XX will be inlined.
The level of a parameter can be fixed by "Parameter Inline(30) foo".
When levels aren't given, the default value is 100. One can also use
the flag "Set Inline Level ..." to set a level.
- Print Assumptions should now handle correctly opaque modules (#2168).
- Print Module (Type) now tries to print more details, such as types and
bodies of the module elements. Note that Print Module Type could be
used on a module to display only its interface. The option
"Set Short Module Printing" could be used to switch back to the earlier
behavior were only field names were displayed.
CoqIDE
- Coqide now supports the "Restart" command, and "Undo" (with a warning).
Better support for "Abort".
- Coqide now runs coqtop as separated process, making it more robust:
coqtop subprocess can be interrupted, or even killed and relaunched
(cf button "Restart Coq", ex-"Go to Start"). For allowing such
interrupts, the Windows version of coqide now requires Windows >= XP
SP1.
- The communication between CoqIDE and Coqtop is now done via a dialect of XML.
- The backtrack engine of CoqIDE has been reworked, it now uses the
"Backtrack" command similarly to Proof General.
- The Coqide parsing of sentences has be reworked and now supports
tactic delimitation via { }.
- Coqide now accepts the Abort command (wish #2357).
- Coqide can read coq_makefile files as "project file" and use it to
set automatically options to send to coqtop.
- Preference files have moved to $XDG_CONFIG_HOME/coq and accelerators
are not stored as a list anymore.
Internal infrastructure
- Opaque proofs are now loaded lazily by default. This allows to be almost as
fast as -dont-load-proofs, while being safer (no creation of axioms) and
avoiding feature restrictions (Print and Print Assumptions work ok).
- Revised hash-consing code allowing more sharing of memory
- Experimental support added for camlp4 (the one provided alongside ocaml),
simply pass option -usecamlp4 to ./configure. By default camlp5 is used.
- Revised build system: no more stages in Makefile thanks to some recursive
aspect of recent gnu make, use of vo.itarget files containing .v to compile
for both make and ocamlbuild, etc.
- Support of cross-compilation via mingw from unix toward Windows,
contact P. Letouzey for more informations.
- New Makefile rules mli-doc to make html of mli in dev/doc/html and
full-stdlib to get a (huge) pdf reflecting the whole standard library.
Extraction
- By default, opaque terms are now truly considered opaque by extraction:
instead of accessing their body, they are now considered as axioms.
The previous behaviour can be reactivated via the option
"Set Extraction AccessOpaque".
- The pretty-printer for Haskell now produces layout-independant code
- A new command "Separate Extraction cst1 cst2 ..." that mixes a
minimal extracted environment a la "Recursive Extraction" and the
production of several files (one per coq source) a la "Extraction Library".
- New option "Set/Unset Extraction KeepSingleton" for preventing the
extraction to optimize singleton container types.
- The extraction now identifies and properly rejects a particular case of
universe polymorphism it cannot handle yet (the pair (I,I) being Prop).
- Support of anonymous fields in record (#2555).
Tools
- Coq now searches directories specified in COQPATH, $XDG_DATA_HOME/coq,
$XDG_DATA_DIRS/coq, and user-contribs before the standard library.
- Coq rc file has moved to $XDG_CONFIG_HOME/coq.
- Major changes to coq_makefile:
* mli/mlpack/mllib taken into account, ml not preproccessed anymore, ml4 work;
* mlihtml generates doc of mli, install-doc install the html doc in DOCDIR
with the same policy as vo in COQLIB;
* More variables are given by coqtop -config, others are defined only if the
users doesn't have defined them elsewhere. Consequently, generated makefile
should work directly on any architecture;
* Packagers can take advantage of $(DSTROOT) introduction. Installation can
be made in $XDG_DATA_HOME/coq;
* -arg option allows to send option as argument to coqc.
Revision 1.13 / (download) - annotate - [select for diffs], Mon Mar 28 20:39:26 2011 UTC (13 years ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2012Q3-base,
pkgsrc-2012Q3,
pkgsrc-2012Q2-base,
pkgsrc-2012Q2,
pkgsrc-2012Q1-base,
pkgsrc-2012Q1,
pkgsrc-2011Q4-base,
pkgsrc-2011Q4,
pkgsrc-2011Q3-base,
pkgsrc-2011Q3,
pkgsrc-2011Q2-base,
pkgsrc-2011Q2,
pkgsrc-2011Q1-base,
pkgsrc-2011Q1
Changes since 1.12: +4 -6
lines
Diff to previous 1.12 (colored) to selected 1.14 (colored)
Update lang/coq to 8.3pl1 Changes from V8.3 to V8.3pl1 o Type inference, notations and implicit arguments bug fixes - #2448 (alpha-renaming problems with notations internally using binders) - #2454 (pattern-matching sometimes not supporting type casts) - fixing combined use of non-implicit and explictly-declared implicit arguments in inductive arities - restored support for using some ident with different scopes in notations o Ltac and tactics bug fixes - #2414 (rewrite in not looking for eq_ind in the right module) - #2433 (new "is_evar"/"has_evar" to restore support for matching evars in Ltac) - #2453 (dependent destruction) - loop in dependent destruction - new "constr_eq" tactic for restoring support for term equality test in Ltac - setoid rewrite under cases and abstraction fixed o Coqdoc and documentation bugs - #2418 (wrong URLs in documentation) - #2441 (coqdoc bug in Mergesort.v) - #2445 (correct support for "'" character in coqdoc links to notations) - fixed wrong use of "moduleid" instead of "module" in coqdoc html indexes - fixing parsing of Multiplication and Division signs (unicode 0xD7 and 0xF7) o Compilation - #2432 (support for compilation with camlp5 6.02.0) - support for compilation with ocaml >= 3.09.3 restored o Extraction - #2413 (prevent type-unsafe optimisations of pattern matching) - Identifiers of a development aimed to be extracted should avoid containing "__", since the extraction make various use of this sub-string, leading to potential name clashes. This was already so in V8.3, but not announced, as mentionned by #2421. o Miscellaneous bug fixes - #2412 (anomaly Ploc.Exc when using Ltac Debug) - #2419 (redundant opp_compare removed) - #2427 (Module Functor claims Signature does not match) - #2431 (compliance of CoqIDE use of mutexes with FreeBSD) - #2434 (anomaly DuringSyntaxChecking with Local/Global prefixes) - a few improvements in efficiency
Revision 1.12 / (download) - annotate - [select for diffs], Sun Nov 14 20:53:02 2010 UTC (13 years, 5 months ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2010Q4-base,
pkgsrc-2010Q4
Changes since 1.11: +7 -8
lines
Diff to previous 1.11 (colored) to selected 1.14 (colored)
Update lang/coq to 8.3 Main changes: Includes a new tactic (nsatz, standing for Hilbert's NullStellensatz, that extends ring to systems of polynomial equations) and a few new libraries (a certification of mergesort, a new library of finite sets with computational and logical contents separated). This version also comes with many improvements of existing features, especially regarding the tactics, the module system, extraction, the type classes, the program command, libraries, coqdoc. Here is an excerpt: * new operator <+ for conveniently chaining application of functors * new round of extension of the modular library of arithmetic * support for matching terms with binders in Ltac, * linking notations in coqdoc, * quote tactic now working on arbitrary expressions, * Lemma and co accept parameters that are automatically introduced, * interactive proofs in module types, * a beautifying coqc option for pretty-printing files See the file CHANGES for a full log of changes.
Revision 1.11 / (download) - annotate - [select for diffs], Sun Nov 7 15:39:55 2010 UTC (13 years, 5 months ago) by tonio
Branch: MAIN
Changes since 1.10: +2 -2
lines
Diff to previous 1.10 (colored) to selected 1.14 (colored)
Make it build with newer gmake
Revision 1.10 / (download) - annotate - [select for diffs], Sat Dec 12 21:12:43 2009 UTC (14 years, 4 months ago) by asau
Branch: MAIN
CVS Tags: pkgsrc-2010Q3-base,
pkgsrc-2010Q3,
pkgsrc-2010Q2-base,
pkgsrc-2010Q2,
pkgsrc-2010Q1-base,
pkgsrc-2010Q1,
pkgsrc-2009Q4-base,
pkgsrc-2009Q4
Changes since 1.9: +2 -1
lines
Diff to previous 1.9 (colored) to selected 1.14 (colored)
Support staged installation.
Revision 1.9 / (download) - annotate - [select for diffs], Sat Sep 5 20:44:58 2009 UTC (14 years, 7 months ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2009Q3-base,
pkgsrc-2009Q3
Changes since 1.8: +7 -6
lines
Diff to previous 1.8 (colored) to selected 1.14 (colored)
Update lang/coq to 8.2pl1
Changes from V8.1 to V8.2
=========================
Language
- If a fixpoint is not written with an explicit { struct ... }, then
all arguments are tried successively (from left to right) until one is
found that satisfies the structural decreasing condition.
- New experimental typeclass system giving ad-hoc polymorphism and
overloading based on dependent records and implicit arguments.
- New syntax "let 'pat := b in c" for let-binding using irrefutable patterns.
- New syntax "forall {A}, T" for specifying maximally inserted implicit
arguments in terms.
- Sort of Record/Structure, Inductive and CoInductive defaults to Type
if omitted.
- Support for optional "where" notation clauses for record fields.
- (Co)Inductive types can be defined as records
(e.g. "CoInductive stream := { hd : nat; tl : stream }.")
- New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent
statements.
- Support for sort-polymorphism on constants denoting inductive types.
- Several evolutions of the module system (handling of module aliases,
functorial module types, an Include feature, etc).
- Prop now a subtype of Set (predicative and impredicative forms).
- Recursive inductive types in Prop with a single constructor of which
all arguments are in Prop is now considered to be a singleton
type. It consequently supports all eliminations to Prop, Set and Type.
As a consequence, Acc_rect has now a more direct proof [possible source
of easily fixed incompatibility in case of manual definition of a recursor
in a recursive singleton inductive type].
- New syntax to do implicit generalization in binders and inside terms.
- New tentative syntax for introduction of record objects without mentioning
the constructor {| field := body; ... |}, turning missing fields into holes
(compatible with refine and Program).
Vernacular commands
- Added option Global to "Arguments Scope" for section surviving.
- Added option "Unset Elimination Schemes" to deactivate the automatic
generation of elimination schemes.
- Modification of the Scheme command so you can ask for the name to be
automatically computed (e.g. Scheme Induction for nat Sort Set).
- New command "Combined Scheme" to build combined mutual induction
principles from existing mutual induction principles.
- New command "Scheme Equality" to build a decidable (boolean) equality
for simple inductive datatypes and a decision property over this equality
(e.g. Scheme Equality for nat).
- Added option "Set Equality Scheme" to make automatic the declaration
of the boolean equality when possible.
- Source of universe inconsistencies now printed when option
"Set Printing Universes" is activated.
- New option "Set Printing Existential Instances" for making the display of
existential variable instances explicit.
- Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the
"compute"/"cbv" reduction strategy, respectively meaning reduce only, or
everything but, the constants id1 ... idn. "lazy" alone or followed by
"[id1 ... idn]", and "-[id1 ... idn]" also supported, meaning apply
all of beta-iota-zeta-delta, possibly restricting delta.
- New command "Strategy" to control the expansion of constants during
conversion tests. It generalizes commands Opaque and Transparent by
introducing a range of levels. Lower levels are assigned to constants
that should be expanded first.
- New options Global and Local to Opaque and Transparent.
- New command "Print Assumptions" to display all variables, parameters
or axioms a theorem or definition relies on.
- "Add Rec LoadPath" now provides references to libraries using partially
qualified names (this holds also for coqtop/coqc option -R).
- SearchAbout supports negated search criteria, reference to logical objects
by their notation, and more generally search of subterms.
- "Declare ML Module" now allows to import .cmxs files when Coq is
compiled in native code with a version of OCaml that supports native
Dynlink (>= 3.11).
- New command "Create HintDb name [discriminated]" to explicitely declare
a new hint database and optionaly turn on a discrimination net
implementation to index all the lemmas in the database.
- New commands "Hint Transparent" and "Hint Opaque" to set the unfolding
status of definitions used by auto. This information is taken into account
by the discrimination net and the unification algorithm.
- "Hint Extern" now takes an optional pattern and applies the given tactic
all the time if no pattern is given.
- Specific sort constraints on Record now taken into account.
- "Print LoadPath" supports a path argument to filter the display.
Libraries
- Several parts of the libraries are now in Type, in particular FSets,
SetoidList, ListSet, Sorting, Zmisc. This may induce a few
incompatibilities. In case of trouble while fixing existing development,
it may help to simply declare Set as an alias for Type (see file
SetIsType).
- New arithmetical library in theories/Numbers. It contains:
* an abstract modular development of natural and integer arithmetics
in Numbers/Natural/Abstract and Numbers/Integer/Abstract
* an implementation of efficient computational bounded and unbounded
integers that can be mapped to processor native arithmetics.
See Numbers/Cyclic/Int31 for 31-bit integers and Numbers/Natural/BigN
for unbounded natural numbers and Numbers/Integer/BigZ for unbounded
integers.
* some proofs that both older libraries Arith, ZArith and NArith and
newer BigN and BigZ implement the abstract modular development.
This allows in particular BigN and BigZ to already come with a
large database of basic lemmas and some generic tactics (ring),
This library has still an experimental status, as well as the
processor-acceleration mechanism, but both its abstract and its
concrete parts are already quite usable and could challenge the use
of nat, N and Z in actual developments. Moreover, an extension of
this framework to rational numbers is ongoing, and an efficient
Q structure is already provided (see Numbers/Rational/BigQ), but
this part is currently incomplete (no abstract layer and generic
lemmas).
- Many changes in FSets/FMaps. In practice, compatibility with earlier
version should be fairly good, but some adaptations may be required.
* Interfaces of unordered ("weak") and ordered sets have been factorized
thanks to new features of Coq modules (in particular Include), see
FSetInterface. Same for maps. Hints in these interfaces have been
reworked (they are now placed in a "set" database).
* To allow full subtyping between weak and ordered sets, a field
"eq_dec" has been added to OrderedType. The old version of OrderedType
is now called MiniOrderedType and functor MOT_to_OT allow to
convert to the new version. The interfaces and implementations
of sets now contain also such a "eq_dec" field.
* FSetDecide, contributed by Aaron Bohannon, contains a decision
procedure allowing to solve basic set-related goals (for instance,
is a point in a particular set ?). See FSetProperties for examples.
* Functors of properties have been improved, especially the ones about
maps, that now propose some induction principles. Some properties
of fold need less hypothesis.
* More uniformity in implementations of sets and maps: they all use
implicit arguments, and no longer export unnecessary scopes (see
bug #1347)
* Internal parts of the implementations based on AVL have evolved a
lot. The main files FSetAVL and FMapAVL are now much more
lightweight now. In particular, minor changes in some functions
has allowed to fully separate the proofs of operational
correctness from the proofs of well-balancing: well-balancing is
critical for efficiency, but not anymore for proving that these
trees implement our interfaces, hence we have moved these proofs
into appendix files FSetFullAVL and FMapFullAVL. Moreover, a few
functions like union and compare have been modified in order to be
structural yet efficient. The appendix files also contains
alternative versions of these few functions, much closer to the
initial Ocaml code and written via the Function framework.
- Library IntMap, subsumed by FSets/FMaps, has been removed from
Coq Standard Library and moved into a user contribution Cachan/IntMap
- Better computational behavior of some constants (eq_nat_dec and
le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare
transparent, ...) (exceptional source of incompatibilities).
- Boolean operators moved from module Bool to module Datatypes (may need
to rename qualified references in script and force notations || and &&
to be at levels 50 and 40 respectively).
- The constructors xI and xO of type positive now have postfix notations
"~1" and "~0", allowing to write numbers in binary form easily, for instance
6 is 1~1~0 and 4*p is p~0~0 (see BinPos.v).
- Improvements to NArith (Nminus, Nmin, Nmax), and to QArith (in particular
a better power function).
- Changes in ZArith: several additional lemmas (used in theories/Numbers),
especially in Zdiv, Znumtheory, Zpower. Moreover, many results in
Zdiv have been generalized: the divisor may simply be non-null
instead of strictly positive (see lemmas with name ending by
"_full"). An alternative file ZOdiv proposes a different behavior
(the one of Ocaml) when dividing by negative numbers.
- Changes in Arith: EqNat and Wf_nat now exported from Arith, some
constructions on nat that were outside Arith are now in (e.g. iter_nat).
- In SetoidList, eqlistA now expresses that two lists have similar elements
at the same position, while the predicate previously called eqlistA
is now equivlistA (this one only states that the lists contain the same
elements, nothing more).
- Changes in Reals:
* Most statement in "sigT" (including the
completeness axiom) are now in "sig" (in case of incompatibility,
use proj1_sig instead of projT1, sig instead of sigT, etc).
* More uniform naming scheme (identifiers in French moved to English,
consistent use of 0 -- zero -- instead of O -- letter O --, etc).
* Lemma on prod_f_SO is now on prod_f_R0.
* Useless hypothesis of ln_exists1 dropped.
* New Rlogic.v states a few logical properties about R axioms.
* RIneq.v extended and made cleaner.
- Slight restructuration of the Logic library regarding choice and classical
logic. Addition of files providing intuitionistic axiomatizations of
descriptions: Epsilon.v, Description.v and IndefiniteDescription.v.
- Definition of pred and minus made compatible with the structural
decreasing criterion for use in fixpoints.
- Files Relations/Rstar.v and Relations/Newman.v moved out to the user
contribution repository (contribution CoC_History). New lemmas about
transitive closure added and some bound variables renamed (exceptional
risk of incompatibilities).
Notations, coercions, implicit arguments and type inference
- More automation in the inference of the return clause of dependent
pattern-matching problems.
- Experimental allowance for omission of the clauses easily detectable as
impossible in pattern-matching problems.
- Improved inference of implicit arguments, now working inside record
declarations.
- New options "Set Maximal Implicit Insertion", "Set Reversible Pattern
Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit
Defensive" for controlling inference and use of implicit arguments.
- New modifier in "Implicit Arguments" to force an implicit argument to
be maximally inserted.
- New options Global and Local to "Implicit Arguments" for section
surviving or non export outside module.
- Level "constr" moved from 9 to 8.
- Structure/Record now printed as Record (unless option Printing All is set).
- Support for parametric notations defining constants.
- Insertion of coercions below product types refrains to unfold
constants (possible source of incompatibility).
- New support for fix/cofix in notations.
Tactic Language
- Second-order pattern-matching now working in Ltac "match" clauses
(syntax for second-order unification variable is "@?X").
- Support for matching on let bindings in match context using syntax
"H := body" or "H := body : type".
- (?X ?Y) patterns now match any application instead of only unary
applications (possible source of incompatibility).
- Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer).
- The general sequence tactical "expr_0 ; [ expr_1 | ... | expr_n ]"
is extended so that at most one expr_i may have the form "expr .."
or just "..". Also, n can be different from the number of subgoals
generated by expr_0. In this case, the value of expr (or idtac in
case of just "..") is applied to the intermediate subgoals to make
the number of tactics equal to the number of subgoals.
- A name used as the name of the parameter of a lemma (like f in
"apply f_equal with (f:=t)") is now interpreted as a ltac variable
if such a variable exists (this is a possible source of
incompatibility and it can be fixed by renaming the variables of a
ltac function into names that do not clash with the lemmas
parameter names used in the tactic).
- New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression.
- "let rec ... in ... " now supported for expressions without explicit
parameters; interpretation is lazy to the contrary of "let ... in ...";
hence, the "rec" keyword can be used to turn the argument of a
"let ... in ..." into a lazy one.
- Patterns for hypotheses types in "match goal" are now interpreted in
type_scope.
- A bound variable whose name is not used elsewhere now serves as
metavariable in "match" and it gets instantiated by an identifier
(allow e.g. to extract the name of a statement like "exists x, P x").
- New printing of Ltac call trace for better debugging.
- The C-zar (formerly know as declarative) proof language is now properly
documented.
Tactics
- New tactics "apply -> term", "apply <- term", "apply -> term in
ident", "apply <- term in ident" for applying equivalences (iff).
- "apply" and "rewrite" now take open terms (terms with undefined existentials)
as input.
- Slight improvement of the hnf and simpl tactics when applied on
expressions with explicit occurrences of match or fix.
- New tactics "eapply in", "erewrite", "erewrite in".
- New tactics "ediscriminate", "einjection", "esimplify_eq".
- Tactics "discriminate", "injection", "simplify_eq" now support any
term as argument. Clause "with" is also supported.
- Unfoldable references can be given by notation's string rather than by name
in unfold.
- The "with" arguments are now typed using informations from the current goal:
allows support for coercions and more inference of implicit arguments.
- Application of "f_equal"-style lemmas works better.
- Tactics elim, case, destruct and induction now support variants eelim,
ecase, edestruct and einduction.
- Tactics destruct and induction now support the "with" option and the
"in" clause option. If the option "in" is used, an equality is added
to remember the term to which the induction or case analysis applied
(possible source of parsing incompatibilities when destruct or induction is
part of a let-in expression in Ltac; extra parentheses are then required).
- New support for "as" clause in tactics "apply in" and "eapply in".
- Some new intro patterns:
* intro pattern "?A" genererates a fresh name based on A.
Caveat about a slight loss of compatibility:
Some intro patterns don't need space between them. In particular
intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it
is still legal but equivalent to intros ?a ?b.
* intro pattern "(A & ... & Y & Z)" synonym to "(A,....,(Y,Z)))))"
for right-associative constructs like /\ or exists.
- Several syntax extensions concerning "rewrite":
* "rewrite A,B,C" can be used to rewrite A, then B, then C. These rewrites
occur only on the first subgoal: in particular, side-conditions of the
"rewrite A" are not concerned by the "rewrite B,C".
* "rewrite A by tac" allows to apply tac on all side-conditions generated by
the "rewrite A".
* "rewrite A at n" allows to select occurrences to rewrite: rewrite only
happen at the n-th exact occurrence of the first successful matching of
A in the goal.
* "rewrite 3 A" or "rewrite 3!A" is equivalent to "rewrite A,A,A".
* "rewrite !A" means rewriting A as long as possible (and at least once).
* "rewrite 3?A" means rewriting A at most three times.
* "rewrite ?A" means rewriting A as long as possible (possibly never).
* many of the above extensions can be combined with each other.
- Introduction patterns better respect the structure of context in presence of
missing or extra names in nested disjunction-conjunction patterns [possible
source of rare incompatibilities].
- New syntax "rename a into b, c into d" for "rename a into b; rename c into d"
- New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]"
to do induction-inversion on instantiated inductive families ? la BasicElim.
- Tactics "apply" and "apply in" now able to reason modulo unfolding of
constants (possible source of incompatibility in situations where apply
may fail, e.g. as argument of a try or a repeat and in a ltac function);
versions that do not unfold are renamed into "simple apply" and
"simple apply in" (usable for compatibility or for automation).
- Tactics "apply" and "apply in" now able to traverse conjunctions and to
select the first matching lemma among the components of the conjunction;
tactic "apply" also able to apply lemmas of conclusion an empty type.
- Tactic "apply" now supports application of several lemmas in a row.
- Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)".
- New tactic "instantiate" (without argument).
- Tactic firstorder "with" and "using" options have their meaning swapped for
consistency with auto/eauto (source of incompatibility).
- Tactic "generalize" now supports "at" options to specify occurrences
and "as" options to name the quantified hypotheses.
- New tactic "specialize H with a" or "specialize (H a)" allows to transform
in-place a universally-quantified hypothesis (H : forall x, T x) into its
instantiated form (H : T a). Nota: "specialize" was in fact there in earlier
versions of Coq, but was undocumented, and had a slightly different behavior.
- New tactic "contradict H" can be used to solve any kind of goal as long as
the user can provide afterwards a proof of the negation of the hypothesis H.
If H is already a negation, say ~T, then a proof of T is asked.
If the current goal is a negation, say ~U, then U is saved in H afterwards,
hence this new tactic "contradict" extends earlier tactic "swap", which is
now obsolete.
- Tactics f_equal is now done in ML instead of Ltac: it now works on any
equality of functions, regardless of the arity of the function.
- New options "before id", "at top", "at bottom" for tactics "move"/"intro".
- Some more debug of reflexive omega (romega), and internal clarifications.
Moreover, romega now has a variant "romega with *" that can be also used
on non-Z goals (nat, N, positive) via a call to a translation tactic named
zify (its purpose is to Z-ify your goal...). This zify may also be used
independantly of romega.
- Tactic "remember" now supports an "in" clause to remember only selected
occurrences of a term.
- Tactic "pose proof" supports name overwriting in case of specialization of an
hypothesis.
- Semi-decision tactic "jp" for first-order intuitionistic logic moved to user
contributions (subsumed by "firstorder").
Program
- Moved useful tactics in theories/Program and documented them.
- Add Program.Basics which contains standard definitions for functional
programming (id, apply, flip...)
- More robust obligation handling, dependent pattern-matching and
well-founded definitions.
- Program CoFixpoint is accepted, Program Fixpoint uses the new way to infer
which argument decreases structurally.
- Program Lemma, Axiom etc... now permit to have obligations in the statement
iff they can be automatically solved by the default tactic.
- Renamed "Obligations Tactic" command to "Obligation Tactic".
- New command "Preterm [ of id ]" to see the actual term fed to Coq for
debugging purposes.
- New option "Transparent Obligations" to control the declaration of
obligations as transparent or opaque. All obligations are now transparent
by default, otherwise the system declares them opaque if possible.
- Changed the notations "left" and "right" to "in_left" and "in_right" to hide
the proofs in standard disjunctions, to avoid breaking existing scripts when
importing Program. Also, put them in program_scope.
Type Classes
- New "Class", "Instance" and "Program Instance" commands to define
classes and instances documented in the reference manual.
- New binding construct "`{Class_1 param_1 .. param_n, Class_2 ...}"
for binding type classes, usable everywhere.
- New command " Print Classes " and " Print Instances some_class " to
print tables for typeclasses.
- New default eauto hint database "typeclass_instances" used by the default
typeclass instance search tactic.
- New theories directory "theories/Classes" for standard typeclasses
declarations. Module Classes.RelationClasses is a typeclass port of
Relation_Definitions plus a generic development of algebra on
n-ary heterogeneous predicates.
Setoid rewriting
- Complete (and still experimental) rewrite of the tactic
based on typeclasses. The old interface and semantics are
almost entirely respected, except:
- Import Setoid is now mandatory to be able to call setoid_replace
and declare morphisms.
- "-->", "++>" and "==>" are now right associative notations
declared at level 55 in scope signature_scope.
Their introduction may break existing scripts that defined
them as notations with different levels.
- One can use [Typeclasses Opaque/Transparent [cst]] to indicate
that [cst] should not be unfolded during unification for morphism
resolution, by default all constants are transparent.
- The [setoid_rewrite]'s semantics change when rewriting with
a lemma: it can rewrite two different instantiations of the lemma
at once. Use [setoid_rewrite H at 1] for (almost) the usual semantics.
[setoid_rewrite] will also try to rewrite under binders now, and can
succeed on different terms than before. In particular, it will unify under
let-bound variables. When called through [rewrite], the semantics are
unchanged though.
- [Add Morphism term : id] has different semantics when used with
parametric morphism: it will try to find a relation on the parameters
too. The behavior has also changed with respect to default relations:
the most recently declared Setoid/Relation will be used, the documentation
explains how to customize this behavior.
- Parametric Relation and Morphism are declared differently, using the
new [Add Parametric] commands, documented in the manual.
- Setoid_Theory is now an alias to Equivalence, scripts building objects
of type Setoid_Theory need to unfold (or [red]) the definitions
of Reflexive, Symmetric and Transitive in order to get the same goals
as before. Scripts which introduced variables explicitely will not break.
- The order of subgoals when doing [setoid_rewrite] with side-conditions
is now always the same: first the new goal, then the conditions.
- New standard library modules Classes.Morphisms declares
standard morphisms on refl/sym/trans relations.
Classes.Morphisms_Prop declares morphisms on propositional
connectives and Classes.Morphisms_Relations on generalized predicate
connectives. Classes.Equivalence declares notations and tactics
related to equivalences and Classes.SetoidTactics defines the
setoid_replace tactics and some support for the "Add *" interface,
notably the tactic applied automatically before each "Add Morphism"
proof.
- User-defined subrelations are supported, as well as higher-order morphisms
and rewriting under binders. The tactic is also extensible entirely in Ltac.
The documentation has been updated to cover these features.
- [setoid_rewrite] and [rewrite] now support the [at] modifier to select
occurrences to rewrite, and both use the [setoid_rewrite] code, even when
rewriting with leibniz equality if occurrences are specified.
Extraction
- Improved behavior of the Caml extraction of modules: name clashes should
not happen anymore.
- The command Extract Inductive has now a syntax for infix notations. This
allows in particular to map Coq lists and pairs onto Caml ones:
Extract Inductive list => list [ "[]" "(::)" ].
Extract Inductive prod => "(*)" [ "(,)" ].
- In pattern matchings, a default pattern "| _ -> ..." is now used whenever
possible if several branches are identical. For instance, functions
corresponding to decidability of equalities are now linear instead of
quadratic.
- A new instruction Extraction Blacklist id1 .. idn allows to prevent filename
conflits with existing code, for instance when extracting module List
to Ocaml.
CoqIDE
- CoqIDE font defaults to monospace so as indentation to be meaningful.
- CoqIDE supports nested goals and any other kind of declaration in the middle
of a proof.
- Undoing non-tactic commands in CoqIDE works faster.
- New CoqIDE menu for activating display of various implicit informations.
- Added the possibility to choose the location of tabs in coqide:
(in Edit->Preferences->Misc)
- New Open and Save As dialogs in CoqIDE which filter *.v files.
Tools
- New stand-alone .vo files verifier "coqchk".
- Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir".
- New coqtop/coqc option -exclude-dir to exclude subdirs for option -R.
- The binary "parser" has been renamed to "coq-parser".
coqdoc
- Improved coqdoc and dump of globalization information to give more
meta-information on identifiers. All categories of Coq definitions are
supported, which makes typesetting trivial in the generated documentation.
- A "--interpolate" option permits to use typesetting information from the
typechecked part of the file to typeset identifiers appearing in Coq escapings
inside the documentation.
- Better handling of utf8 ("--utf8" option) and respect of spaces in the source.
- Support for hyperlinking and indexing developments in the TeX output.
- New option "color" of the coqdoc style file to render identifiers using colors.
- Additional macros in the TeX ouput allowing to customize indentation and size of
empty lines. New environment "coqdoccode" for Coq code.
Miscellaneous
- Coq installation provides enough files so that Ocaml's extensions need not
the Coq sources to be compiled (this assumes O'Caml 3.10 and Camlp5).
- New commands "Set Whelp Server" and "Set Whelp Getter" to customize the
Whelp search tool.
- Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into
"Test Printing Let for ref" and "Test Printing If for ref".
- An overhauled build system (new Makefiles); see dev/doc/build-system.txt.
- Add -browser option to configure script.
- Build a shared library for the C part of Coq, and use it by default on
non-(Windows or MacOS) systems. Bytecode executables are now pure. The
behaviour is configurable with -coqrunbyteflags, -coqtoolsbyteflags and
-custom configure options.
- Complexity tests can be skipped by setting the environment variable
COQTEST_SKIPCOMPLEXITY.
Revision 1.8 / (download) - annotate - [select for diffs], Sat Jan 12 11:48:40 2008 UTC (16 years, 3 months ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2009Q2-base,
pkgsrc-2009Q2,
pkgsrc-2009Q1-base,
pkgsrc-2009Q1,
pkgsrc-2008Q4-base,
pkgsrc-2008Q4,
pkgsrc-2008Q3-base,
pkgsrc-2008Q3,
pkgsrc-2008Q2-base,
pkgsrc-2008Q2,
pkgsrc-2008Q1-base,
pkgsrc-2008Q1,
cwrapper,
cube-native-xorg-base,
cube-native-xorg
Changes since 1.7: +5 -5
lines
Diff to previous 1.7 (colored) to selected 1.14 (colored)
Update lang/coq to 8.1pl3 hanges from V8.1pl2 to V8.1pl3 =============================== Bug fixes - A critical bug and a few other bugs have been fixed.
Revision 1.7 / (download) - annotate - [select for diffs], Sat Dec 1 13:05:36 2007 UTC (16 years, 4 months ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2007Q4-base,
pkgsrc-2007Q4
Changes since 1.6: +6 -5
lines
Diff to previous 1.6 (colored) to selected 1.14 (colored)
Update lang/coq to 8.2pl2 As camlp5 is required with ocaml 3.10, bring it as a dependency anyway, instead of requiring ocaml 3.10 Changes include: * Installation - Support for compilation with ocaml 3.10 and (transitional) camlp5. - Many bugs have been fixed (cf coq-bugs web page) - All known failures of ROmega have been fixed. It should now be a faithful and quicker replacement for Omega (except when nat parts are involved). ROmega and Omega now handle <->. - Better computational behavior of some constants (eq_nat_dec and le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare transparent) [exceptionally source of incompatibilities]. - Loading FSets/FMap used to open unwanted scopes of integer datatypes (see bug #1347). These scopes may need to be manually opened now.
Revision 1.6 / (download) - annotate - [select for diffs], Sun Feb 25 15:03:52 2007 UTC (17 years, 1 month ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2007Q3-base,
pkgsrc-2007Q3,
pkgsrc-2007Q2-base,
pkgsrc-2007Q2,
pkgsrc-2007Q1-base,
pkgsrc-2007Q1
Changes since 1.5: +5 -5
lines
Diff to previous 1.5 (colored) to selected 1.14 (colored)
Update lang/coq to 8.1 Many changes, among them: - Many bugs have been fixed (cf coq-bugs web page) - changed parsing precedence of let/in and fun constructions of Ltac: let x := t in e1; e2 is now parsed as let x := t in (e1;e2). - New primitive "external" for communication with tool external to Coq. - Omega now handles arbitrary precision integers. - Haskell extraction: types of functions are now printed, better unsafeCoerce mechanism, both for hugs and ghc. - Scheme extraction improved, see http://www.pps.jussieu.fr/~letouzey/scheme. - New notation "exists! x:A, P" for unique existence. - New library on String and Ascii characters (contributed by L. Thery). - New library FSets+FMaps of finite sets and maps. - New library QArith on rational numbers. - Few improvements in ZArith potentially exceptionally breaking the compatibility (useless hypothesys of Zgt_square_simpl and Zlt_square_simpl removed; fixed names mentioning letter O instead of digit 0; weaken premises in Z_lt_induction).
Revision 1.5 / (download) - annotate - [select for diffs], Fri Jan 27 19:22:58 2006 UTC (18 years, 2 months ago) by tonio
Branch: MAIN
CVS Tags: pkgsrc-2006Q4-base,
pkgsrc-2006Q4,
pkgsrc-2006Q3-base,
pkgsrc-2006Q3,
pkgsrc-2006Q2-base,
pkgsrc-2006Q2,
pkgsrc-2006Q1-base,
pkgsrc-2006Q1
Changes since 1.4: +5 -5
lines
Diff to previous 1.4 (colored) to selected 1.14 (colored)
Update lang/coq to 8.0pl3 Changelog: - Coq sources made compatible with ocaml 3.09.0 and lablgtk 2.6.0. - The search depth argument of auto can be parameterised in the Ltac language - Added entry constr_may_eval for tactic extensions (new syntax) - A couple of lemmas of ZArith were renamed: O -> 0 - many bugfixes, for extraction, Ltac, tactics...
Revision 1.4 / (download) - annotate - [select for diffs], Mon Jan 16 14:34:34 2006 UTC (18 years, 3 months ago) by tonio
Branch: MAIN
Changes since 1.3: +2 -2
lines
Diff to previous 1.3 (colored) to selected 1.14 (colored)
Make lang/coq compile with ocaml 3.09 by applying the patch distributed by the coq team Bump PKGREVISION, and require ocaml >= 3.09
Revision 1.3 / (download) - annotate - [select for diffs], Thu Feb 24 09:03:06 2005 UTC (19 years, 1 month ago) by agc
Branch: MAIN
CVS Tags: pkgsrc-2005Q4-base,
pkgsrc-2005Q4,
pkgsrc-2005Q3-base,
pkgsrc-2005Q3,
pkgsrc-2005Q2-base,
pkgsrc-2005Q2,
pkgsrc-2005Q1-base,
pkgsrc-2005Q1
Changes since 1.2: +2 -1
lines
Diff to previous 1.2 (colored) to selected 1.14 (colored)
Add RMD160 digests
Revision 1.2 / (download) - annotate - [select for diffs], Sat Feb 5 11:19:02 2005 UTC (19 years, 2 months ago) by adrianp
Branch: MAIN
Changes since 1.1: +4 -4
lines
Diff to previous 1.1 (colored) to selected 1.14 (colored)
- Update of coq from 7.4 to 8.0pl2 - Initial patches supplied by Antoine Reilles, thanks ! - Lots of changes/fixes/updates, see: CHANGES
Revision 1.1.1.1 / (download) - annotate - [select for diffs] (vendor branch), Sat Mar 22 20:21:17 2003 UTC (21 years, 1 month ago) by kristerw
Branch: TNF
CVS Tags: pkgsrc-base,
pkgsrc-2004Q4-base,
pkgsrc-2004Q4,
pkgsrc-2004Q3-base,
pkgsrc-2004Q3,
pkgsrc-2004Q2-base,
pkgsrc-2004Q2,
pkgsrc-2004Q1-base,
pkgsrc-2004Q1,
pkgsrc-2003Q4-base,
pkgsrc-2003Q4
Changes since 1.1: +0 -0
lines
Diff to previous 1.1 (colored) to selected 1.14 (colored)
By popular demand, move coq-7.4 from math to lang in order to be consistent
with prior art (e.g. lang/twelf).
Coq is a Proof Assistant for a Logical Framework known as the
Calculus of Inductive Constructions. It allows the interactive
construction of formal proofs, and also the manipulation of
functional programs consistently with their specifications.
Revision 1.1 / (download) - annotate - [select for diffs], Sat Mar 22 20:21:17 2003 UTC (21 years, 1 month ago) by kristerw
Branch: MAIN
Diff to selected 1.14 (colored)
Initial revision