Generated code no longer records where a Lake dependency sits on the machine that generated
it. A dependency required by path was written as a path climbing out of the project
(../../shared/formal/Shared/Urn.lean) in source comments, sources.json, manifest.json,
__meta and build-info.json; every Lake dependency is now written <package:NAME>/…, as one
fetched with git already was. The packages lungo generate writes name the project’s own files
relative to the Lean project, not to the output directory, and a Cargo build whose Lean project
lies outside the package writes it by its package too. Outputs generated by an earlier release
are regenerated once.
The runtime
A socket finalized while the event loop is waiting on it no longer stops the program. On
macOS the program stood still for good, with the closing thread and the loop each waiting for
the other; on Windows it ended with INTERNAL PANIC: event loop poll failed: … not a socket (os error 10038). A finalized socket is now closed by the event loop once its wait returns,
as libuv closes a handle, and never while the loop is waiting on it.
Generated code for Rust
The handler trait generated for an async facility no longer fails a crate’s
cargo clippy -- -D warnings: it allows Clippy’s lints, as the rest of the generated code
does.
Building lungo
On a Windows MSVC target, lungo’s workspace builds and tests: the comparison of PureRust with
Lean’s native backend, which needs a *-windows-gnu target (LNG0104), is left out there with
a build warning that says so, rather than failing the build.