CoqIDE on Windows does not report error if "Compile Buffer fails"

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#3991
From: @MSoegtropIMC
Reported version: 8.5
CC: @gares, @MSoegtropIMC

[coqbot]

Comment author: @MSoegtropIMC

Dear Coq team,

CoqIde 8.5-beta1 does not report an error if a compile buffer fails. As far as I can tell, this happens for any error, so I did not supply a sample.

Best regards,

Michael

[coqbot]

Comment author: @gares

I have to admit that I did not even know this feature existed ;-)

But here I see a (temporary) message in the bottom bar.

Is this also broken on windows? Or you were expecting a red
error in the output window (that would make sense...) and
you missed it?

If so I will turn the bug into a feature request.

[coqbot]

Comment author: @MSoegtropIMC

Dear Enrico,

on Windows I don't see any difference between a succesfull and a failed compile, not even a temporary message in the status bar.

With 8.4, in the case of an error the errors are shown in the bottom right message area and a message is shown in the status bar. On a successfull compile I get a message in the status bar. On 8.5 neither seems to work.

Best regards,

Michael

[coqbot]

Comment author: @gares

Looks like async-io on pipes does not work on Windows (this is also why I use sockets for proof workers).

8.4 used synchronous io there, since commit 6254115

I guess we could just take the old code and put an if around it.

[coqbot]

Comment author: @Zimmi48

I cannot reproduce the bug in Coq 8.5pl2 on Linux.
I get both the temporary message in the status bar and a more complete description in the message window, such as:

Compilation output:

File "/home/theo/test.v", line 2, characters 2-8:
Error: The reference trival was not found in the current environment.

Can we mark this bug as fixed or is there still a problem on Windows (in Coq 8.5pl2)?

[coqbot]

Comment author: @MSoegtropIMC

Dear Théo,

as fa as I know this problem always existed only on Windows. And it doesn't seem to be fixed there in 8.5pl2. When I create a file with an error, save it and compile it, I just get:

Running: coqc -I "C:\TEMP" "C:\TEMP\Test.v" 2>&1

in the message buffer, but nothing else.

Best regards,

Michael

[coqbot]

Comment author: @Zimmi48

Yes, Enrico just explained that to me. Sorry for the noise :S