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
On Windows, closing a socket no longer risks stopping the program. A socket finalized while
the event loop was about to wait on it made the loop’s wait fail, and the program ended with
INTERNAL PANIC: event loop poll failed: … not a socket (os error 10038); the loop now waits
again without it, as it always did on Linux and macOS.
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.