refactor: ignore borrow annotations at export/extern tricks

[hargoniX]

This PR places set_option compiler.ignoreBorrowAnnotation true in on to all export/extern
pairs. This is necessary because export forces all arguments to be passed as owned while extern
respects borrow annotations. The current approach to the export/extern trick was always broken
but never surfaced. However, with upcoming changes many export/extern pairs are going to be
affected by borrow annotations and would've broken without this.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-16 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. (2026-03-16 10:50:16)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-16 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. (2026-03-16 10:50:18)