search

rust-lang / miri

An interpreter for Rust's mid-level intermediate representation
Apache License 2.0
4.16k stars 318 forks source link

Fix miri.bat to not exit unconditionally #3715

Closed cgettys-microsoft closed 4 days ago

cgettys-microsoft commented 5 days ago

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 commented 5 days ago

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 commented 5 days ago

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 commented 5 days ago

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

RalfJung commented 5 days ago

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 commented 5 days ago

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

RossSmyth commented 5 days ago

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 commented 5 days ago

LGTM though

cgettys-microsoft commented 5 days ago

@rustbot ready

RalfJung commented 5 days ago

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 commented 5 days ago

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 commented 5 days ago

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 :disappointed:. 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 commented 5 days ago

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 commented 5 days ago

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 commented 5 days ago

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 commented 4 days ago

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 commented 4 days ago

:pushpin: Commit b551931fad2d78efbb8d0f3b467faae740be9482 has been approved by RalfJung

It is now in the queue for this repository.

bors commented 4 days ago

:hourglass: Testing commit b551931fad2d78efbb8d0f3b467faae740be9482 with merge 0a8e39bf4525b468f3834b59895e812347f8938b...

bors commented 4 days ago

:sunny: Test successful - checks-actions Approved by: RalfJung Pushing 0a8e39bf4525b468f3834b59895e812347f8938b to master...

RossSmyth commented 4 days ago

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

RossSmyth commented 4 days ago

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 commented 4 days ago

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