I/R: support native Windows - #261
Open
DanielMidgley wants to merge 1 commit into
Open
Conversation
The daemon assumed POSIX and would not run under native Windows Python. Make it work there without WSL. Linux and macOS are unchanged: every platform branch is guarded by IS_WINDOWS / os.name (ISABELLE_PLATFORM_FAMILY in ML), and the new helpers are pass-throughs. Add ir/win_compat.py for the differences. The `isabelle` launcher is a Cygwin bash script that CreateProcess rejects (WinError 193), so run it through Isabelle's bundled bash, with Cygwin's bin on PATH and paths converted both ways — /cygdrive/ form for arguments in, Windows form for `isabelle getenv` values out. It also replaces os.killpg / start_new_session, guards SIGHUP, and forces UTF-8 stdio, since the locale codepage cannot encode the "●" in the status lines and killed startup with UnicodeEncodeError. Swap the AF_UNIX management console for an ephemeral localhost port plus a rendezvous file at the same path, leaving mgmt_socket_path() and discover_mgmt_sockets() untouched. That port is reachable by any local user, unlike a 0600 socket, so Windows clients must send a token and the file is ACL'd to the current user. Three protocol fixes: generate_token prefers IR_REPL_AUTH_TOKEN, minted by Python's CSPRNG since native Poly/ML cannot open /dev/urandom; SO_REUSEADDR is not set on Windows, where it also permits binding a port another process is actively listening on, so I/R announced a port it did not own and hung with no diagnostic; and line parsing tolerates the CRLF that Java's PrintWriter.println makes I/Q send, which failed every repl_* auth while repl_connect still reported success. Tested on Windows 11 / Isabelle2025-2 / CPython 3.12: standalone --daemon, I/Q --expect-ml, mgmt auth accept/reject, --kill-daemon. Not run on Linux locally; the existing I/R CI covers that.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description of changes:
Makes the I/R daemon run under native Windows Python (no WSL). Linux and macOS
behaviour is unchanged -- every platform branch is guarded by
IS_WINDOWS/os.name(ISABELLE_PLATFORM_FAMILYin ML), and the new helpers inir/win_compat.pyare pass-throughs on POSIX.What was broken on Windows:
isabelleis a Cygwin bash script →WinError 193on every subprocess call.Now run via Isabelle's bundled bash, with
/cygdrive/conversion forarguments going in and Windows form for
getenvvalues coming out.os.killpg/start_new_session/SIGHUPunavailable →terminate_tree(),SPAWN_KW, guarded signal registration.AF_UNIXnot exposed by CPython on Windows → the mgmt console uses anephemeral localhost port plus a rendezvous file at the same path. That port is
reachable by any local user, unlike a 0600 socket, so the Windows path adds a
token and a per-user ACL on the file.
●in the statuslines killed startup with
UnicodeEncodeError. Explicit UTF-8 reads + stdio./dev/urandom→generate_tokenprefersIR_REPL_AUTH_TOKEN, minted by Python's CSPRNG.SO_REUSEADDRon Windows also permits binding a port another process isactively listening on → I/R announced a port it did not own and hung with no
diagnostic. Not set there now.
PrintWriter.printlnsends CRLF → everyrepl_*call failed auth whilerepl_connect(which never authenticates) reported success. Line parsing isnow CRLF-tolerant.
Tested on Windows 11 / Isabelle2025-2 / CPython 3.12: standalone
--daemon, theI/Q
--daemon --expect-mlpath, mgmt console auth accept/reject,--kill-daemon.Not run on Linux locally.
ir/test_repl.pyis untouched and still POSIX-only (os.killpg), so this file still does not run on Windows.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.