The Coq mailing list

[Roger Witte <Roger.Witte AT dft.gov.uk>]

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.