| Age | Commit message (Collapse) | Author | Files | Lines | |
|---|---|---|---|---|---|
| 2022-11-23 | massive revision bump after textproc/icu update | adam | 1 | -2/+2 | |
| 2022-08-11 | Bump all dependent packages of wayland (belatedly) | gutteridge | 1 | -2/+2 | |
| The package changed with the addition of its libepoll-shim dependency. Otherwise, we can get: ERROR: libepoll-shim>=0.0.20210418 is not installed; can't buildlink files. | |||||
| 2022-06-30 | *: Revbump packages that use Python at runtime without a PKGNAME prefix | nia | 1 | -1/+2 | |
| 2022-06-21 | lang/coq: update to 8.15.2 to make it work with current ocaml. | dholland | 10 | -3459/+3288 | |
| (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. | |||||
| 2022-06-03 | coq: mark as BROKEN because it does not support ocaml 4.14 | wiz | 1 | -1/+3 | |
| 2022-05-01 | *: fix usage of versioned_dependencies | wiz | 2 | -4/+3 | |
| Remove unused includes, fix dependencies where it's not included. | |||||
| 2022-04-18 | revbump for textproc/icu update | adam | 1 | -2/+2 | |
| 2021-12-08 | revbump for icu and libffi | adam | 1 | -2/+2 | |
| 2021-10-26 | lang: Replace RMD160 checksums with BLAKE2s checksums | nia | 1 | -2/+2 | |
| 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 | |||||
| 2021-10-07 | lang: Remove SHA1 hashes for distfiles | nia | 1 | -2/+1 | |
| 2021-04-21 | revbump for textproc/icu | adam | 1 | -2/+2 | |
| 2021-03-08 | Recursive revbump associated with update of lang/ocaml | jaapb | 1 | -1/+2 | |
| 2021-02-09 | take MAINTAINER, ok jaapb@ | dholland | 1 | -2/+2 | |
| 2021-02-09 | Update lang/coq to 8.12.2. | dholland | 6 | -713/+2021 | |
| 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 | |||||
| 2020-11-05 | *: Recursive revbump from textproc/icu-68.1 | ryoon | 1 | -2/+2 | |
| 2020-08-17 | *: revbump after fontconfig bl3 changes (libuuid removal) | leot | 1 | -2/+2 | |
| 2020-06-02 | Revbump for icu | adam | 1 | -2/+2 | |
| 2020-05-23 | (lang/coq) Fix build: Remove no effective SUBST block | mef | 1 | -7/+1 | |
| 2020-04-28 | lang/coq: needs bash as tool | riastradh | 1 | -1/+2 | |
| Otherwise build fails with: OCAMLOPT -o bin/coqide CHECK revision env: bash: No such file or directory gmake[1]: *** [Makefile.dev:34: revision] Error 127 gmake[1]: Leaving directory '/tmp/pkgbuild/2020Q1/lang/coq/work/coq-8.10.2' gmake: *** [Makefile:179: submake] Error 2 | |||||
| 2020-03-10 | librsvg: update bl3.mk to remove libcroco in rust case | wiz | 1 | -2/+2 | |
| recursive bump for the dependency change | |||||
| 2020-03-08 | *: recursive bump for libffi | wiz | 1 | -2/+2 | |
| 2020-03-01 | lang/coq now needs adwaita-icon-theme. | dholland | 2 | -2/+4 | |
| (without it the new coqide is missing things, and it seems to specifically refer to adwaita-icon-theme by name) Bump PKGREVISION to 1, since coqide is a default-on option. | |||||
| 2020-01-24 | Updated lang/coq to version 8.10.2. | jaapb | 6 | -116/+175 | |
| 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. | |||||
| 2020-01-18 | *: Recursive revision bump for openssl 1.1.1. | jperkin | 1 | -2/+2 | |
| 2019-11-03 | lang: align variable assignments | rillig | 2 | -59/+59 | |
| pkglint -Wall -F --only aligned --only indent -r No manual corrections. | |||||
| 2019-09-02 | Rewrite PYTHON_VERSIONS_ACCEPTED to PYTHON_VERSIONS_INCOMPATIBLE | adam | 1 | -2/+2 | |
| 2019-09-01 | coq: patch to build with ocaml 4.08 | markd | 3 | -3/+19 | |
| 2019-07-21 | *: recursive bump for gdk-pixbuf2-2.38.1 | wiz | 1 | -2/+2 | |
| 2019-07-20 | *: recursive bump for nettle 3.5.1 | wiz | 1 | -1/+2 | |
| 2019-05-23 | Updated lang/coq to version 8.9.1. | jaapb | 2 | -8/+7 | |
| 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. | |||||
| 2019-05-05 | Recursive rebvump from devel/nss | ryoon | 1 | -2/+2 | |
| 2019-04-26 | More packages wave bye-bye to python34 and python35 | roy | 1 | -2/+2 | |
| 2019-04-25 | PKGREVISION bump for anything using python without a PYPKGPREFIX. | maya | 1 | -2/+2 | |
| This is a semi-manual PKGREVISION bump. | |||||
| 2019-04-03 | Recursive revbump from textproc/icu | ryoon | 1 | -1/+2 | |
| 2019-03-06 | Updated lang/coq to version 8.9.0. | jaapb | 5 | -2130/+2202 | |
| Many improvements and fixes, but none that appear to break compatibility. For more details see the CHANGES file. | |||||
| 2018-12-09 | revbump after updating textproc/icu | adam | 1 | -2/+2 | |
| 2018-11-29 | Revbump for libcanberra gstreamer change. | prlw1 | 1 | -2/+2 | |
| 2018-11-14 | Revbump after cairo 1.16.0 update. | kleink | 1 | -2/+2 | |
| 2018-11-12 | Recursive revbump from hardbuzz-2.1.1 | ryoon | 1 | -2/+2 | |
| 2018-10-24 | *: (belatedly) revbump for net/libsoup update | leot | 1 | -1/+2 | |
| Thanks to <wiz>! | |||||
| 2018-08-02 | Updated package lang/coq to version 8.8.1. | jaapb | 4 | -192/+437 | |
| 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. | |||||
| 2018-07-20 | Recursive revbump from textproc/icu-62.1 | ryoon | 1 | -2/+2 | |
| 2018-06-16 | coq: always installs coqdoc.sty in tex tree. | markd | 1 | -2/+2 | |
| 2018-04-17 | Add p11-kit to gnutls/bl3.mk and bump dependencies. | wiz | 1 | -2/+2 | |
| 2018-04-16 | Recursive bump for new fribidi dependency in pango. | wiz | 1 | -2/+2 | |
| 2018-04-14 | revbump after icu update | adam | 1 | -1/+2 | |
| 2018-04-09 | Updated lang/coq to version 8.7.2. | jaapb | 3 | -11/+37 | |
| This fixes a critical bug in the VM handling of universes, and adds various other minor fixes and improvements. | |||||
| 2018-03-12 | Recursive bumps for fontconfig and libzip dependency changes. | wiz | 1 | -2/+2 | |
| 2018-01-28 | Bump PKGREVISION for gdbm shlib major bump | wiz | 1 | -1/+2 | |
| 2018-01-22 | Corrected PLIST for lang/coq | jaapb | 1 | -3/+2 | |
 |
index : pkgsrc | |
| [no description] | Dyson |
| summaryrefslogtreecommitdiff |