perf: build o.noexport from o.export instead of compiling from C code

[Rob23oba]

No description provided.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-09-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-30 12:20:30)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-09-30 12:20:31)

[Kha]

@Rob23oba I'm curious, what is the status here? I guess we would have to adjust lean-llvm to ship llvm-objcopy

[ydewit]

@Rob23oba I am assuming this pr will also simplify lakefile.lean? E.g.:

  ...
  nativeFacets := fun shouldExport =>
    if shouldExport then
      #[Module.oExportFacet, `module.oShimExportFacet]
    else
      #[Module.oNoExportFacet, `module.oShimNoExportFacet]

[Rob23oba]

I don't really know enough about lakefiles to be able to answer that question. But @Kha, to answer your question, I'm not sure I'm completely happy about how fast it is, it still takes a few seconds to go through all the files (process creation overhead?). Also, I'm not very familiar with the lake code base so it'd be nice if @tydeu could look over those changes.

[Kha]

I'm not sure I'm completely happy about how fast it is, it still takes a few seconds to go through all the files (process creation overhead?).

Well that's still something like an improvement of two orders of magnitude over the previous code, isn't it?

[tydeu]

@Rob23oba The general idea here looks good to me. Did you mean for the code to be ready for review? After looking at this PR again today, I realized that is not clear to me from the discussion who is waiting on who.

[Rob23oba]

Right, I guess I should add: before realizing that there was already a solution for this problem (llvm-objcopy) I wrote my own piece of code that could remove the section in question based on the specification at https://learn.microsoft.com/en-us/windows/win32/debug/pe-format. After realizing the existence of llvm-objcopy I then wrote this PR using it. But after I tested it locally I thought that it was actually still pretty slow (~30 files/sec) and that it might be faster to use my original attempt at writing it myself since it's literally just ~300 loc and would have less complexity than llvm-objcopy. So I tested using it instead for the stage0 build but then found that it wasn't much of a difference, so I decided at first not to put it in this PR. But later, I tested it again, this time modified to traverse the file tree itself. That got, well, mixed results. One time it felt like it took roughly as long as through the stage0 make file but another time it took just around 2 seconds... not sure what exactly was going on each time. So, in general, I'm a bit inconclusive if we should keep it as-is (with llvm-objcopy) or if we should instead use the piece of C code I wrote.

[tydeu]

@Rob23oba I would start with llvm-objcopy in this PR (since that already provides a significant speedup) and then potentially revamp it to more custom code (in a later PR) if that is shown to be a significant performance improvement. There is also a separate benefit to using a tool vendor by a third party rather than code we would need to maintain in the future.

[Rob23oba]

Alright then, I guess I'd be ready for a review then

[Kha]

I guess we would have to adjust lean-llvm to ship llvm-objcopy

This part is still outstanding, no? WIthout it, I assume this would have minimal impact for the average user