fix: pass Lake module setup to highlighted extractor - #222
Conversation
3e0dad3 to
a1eb3e3
Compare
ejgallego
changed the title
c809243 to
feb86d0
Compare
ejgallego
changed the title
|
CI problems seem to be also present upstream, investigating. Otherwise this PR is ready for review. |
db5981c to
af2adcc
Compare
| -- Keep the old and modern facet implementations separate: their Lake job/trace APIs differ enough | ||
| -- that factoring the full body would force more compatibility shims. The setup-file behavior is | ||
| -- factored only at the argument level, where it does not expose old and modern Lake APIs to each | ||
| -- other. |
There was a problem hiding this comment.
This comment doesn't make much sense to me. Can you please clarify a bit?
The existing split is due to a change in Lake's bind, not a change introduced here.
There was a problem hiding this comment.
The comment is indeed bad and belongs to a previous version of this PR. Fixed, thanks.
| | _ => none | ||
|
|
||
| /-- | ||
| Whether this toolchain can run the FFI regression for the highlighted facet's Lake setup-file path. |
There was a problem hiding this comment.
Why do we version-gate here but feature-gate elsewhere?
af2adcc to
8ad177f
Compare
| #if defined(_WIN32) | ||
| #define SUBVERSO_FFI_EXPORT __declspec(dllexport) | ||
| #elif defined(__GNUC__) || defined(__clang__) | ||
| #define SUBVERSO_FFI_EXPORT __attribute__((visibility("default"))) | ||
| #else | ||
| #define SUBVERSO_FFI_EXPORT | ||
| #endif |
There was a problem hiding this comment.
Why do we need this macro?
There was a problem hiding this comment.
Good catch, thanks! This is necessary for cross-platform compat, but the LEAN_EXPORT macro does exactly this, when -DLEAN_EXPORTING is setup. Will amend.
| -- Feature-probe Lake's setup-file support instead of version-gating it, so older Lake keeps the | ||
| -- original extractor CLI while newer Lake passes the module setup file it already computes. |
There was a problem hiding this comment.
This reads like an LLM justifying a change it made during a session, rather than as a useful comment to help future readers understand the code. What about:
| -- Feature-probe Lake's setup-file support instead of version-gating it, so older Lake keeps the | |
| -- original extractor CLI while newer Lake passes the module setup file it already computes. | |
| -- Checks whether the current toolchain supports setup files. If not, adding them is a no-op. |
But perhaps it should be an error if not supported, so that users get more helpful messages?
There was a problem hiding this comment.
Thanks, will amend. I'd say we can keep the no-op, explicitly passing --setup to an unsupported extractor already produces an error through the compatibility fallback IIANM.
| -- The fixture's `lp_ffi_answer` symbol uses package-aware module names, so probe the corresponding | ||
| -- setup features rather than inferring them from the Lean version. |
There was a problem hiding this comment.
This also reads like an LLM changing course during development. What are package-aware module names? The comment itself really doesn't help me understand the code.
There was a problem hiding this comment.
"package-aware" names refers to the change in Lean 4.27; prior to Lean 4.27, a declaration named answer was looked up under the global native symbol l_answer. Newer Lean records the package ID from lake setup file. For package ffi, the same declaration becomes lp_ffi_answer.
I think the best fix here is to restrict this test to Lean >= 4.27 . If we'd like to test 4.25/4.26 we can add a new fixture.
There was a problem hiding this comment.
I'm looking into this in more detail, there is something about how #eval resolves native symbols which I still don't understand.
| -- artifacts or a previously-generated dependency source — those are managed below / kept warm. | ||
| copyRecursively project buildDir | ||
| (fun f => f != ".lake" && f != "no-mod" && f != "lake-manifest.json") | ||
| -- The prepared copy must run under the matrix/fixed toolchain, not under a fixture's checked-in |
There was a problem hiding this comment.
Can you elaborate a bit on what this means?
There was a problem hiding this comment.
This was ensuring the correct toolchain was selected for the test and not rewritten by lake. After review, I think the best is to eliminate the FFI special path and have it as an standard test. Will amend.
2 participants
Fix highlighted source extraction for modules whose Lake build context includes setup data, such as dynamic libraries.
The highlighted module facet now passes Lake's module setup file to
subverso-extract-modwhen Lake exposes one. The extractor loads that setup before elaboration, so extraction sees the same imports, options, plugins, import artifacts, dynamic libraries, and package metadata as the module build. Older Lake versions continue using the existing extractor arguments.This adds an FFI regression fixture that builds a dynamic library and checks
Ffi:highlighted. The fixture runs on Lean 4.27 and newer; setup files exist in some earlier module-system releases, but this fixture's extern#evalfails during the module build before SubVerso extraction runs there.Related: #221 , thanks to @kim-em for submitting the report and a preliminary fix.