c code generation at compile time

Stream: lean4

[Mac]

@Tomas Skrivan well Alloy does most of that and is very small, so I would suggest just look at its source code (in particular Alloy.C.Extension and Alloy.C.Command).

[Mac]

@Tomas Skrivan You can also find examples of defining custom attributes and extensions in the tests/leanpkg directory of the Lean 4 repo (e.g., user_attr).

[Tomas Skrivan]

Thanks a lot for the pointers!

[Arthur Paulino]

@Mac How are you envisioning the integration with lake? will it be generic enough to allow plugging in completely custom solutions?

[Mac]

@Arthur Paulino yeah, that is the hope. Essentially, I want to add the ability to define custom facets for modules that are also materialized when a module is built

[Arthur Paulino]

So @Mac just to make sure (double checking by asking in a different way), is it safe to assume that lake will be able to run custom Lean code before starting the build process?

[Arthur Paulino]

(Or at least is it safe that this is the solution you're aiming for: running custom Lean code before building)

[Mac]

@Arthur Paulino Yes! In fact, it can already do that! :grinning: Take a look at theextraDepTarget configruration option, it is run before its corresponding package is built.

[Mac]

The point of the planned module facet extension is to make it easier to run custom code per module, rather than having to manual build and manage the whole transitive import graph.

[Arthur Paulino]

Sweet! I saw the extraDepTarget config option earlier but I wasn't sure it was what I thought it was. The description says it's an target that should be built before the package, but it doesn't say anything about actually running the code. Also I noticed that alloy doesn't use it, so I'm confused by how you're doing it

[Mac]

Arthur Paulino said:

The description says it's an target that should be built before the package, but it doesn't say anything about actually running the code.

Building entails running code. :wink: Targets in Lake are just BuildM monads that run asynchronously.

Arthur Paulino said:

Also I noticed that alloy doesn't use it, so I'm confused by how you're doing it

A couple of reasons for this:

1. Alloy is very WIP (hence I had yet to promote it and only did so when it was relevant tot the discuss at hand,
2. Alloy doesn't need extra code run to build Alloy (the lean library) itself, hence it doesn't need to use extraDepTarget. It would however, like to add tot he build process of packages that use it.
3. I was waiting on coding some better Lake integration before sprucing up its build script.

[Mac]

Examples of using extraDepTarget in practice can be found in the mathport project (e.g., mathlib3port's lakefile.lean)

[Arthur Paulino]

Alright, thank you very much!!

[Tomas Skrivan]

@Mac I was playing around with Alloy and I'm wondering how do I actually execute my_add or that is not possible yet? And only the code generation is working now?

[Arthur Paulino]

@Tomas Skrivan are you using alloy as a dependency or playing around with it from within its directory?

[Tomas Skrivan]

From within it's directory. I just added #eval my_add 1.0 2.0 in the example code and it didn't work (not that surprised) But it is not clear to me how to set it up to actually run my_add

[Arthur Paulino]

I'm gonna finish the dishes and then I'm going to try it

[Sebastian Ullrich]

The initial post does not really explain the motivation here. What exactly is it you want to solve in C that you cannot solve in Lean?

[Arthur Paulino]

Tomas' idea (please correct me if I'm wrong) is to provide multiple backend options like CUDA, as long as there is a Kernel for it

[Arthur Paulino]

And the end goal is to have access to super optimized low level numerical implementations while still writing friendly Lean code

[Sebastian Ullrich]

Ok, I don't know the first thing about CUDA. Why is it necessary to translate whole terms to C instead of individual operations for it?

[Arthur Paulino]

My guess is that then we'd have to cover the whole API with atomic implementations instead of defining a rule for well formed expressions and then let the automation take care of the rest. Maybe this response explains better. It started with my approach to NumLean (which I'm going to keep rolling and learn as much as I can from it)

[Arthur Paulino]

Alright I couldn't figure out how to execute my_add either

[Mac]

Tomas Skrivan said:

Mac I was playing around with Alloy and I'm wondering how do I actually execute my_add or that is not possible yet? And only the code generation is working now?

'You can't execute extern declarations in the same module they are written in (this is a limitation of Lean). They have to be compiled to be compiled together with their native implementation into a shared library that is passed to --load-dynlib in the server to allow the interpret to execute them.

To your second question. Yeah, only code generation is working to some degree right now.

[Joe Hendrix]

@Sebastian Ullrich My own motivation is to be able to write a Lean DSL that lets me easily generate bindings to C functions with native interfaces. e.g., so I can invoke native crypto functions from within Lean without writing C glue code. This could be solved by a Lean module similar to the Haskell FFI declarations, but that code tended to be pretty clunky to write in Haskell. I think the Alloy approach could be a lot more readable.

[Tomas Skrivan]

@Sebastian Ullrich For what I want to do, the prime example is the 'saxpy' operation s*x+y where s is a scalar and x and y are vectors. If you implement scalar multiplication and addition separately then you have to traverse the memory twice, effectively writing two for loops. If you implement 'saxpy' directly you can do it with just one for loop and traverse the memory just once. However, I do not want to implement 'saxpy' and other BLAS functions by hand but I want to generate their fast implementations. I think Lean can allow me to do something very similar to expression templates as used in C++ libraries Eigen or Blaze.

[Arthur Paulino]

@Mac I'm trying to recreate your steps, passing Test.lean as an input

import LeanPreprocess

@[compile]
constant test : Float

def main : IO Unit := do
  IO.println "hi"

But it says:

Test.lean:1:0: error: unknown package 'Init'
Test.lean:4:16: error: unknown identifier 'Float'
Test.lean:4:16: error: unknown constant 'sorryAx'
Test.lean:6:11: error: unknown identifier 'IO'
Test.lean:6:11: error: unknown constant 'sorryAx'
error: file Test.lean has errors

[Arthur Paulino]

No matter what I put in Test.lean, it fails to be accepted as a input of Main.lean

[Mac]

@Arthur Paulino where are you writing this? What is LeanPreprocess?

[Arthur Paulino]

It's a POC package that I'm playing with. I'm gonna push it to github

[Mac]

@Arthur Paulino a program that runs the Lean elaborator also needs to have its LEAN_PATH set appropriately (i.e., to the path of the .olean files of the module it plans on using, including those of Lean proper), That error generally appears when LEAN_PATH is not set up properly.

[Arthur Paulino]

https://github.com/arthurpaulino/LeanPreprocess

[Arthur Paulino]

ah, I think I see it on your lakefile

[Arthur Paulino]

Whoa, it worked
Thanks!

[Mac]

@Arthur Paulino fyi, I just updated Alloy to use a newer Lean and the newer code pattern for doing this.

[Mac]

@Arthur Paulino also note that on the command line you can use lake env LeanPreprocess <args...> to have Lake automatically fill set LEAN_PATH with the olean directories of the working directory's project.

[Arthur Paulino]

@Mac do you know how to iterate over the declarations of an Environment that are marked with a certain attribute?

[Arthur Paulino]

I think I'm getting closer and closer

[Mac]

@Arthur Paulino myAttr.ext.getState env will get you a NameSet of the names of all the declarations with the attribute which you can iterate over as desired.

[Arthur Paulino]

is it possible to extract their implementations too?

[Mac]

@Arthur Paulino declarations in Lean have mean kinds of implementations (e.g., the original Syntax, the elaborated Expr of its ConstantInfo used in proofs, its compiled IR, the emitted C code from the IR, etc.). Which do you mean? For example, I use multiple of these elements in the C Emitter for Alloy.. The code is here.

[Arthur Paulino]

I'm trying something similar to what you did:

builtin_initialize implExt : MapDeclarationExtension Syntax ←
  mkMapDeclarationExtension `KArray --?????

def implExt.getLocalEntries (env : Environment) : Array (Name × Syntax) :=
  implExt.getState env |>.fold (init := #[]) fun a n s => a.push (n, s)

def extractCCode (leanFile : FilePath) : IO String := do
  let input ← IO.FS.readFile leanFile
  let (env, ok) ← Lean.Elab.runFrontend input Options.empty leanFile.toString `main
  if ok then
    for (declName, impl) in implExt.getLocalEntries env do
      IO.println s!"-----{declName} {impl}------"
    if kArrayCompileAttr.hasTag env `test then
      emitCCode env |>.toString
    else ""
  else
    throw $ IO.userError s!"file {leanFile} has errors"

But it's not printing anything on that for (declName, impl) in implExt.getLocalEntries env do

[Mac]

@Arthur Paulino a couple of comments:

1. You need to add things to the extension, where are you doing that?
2. builtin_initialize are only run in compiled code. Are you using this from an executable? If not, you need to use initialize. If you use initialize, the use of the extension (i.e., actually adding / getting state) has to be done in a separate module.

[Arthur Paulino]

This PR summarizes my current attempt: https://github.com/lecopivo/lean4-karray/pull/4/files
My current doubt is whether it's possible or not to extract the implementation of the function whose declaration is declName inside the emitCCode function, which also receives the Environment as a parameter.

[Arthur Paulino]

Hey @Mac , that error is happening again, but this time I have everything set in the examples script (here).

This is the error:

examples/Test.lean:1:0: error: unknown package 'Init'
examples/Test.lean:3:41: error: unknown identifier 'Float'
examples/Test.lean:3:41: error: unknown constant 'sorryAx'
examples/Test.lean:3:61: error: expected command
examples/Test.lean:5:11: error: unknown identifier 'IO'
examples/Test.lean:5:11: error: unknown constant 'sorryAx'
examples/Test.lean:6:13: error: expected token

[Arthur Paulino]

And I have no idea why this is happening because I tried to mirror what is here, which works fine

[Mac]

@Arthur Paulino you are not using Lean.initSerachPath correctly -- it should be run once as Lean.initSearchPath (<- Lean.findSysroot?)

[Arthur Paulino]

Nice! But for some reason kArrayCompileAttr.ext.getState env |>.toList is an empty list

[Arthur Paulino]

And Test.lean has this definition:

@[karray_compile c_test] def test (a b : Float) : Float := a + b

[Arthur Paulino]

Aha, this is the culprit:

afterSet := fun declName _ => do
let env ← ofExcept $ addExtern (← getEnv) declName
setEnv env