The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi Roger,

Thanks for following up. In this case, the Unicode input issue is a
bug that has already been noticed and very recently reported and
fixed. So this annoyance will disappear in 8.10.1.

As for the URL that you reported not working, we will fix this. It is
a consequence of a recent change of Coq's web server. Please bear with
us, as it might not be immediate.

Regarding the other problems you reported, I don't have the same
problems here, so they might be Windows-specific. If some other
Windows user can confirm this and open issues, that would be great.

Regards,
Théo

Le jeu. 10 oct. 2019 à 11:00, Roger Witte 
<Roger.Witte AT dft.gov.uk>
 a écrit :
>
> Also it appears the my earlier allegation that the (excellent!) latex to 
> Unicode function in coqide stopped working after so long was false.  The 
> issue was that the feature only works at the last character in the buffer 
> (a nuisance but acceptable). It was being killed by trailing whitespace.
>
>
>
> Regards
>
> Roger
>
> From: Roger Witte
> Sent: 09 October 2019 20:06
> To: 
> coq-club AT inria.fr
> Subject: Re: [Coq-Club] Coq 8.10.0
>
>
>
> Thanks for your comments, Theo.
>
>
>
> coq.inria.fr/distrib/V8.10.0/refman
>
> coq.inria.fr/distrib/V8.10.0/stdlib
>
>
>
> Help About CoqIDE website link goes Failed to execute helper program 
> (Invalid argument)
>
>
>
> By the way, opening \coq\lib\coq\theories\Init\Prelude.v causes coqidetop 
> died badly.
>
>
>
> Sorry I didn't spot any of the betas. I'll try to pay more attention in 
> future.
>
>
>
> Cheers
>
> Roger
>
> ________________________________
>
> From: Théo Zimmermann 
> <theo.zimmi AT gmail.com>
> Sent: Wednesday, 9 October 2019 17:25
> To: Coq Club 
> <coq-club AT inria.fr>
> Subject: Re: [Coq-Club] Coq 8.10.0
>
> Hi,
>
> > I saw the announcement on the web site yesterday evening and tried a 
> > download.  I will download again this evening in case you have made fixes 
> > overnight.
>
> Don't bother. Once a version has been uploaded with a given version
> number, it won't ever change. That's a basic rule of release
> management. It is unfortunate that you did not try any of the beta
> versions. These versions are reasonably stable and are precisely
> intended to gather user feedback before we commit on a final release.
>
> >         -       The help menu is broken: The links to the reference 
> > manual and library documentation go to bad addresses, as does the link to 
> > coq home from the about dialog.
>
> Could you please tell us which addresses these are? This can hopefully
> get fixed without changing anything in CoqIDE.
>
> > If you can tell me how to raise a bug report without logging in to 
> > github, I will happily do so but I don't want to join github.
>
> We do not support any other method of reporting a bug officially.
> However, if the people who are working on maintaining CoqIDE and the
> new Unicode support see your message and are ready to interact to you
> via e-mail, these bugs could still be investigated and hopefully fixed
> for the next patch-level release (8.10.1).
>
> If someone else has similar problem and does not mind using GitHub,
> feel free to open an issue. I won't however open an issue myself to
> copy-paste these various problem reports because solving them would
> definitely require a feedback-loop / interaction with the reporter.
>
> Regards,
> Théo
>
> __________________________________________________________________________________________
> This email has originated from external sources and has been scanned by 
> DfT’s email scanning service.
> __________________________________________________________________________________________
>
> ________________________________
> The information in this email may be confidential or otherwise protected by 
> law. If you received it in error, please let us know by return e-mail and 
> then delete it immediately, without printing or passing it on to anybody 
> else.
> Incoming and outgoing e-mail messages are routinely monitored for 
> compliance with our policy on the use of electronic communications and for 
> other lawful purposes.