head 1.8; access; symbols pkgsrc-2022Q1:1.7.0.10 pkgsrc-2022Q1-base:1.7 pkgsrc-2021Q4:1.7.0.8 pkgsrc-2021Q4-base:1.7 pkgsrc-2021Q3:1.7.0.6 pkgsrc-2021Q3-base:1.7 pkgsrc-2021Q2:1.7.0.4 pkgsrc-2021Q2-base:1.7 pkgsrc-2021Q1:1.7.0.2 pkgsrc-2021Q1-base:1.7 pkgsrc-2020Q4:1.6.0.8 pkgsrc-2020Q4-base:1.6 pkgsrc-2020Q3:1.6.0.6 pkgsrc-2020Q3-base:1.6 pkgsrc-2020Q2:1.6.0.4 pkgsrc-2020Q2-base:1.6 pkgsrc-2020Q1:1.6.0.2 pkgsrc-2020Q1-base:1.6 pkgsrc-2019Q4:1.5.0.10 pkgsrc-2019Q4-base:1.5 pkgsrc-2019Q3:1.5.0.6 pkgsrc-2019Q3-base:1.5 pkgsrc-2019Q2:1.5.0.4 pkgsrc-2019Q2-base:1.5 pkgsrc-2019Q1:1.5.0.2 pkgsrc-2019Q1-base:1.5 pkgsrc-2018Q4:1.4.0.10 pkgsrc-2018Q4-base:1.4 pkgsrc-2018Q3:1.4.0.8 pkgsrc-2018Q3-base:1.4 pkgsrc-2018Q2:1.4.0.6 pkgsrc-2018Q2-base:1.4 pkgsrc-2018Q1:1.4.0.4 pkgsrc-2018Q1-base:1.4 pkgsrc-2017Q4:1.4.0.2 pkgsrc-2017Q4-base:1.4 pkgsrc-2017Q3:1.3.0.8 pkgsrc-2017Q3-base:1.3 pkgsrc-2017Q2:1.3.0.4 pkgsrc-2017Q2-base:1.3 pkgsrc-2017Q1:1.3.0.2 pkgsrc-2017Q1-base:1.3 pkgsrc-2016Q4:1.2.0.4 pkgsrc-2016Q4-base:1.2 pkgsrc-2016Q3:1.2.0.2 pkgsrc-2016Q3-base:1.2 pkgsrc-2016Q2:1.1.0.4 pkgsrc-2016Q2-base:1.1 pkgsrc-2016Q1:1.1.0.2 pkgsrc-2016Q1-base:1.1; locks; strict; comment @# @; 1.8 date 2022.06.21.02.21.22; author dholland; state dead; branches; next 1.7; commitid 33KtZWGt0p2nMQID; 1.7 date 2021.02.09.22.37.43; author dholland; state Exp; branches; next 1.6; commitid bnwlxAN6i9IVq5HC; 1.6 date 2020.01.24.15.54.48; author jaapb; state Exp; branches; next 1.5; commitid 45tw63aXsHRzwXTB; 1.5 date 2019.03.06.09.28.23; author jaapb; state Exp; branches; next 1.4; commitid RAvgSdfNiAVRNheB; 1.4 date 2017.11.03.11.20.28; author jaapb; state Exp; branches; next 1.3; commitid woS4QhJBeqqI6AdA; 1.3 date 2016.12.30.13.23.06; author jaapb; state Exp; branches; next 1.2; commitid q0OxTE2Kw94YG0Az; 1.2 date 2016.07.02.10.17.18; author jaapb; state Exp; branches; next 1.1; commitid lOMIBDGhyG7MtJcz; 1.1 date 2016.02.06.16.08.36; author jaapb; state Exp; branches; next ; commitid TcyL81NHcysY8STy; desc @@ 1.8 log @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. @ text @$NetBSD: patch-Makefile.common,v 1.7 2021/02/09 22:37:43 dholland Exp $ Use BSD_INSTALL_* --- Makefile.common.orig 2020-12-11 08:46:08.000000000 +0000 +++ Makefile.common @@@@ -90,8 +90,8 @@@@ DYNOBJ:=.cmo DYNLIB:=.cma endif -INSTALLBIN:=install -INSTALLLIB:=install -m 644 +INSTALLBIN:=${BSD_INSTALL_SCRIPT} +INSTALLLIB:=${BSD_INSTALL_LIB} INSTALLSH:=./install.sh MKDIR:=install -d @ 1.7 log @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 @ text @d1 1 a1 1 $NetBSD: patch-Makefile.common,v 1.6 2020/01/24 15:54:48 jaapb Exp $ @ 1.6 log @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. @ text @d1 1 a1 1 $NetBSD: patch-Makefile.common,v 1.5 2019/03/06 09:28:23 jaapb Exp $ d5 1 a5 1 --- Makefile.common.orig 2018-10-31 12:53:51.000000000 +0000 d7 1 a7 1 @@@@ -83,8 +83,8 @@@@ DYNOBJ:=.cmo @ 1.5 log @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. @ text @d1 1 a1 1 $NetBSD$ d4 1 @ 1.4 log @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 @ text @d4 1 a4 1 --- Makefile.common.orig 2017-10-16 08:53:18.000000000 +0000 d6 1 a6 1 @@@@ -69,8 +69,8 @@@@ DYNOBJ:=.cmo d12 1 a12 1 +INSTALLBIN:=${BSD_INSTALL_PROGRAM} @ 1.3 log @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. @ text @d4 1 a4 1 --- Makefile.common.orig 2016-10-25 20:17:16.000000000 +0000 d6 2 a7 1 @@@@ -35,7 +35,7 @@@@ else d10 3 a12 2 INSTALLBIN:=install -INSTALLLIB:=install -m 644 @ 1.2 log @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 @ text @d4 1 a4 2 Compile with OCaml 4.03 --- Makefile.common.orig 2016-04-11 13:12:51.000000000 +0000 a14 9 @@@@ -231,7 +231,7 @@@@ endif LINKCMO:=$(CORECMA) $(STATICPLUGINS) LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) -IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/errors.cmo lib/spawn.cmo +IDEDEPS:=lib/clib.cma lib/errors.cmo lib/spawn.cmo IDECMA:=ide/ide.cma IDETOPLOOPCMA=ide/coqidetop.cma @ 1.1 log @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.) @ text @d4 2 a5 1 --- Makefile.common.orig 2015-12-16 23:44:44.000000000 +0000 d16 9 @