c output file

Stream: general

[Matthew Weingarten]

I am trying to look at the C output file produced by lean4 compiler using the command

./lean --c=out.c test.lean

However even with simple examples like this test.lean file :

def main (n : List String) : IO UInt32 :=
do IO.println (toString n);
   pure 0

or

def const(x : Nat) : Nat := x

it merely displays "cannot extract code, module name of input file is no known", which I don't understand.

Running --make or --run works no issue. Appreciate any advice!

[Mario Carneiro]

I have not used lean 4, but I would start by trying to run some of the tests, mimicking the test_single.sh setup

[Mario Carneiro]

You might have to be in the right working directory

[Gabriel Ebner]

I believe the officially "supported" way to build lean4 code is to use the new leanmake tool, which also requires a specific directory structure. I don't believe there is any documentation (or even example projects) yet.

[Marc Huisinga]

the current server in the lean4 repo has a small compilation example: https://github.com/leanprover/lean4/tree/master/src/Lean/Server

[Matthew Weingarten]

Thanks for the replies, I still don't quite understand what is going wrong.
As far as I am aware the work in progress lean4 compiler generates a C file from a lean file.
in lean4/tests/plugin/ running bash test_single.sh Default.lean.c does output a c file Default.lean.c after running , but I cant reproduce results for an arbitrary .lean file, showing :

Cannot extract code, module name of input file not known

What am I missing?

[Wojciech Nawrocki]

@Matthew Weingarten Before trying to build anything at all manually, make sure that you've set up elan to automatically use Lean 4 like in these instructions. Then if you have Blah.lean in any child of the lean4/ directory (since this subtree is where elan will auto-switch to Lean 4), you can use leanmake +lean4 bin PKG=Blah LINK_OPTS=-rdynamic to build it.

As for the plugin, in lean4/tests/plugin bash test_single.sh SnakeLinter.lean works for me, but there doesn't seem to be any Default? Unless you added one?