Need help with compiling extra .c file with Lake

Stream: new members

[Yuri]

I am using Lean (version 4.7.0, aarch64-apple-darwin, commit 6fce8f7d5cd1, Release).

Consider a simple lake project: lake new MyLibrary lib:

MyLibrary
├── MyLibrary
│   └── Basic.lean
├── MyLibrary.lean
├── lakefile.lean
└── lean-toolchain

And lakefile.lean:

import Lake
open Lake DSL

package «MyLibrary» where
  -- add package configuration options here

@[default_target]
lean_lib «MyLibrary» where
  -- add library configuration options here

I would like to create a new file: MyLibrary.c along side MyLibrary.lean and have Lake compile and link it with all the other generated .c files.

Based on an initial search, I found out about library_facet and module_facet, which seems to be the way to go. But how?

Could someone get me started?

thanks,

[Yuri]

I realized that I should have posted this in the lean4 channel?

[Yuri]

Yuri de Wit said:

I can create a library_facet and I can explicitly invoke it using lake build MyLibrary:test:

library_facet test lib : Unit := do
  IO.println "test!"
  logInfo "test!!"
  return .nil

How can I make this run automatically when the the library is built? Adding the facet does not work.

  defaultFacets := #[`test]
  nativeFacets := #[`test]

Or maybe I misunderstand what is the purpose of a library_facet?