Fix miri.bat to not exit unconditionally

[cgettys-microsoft]

#3703 has a small typo causing it to regress ./miri.bat to not working at all.

This PR fixes it. Tested on Windows 11, with stable toolchain missing as well as installed.

./miri toolchain
error: toolchain 'stable-x86_64-pc-windows-msvc' is not installed
Failed to build miri-script. Is the 'stable' toolchain installed?

Closes #3714

[RossSmyth]

I implemented it the same as you first, then thought about what I wrote about in my review and changed it to what it is now. But I did not think that & and && would have different precedence so I didn't check it again.

[cgettys-microsoft]

Didn't occur to me, either.

|| (echo Failed to build miri-script. Is the 'stable' toolchain installed? & exit /b)

as you suggested on Zulip also works. Not sure which is "better" stylistically or functionally, so I'll defer to you or others with better batch knowledge on what we want to do to fix it.

[RalfJung]

I have no batch knowledge :) so I am fine with whatever the Windows Gurus agree upon here.

[RalfJung]

But my feeling is that explicit is better than implicit, so the version with parentheses seems more appealing to me. That's also why I used parentheses in the Unix Shell version.

[cgettys-microsoft]

Seems like a reasonable reason to go that way - switched to @RossSmyth's version (tested locally again to be careful).

[RossSmyth]

As I explained in the review comment, the version with parenthesis and & covers an edge case that the && version does not. So just to cover our butt it is probably better.

[RossSmyth]

LGTM though

[cgettys-microsoft]

@rustbot ready

[RalfJung]

So does the single & here mean sequencing now? Elsewhere you said it means "fork", I guess similar to what it means in Unix - but that would be the wrong meaning here as it would run " echo" and "exit" in parallel, which is not what we want? Or did I misunderstand?

[RalfJung]

I do not know which review comment you are referring to, @RossSmyth. Please always add a link when referring to other comments like that :)

[Cgettys]

So does the single & here mean sequencing now? Elsewhere you said it means "fork", I guess similar to what it means in Unix - but that would be the wrong meaning here as it would run " echo" and "exit" in parallel, which is not what we want? Or did I misunderstand?

I was wrong about the meaning of & in batch / cmd... I'm rusty on it (ha)- but I believe @RossSmyth's explanation is right.

I'm having a hard time finding any decent official docs for batch files. Powershell is much better documented 😞.
Both I believe are the call / chain operator.
I believe && is conditional (on the exit code of the previous) but & is not. And they may have different precedence vs the || operator as well.
Effectively the previous version was equivalent to:

cargo +stable build %CARGO_EXTRA_FLAGS% -q --target-dir %MIRI_SCRIPT_TARGET_DIR% --manifest-path %0\..\miri-script\Cargo.toml ||   echo Failed to build miri-script. Is the 'stable' toolchain installed? 

exit /b

Which was definitely not what we wanted.

I'll see if I can find a better reference.
Honestly, if I get a chance, I may just create a .ps1 / Powershell version in the future - it's much better documented and I actually know it well enough to speak to its behavior more...

[Cgettys]

I do not know which review comment you are referring to, @RossSmyth. Please always add a link when referring to other comments like that :)

I can't find it either. I thought he meant the discussion in Zulip earlier today, but that doesn't quite make sense in context? Dunno

[Cgettys]

Here's the not-relevant powershell docs for the powershell version of those operators. But Batch / cmd.exe != powershell.
Precedence / operators
The source of my confusion, which I don't think is what & means in a .batch file: background operator

[Cgettys]

Ok, finally found the official, 1st party docs... buried in a generic page instead of a nicely searchable
one.
Using multiple commands and conditional processing symbols

& [...]
command1 & command2
Use to separate multiple commands on one command line. Cmd.exe runs the first command, and then the second command.

&& [...]
command1 && command2

Use to run the command following && only if the command preceding the symbol is successful. Cmd.exe runs the first command, and then runs the second command only if the first command completed successfully.

|| [...]
command1 || command2
Use to run the command following || only if the command preceding || fails. Cmd.exe runs the first command, and then runs the second command only if the first command did not complete successfully (receives an error code greater than zero).

( ) [...]
( command1 & command2)
Use to group or nest multiple commands.

This still doesn't make sense to me, unless there's operator precedence involved as we suspected
I'd kind of have expected
a || b & c
to have been evaluated as
(a || b) & c
(barring some sort of operator precedence going on)
which is the same as

(a || b)
c

and since c is exit, we didn't run miri-script.
So I don't quite see why the && would have fixed it in that case (as b being echo in (a || b) presumably would guarantee that that expression would have exited with code 0.

But big picture, with the appropriate parentheses to force b and c to run in the failure case, together, either & or && would work, and & is a bit more foolproof because if echo somehow fails, we still should run exit / should not try to run miri-script if the toolchain is missing.

Hope that answers the question @RalfJung.

[RalfJung]

Okay, thanks for checking!
@bors r+

Honestly, if I get a chance, I may just create a .ps1 / Powershell version in the future - it's much better documented and I actually know it well enough to speak to its behavior more...

I'm fine with replacing the bat file by a ps1 file, happy to leave that decision to Windows-using folks. I'd prefer not to have both a bat file and a ps1 file though.

[bors]

📌 Commit b551931 has been approved by RalfJung

It is now in the queue for this repository.

[bors]

⌛ Testing commit b551931 with merge 0a8e39b...

[bors]

☀️ Test successful - checks-actions
Approved by: RalfJung
Pushing 0a8e39b to master...

[RossSmyth]

I do not think this semantically correct for all failure cases.

If the cargo command fails we want the statement to be post-dominated by the exit /b statement. But the current implementation means "only exit if the echo command succeeds."

Basically if echo ever has a write error it will not exit, so I would recommend my Zulip suggestion so that it will always exit in the error case:

Suggested change

	|| echo Failed to build miri-script. Is the 'stable' toolchain installed? && exit /b
	|| (echo Failed to build miri-script. Is the 'stable' toolchain installed? & exit /b)

[RossSmyth]

Oh oops, I never actually finalized the review. I was referring to a comment only I could see. Posted it just for posterity

[RossSmyth]

Okay, thanks for checking! @bors r+

Honestly, if I get a chance, I may just create a .ps1 / Powershell version in the future - it's much better documented and I actually know it well enough to speak to its behavior more...

I'm fine with replacing the bat file by a ps1 file, happy to leave that decision to Windows-using folks. I'd prefer not to have both a bat file and a ps1 file though.

The problem with .ps1 files is that by default on Windows, PowerShell scripts are not able to be executed. And some people (such as on corporate computers) cannot configure them to be executable. I think PowerShell is decent, but for scripts to be executable by arbitrary people bat files are the only real choice, or else you lock out people who are unable to run PowerShell scripts.

[cgettys-microsoft]

Okay, thanks for checking! @bors r+

Honestly, if I get a chance, I may just create a .ps1 / Powershell version in the future - it's much better documented and I actually know it well enough to speak to its behavior more...

I'm fine with replacing the bat file by a ps1 file, happy to leave that decision to Windows-using folks. I'd prefer not to have both a bat file and a ps1 file though.

The problem with .ps1 files is that by default on Windows, PowerShell scripts are not able to be executed. And some people (such as on corporate computers) cannot configure them to be executable. I think PowerShell is decent, but for scripts to be executable by arbitrary people bat files are the only real choice, or else you lock out people who are unable to run PowerShell scripts.

That's a fair reason. But then again - is ./miri.bat used outside of dev? if not, there are very few devs who don't have the ability to run powershell, I'd think