The Coq mailing list

[Richard Ford <richardlford AT gmail.com>]

Thanks for your suggestion. The reason I thought it was related was that this might be something that could be implemented for the 8.13 release. I'll add an issue, and I suppose if I really want it, I should implement and submit a pull request.

Rich

On Wed, Dec 16, 2020 at 2:24 PM Théo Zimmermann <theo AT irif.fr> wrote:

Hi Richard,

It's been received, but there isn't really any process to treat
feedback in the form of e-mails, so it probably happened that all the
people that could answer were too busy at the time they read it or
something like that.
If you want to avoid your feedback being lost, please use our issue
tracker system instead: https://github.com/coq/coq/issues

Thanks,
Théo

Le mer. 16 déc. 2020 à 16:59, Richard Ford <richardlford AT gmail.com> a écrit :
>
> Hi. It's been 8 days since I sent the above email and I've not seen a response. Did this get lost?
>
> Thanks.
>
> On Tue, Dec 8, 2020 at 6:06 PM Richard Ford <richardlford AT gmail.com> wrote:
>>
>> The documentation of Primitive Integers, Primitive Floats, and Primitive Arrays makes the point that, when extracting to OCaml, that implementations of Uint63, Float64, and PArray are not provided, but that the user must supply them. But it also points out that the Coq kernel has implementations of all of these. That being the case, could the building and installation of Coq be modified so that the binary form of these libraries is made available for those that would like to compile and execute Coq programs that use these features and are extracted to OCaml? That would save the user the work of extracting these from the Coq sources and having to rebuild them for each Coq version.
>>
>> Thanks,
>>
>> Richard L Ford
>>
>>
>>
>> On Tue, Dec 8, 2020 at 3:13 PM Enrico Tassi <Enrico.Tassi AT inria.fr> wrote:
>>>
>>> Dear Coq users,
>>>
>>> The Coq development team is proud to announce the immediate
>>> availability of Coq 8.13+beta1:
>>>
>>> https://github.com/coq/coq/releases/tag/V8.13+beta1
>>>
>>> The full list of changes is available at the following address
>>>
>>> https://coq.github.io/doc/v8.13/refman/changes.html#version-8-13
>>>
>>> We encourage our users to test this beta release, in particular:
>>>
>>> - The windows installer is now based on the Coq platform: This
>>>   greatly simplifies its build process and makes it easy to add
>>>   more packages. At the same time this new installer was only
>>>   tested by two people, so if you use Windows please give us
>>>   feedback on any problem you may encounter.
>>>
>>> - The notation system received many fixes and improvements, in
>>>   particular the way notations are selected for printing changed:
>>>   Coq now prefers notations which match a larger part of the term to
>>>   abbreviate, and takes into account the order in which notations are
>>>   imported in the current scope only in a second instance.
>>>   The new rules were designed together with power users, and tested
>>>   by some of them, but our automatic testing infrastructure for
>>>   regressions in notation printing is still weak. If your Coq library
>>>   makes heavy use of notations, please give us feedback on any
>>>   regression.
>>>
>>> The 8.13.0 release is expected to occur about one month from now.
>>>
>>> Best,
>>> --
>>> Enrico Tassi, for the Coq dev team
>>>
>>>
>>>
>>>