Package decl with IO

Stream: lean4

[James Gallicchio]

Hi, I'm configuring the moreLinkArgs of a package declaration depending on the system configuration. Is that a bad idea? I know very little about building c++. Perhaps that's a bad idea/unnecessary and I should avoid it.

But if it's not a bad idea, how could I configure my lakefile to do so? The package def doesn't have IO access, so I think it's not really possible

[James Gallicchio]

(@Mac mainly -- sorry for the Thanksgiving ping, this is not particularly urgent)

[Mac]

James Gallicchio said:

Hi, I'm configuring the moreLinkArgs of a package declaration depending on the system configuration. Is that a bad idea? I know very little about building c++. Perhaps that's a bad idea/unnecessary and I should avoid it.

That is fine, you should just match sure you have a case for each relevant operating system (e.g., Windows, MacOS, Linux) and probably test the build on each in your GitHub CI.

James Gallicchio said:

But if it's not a bad idea, how could I configure my lakefile to do so? The package def doesn't have IO access, so I think it's not really possible

I had originally allowed a package declaration to perform IO, but I ended up removing it. The reason being you can achieve the same result through meta programming. That is, you can write a macro or elaborator that expands/elaborates to the value you want.

[James Gallicchio]

Ohh, that makes sense. Thanks, will give that a shot