Gpick is an advanced color picker and palette editing tool.
Main features
* Magnification and mouse pointer control with keyboard.
* Automatic color name assignment.
* Export to following formats:
* Inkscape/Gimp Palette (*.gpl)
* Adobe Swatch Exchange (*.ase)
* Alias/WaveFront Material (*.mtl)
* Cascaded Style Sheet (*.css)
* Hyper Text Markup Language (*.html)
* Customizeable text file
* Import from following formats:
* Inkscape/Gimp Palette (*.gpl)
* Adobe Swatch Exchange (*.ase)
* Customizeable text file
* Oversampling with five falloff types:
* Multiple pixel values are averaged to help picking
colors from sources with noise, patterns and etc,
where each pixel is different and overall color is
produced by different amounts of particular color.
* Palette from image.
* Color scheme creation tools.
* Mix two or more colors using variable number of steps
and different mixing types.
* Lightness and/or saturation variations.
* Harmonious colors.
- cupsfilters.drv: Corrected cupsFilter entry for the "Generic
IPP Everywhere Printer".
- driverless: Fixes on the man page
- driverless: Do not error-exit (non-zero status) when run by
CUPS as backend or PPD generator when no driverless printer
is found or Avahi not running. When run from thr command
line, exit status is the same as of ippfind.
- imagetoraster: Removed (incomplete) PWG Raster support. For
PWG Raster output we let the rastertopwg filter from CUPS do
the finalization (mainly adding white pixels at the borders
to get a full-page bitmap).
- imagetoraster: Fixed several bugs in the calculation of the
page geometry
- libcupsfilters: If the IPP-polled printer has the
"sides-supported" attribute, determine the need of a
"Duplex" option solely whether the attribute has a
"two-sided-long-edge" choice and ignore the "duplex"
parameter of the ppdCreateFromIPP() function call. This lets
the more precise information coming from the IPP query
always be preferred against information from the Bonjour
record.
- driverless: When listing printers let the device ID contain
"AppleRaster" (for Apple Raster printers) and "PWGRaster"
(for IPP Everywhere printers) in the "CMD" field.
- driverless: Added "-T 3" to the ippfind command line. This
makes ippfind search the Bonjour broadcasts for up to 3
seconds when searching for IPP printers, raising the
reliability in finding all of them
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.
===== 2.8.3 (2016-11-04) =====
* Features/Changes
** Runtime: complete support for 4.04
* Bug fixes
** Compiler: fix order of javascript files
** Compiler: fix Javascript lexer (newline inside strings)
** Compiler: fix bug in closure generation
** Compiler: fix regression in closure generation (introduced in 2.8) (#531)
** Compiler: fix code generation when static evaluation is disabled
===== 2.8.2 (2016-09-10) =====
* Features/Changes
** Lib: add Dom_html.Keyboard_code & Dom_html.Keyboard_key (Corwin de Boor)
** Misc: update lib and runtime to work better with non browser environment
** Misc: initial support for 4.04
* Bug fixes
** Compiler: fix js output for x - -1
** Compiler: fix parsing of annotations in the runtime
** Compiler: fix javascript minifier
** Compiler: various fixes for separate compilation.
pre-4.03 versions of OCaml can use the uchar library. Given that pkgsrc
uses 4.04 now, this library will always be empty, but it is needed for
dependency purposes.
===== 6.1 (2016-12-20) =====
* Remove redundant dependency on calendar
* Permit client routing to "./"
* -y parameter for eliom-distillery (do not ask)
* Eliom_client: do not execute onload after OCaml services
* Permit suffix params in Eliom_service.create_attached_post
===== 6.0 (2016-12-08) =====
* Improve Eliom_service and Eliom_registration APIs using GADTs
* Implement client-side services, useful for mobile apps. This includes
** client-side service registration (Eliom_registration)
** client-side service routing (Eliom_client.change_page_uri)
* Transition to PPX internally
* Compatibility with
** OCaml 4.03.0 and 4.04.0
** Js_of_ocaml 2.8.2 and newer
** TyXML 4.0 and newer
* Various bugfixes and improvements
* PostgreSQL Ocsipersist backend
* Compatibility with TyXML 4.0.x
* Export OpenSSL options through configuration file
* Various small fixes and improvements
* Fix handling of comments in the ppx.
* Fix printing of utf8 in attributes.
* Properly flush ppx errors. This bug was causing some blank error messages.
* Fix handling of whitespaces in <select> in the ppx.
* Remove -ansi flag to be compatible with OCaml 4.04 (thanks Mark Shinwell, ).
* Use accessor functions for X509_STORE_CTX.
* Change CLIBS order to allow static linking.
github tag, not a 'proper' release, but unfortunately this was needed for
compatibility reasons with other packages. The changelog has not been
updated upstream.
Batteries 2.5.3 synchronizes library functions with OCaml 4.04+beta2,
and will hopefully be an extension of the upcoming OCaml 4.04 release.
- Compatibility with OCaml 4.04.
5e63a9a756f
(Gabriel Scherer)
