redex.py: fix binary autodetection

[GunniBusch]

Summary

• factor redex binary lookup into find_redex_binary() so validation and execution share the same autodetection path
• allow validation to accept an autodetected redex-all from PATH or a bundled binary next to redex.py
• add focused tests for autodetected and missing binary cases

Why

Validation previously rejected runs without --redex-binary even though runtime already supported autodetecting the binary.

Validation

• python3 test/test_redex_args.py
• python3 -m py_compile redex.py test/test_redex_args.py

[meta-codesync]

@xuhdev has imported this pull request. If you are a Meta employee, you can view this in D101099802.

[xuhdev]

What's the purpose of this line?

[GunniBusch]

To find the redex-all file in the same directory if not given via flag. It would fail before reaching run-binary

[xuhdev]

This specifically requires --redex-binary argument to be passed, see the line right below:

raise argparse.ArgumentTypeError("Requires --redex-binary argument")

[GunniBusch]

Yup, and if the new function doesnt find the binary, it will set it to null. This means, it will got to the exception raising. But if it found one, it sets the arg value and bascaily dies the sea was setting the flag to a value.

why? because in your docs, you say somewhere that you need to either set the flag or have it in the same directory.

This is already the case, but because the check for that previously happens after validating the flags.

So currently (ie in the current main branch) you check for the binary in the same directory already here

redex/redex.py

Lines 237 to 244 in b342673

	def run_redex_binary(
	state: State,
	exception_formatter: ExceptionMessageFormatter,
	output_line_handler: typing.Optional[typing.Callable[[str], str]],
	) -> None:
	if state.args.redex_binary is None:
	state.args.redex_binary = shutil.which("redex-all")

But this (run_redex) is never called if args.redex_binary is None , because raise argparse.ArgumentTypeError("Requires --redex-binary argument") is thrown before. (Because validate_args is run before run_redex, which raises that exception if state.args.redex_binary is None )

redex/redex.py

Lines 1815 to 1816 in b342673

	validate_args(args)
	with_temp_cleanup(lambda: run_redex(args), args.always_clean_up)

So what I did, I basically removed the check logic from run_redex, put that into find_redex_binary, and set args.redex_binary to the return value of said function, inside validate_args. I also did this in run_redex to not mix refactor with fix in this pr

[xuhdev]

Where did you see "you say somewhere that you need to either set the flag or have it in the same directory."? Is this from the Windows context in the installation page?

Bundling the redex-all binary with the python scripts is not supported on Windows. Manually copy the binary into the same directory as redex.py and use redex.py that way, or ensure that redex.py is called with the --redex-binary parameter:

Because this is a behavior change, I just wanna make sure if you see it somewhere in doc, the doc is kept in sync.

[GunniBusch]

yes, from the windows steps.

[meta-codesync]

@xuhdev merged this pull request in 6b6d942.