zetzit / zz

πŸΊπŸ™ ZetZ a zymbolic verifier and tranzpiler to bare metal C
MIT License
1.6k stars 52 forks source link

Is there a way to emit C source code only? #60

Closed xxuejie closed 4 years ago

xxuejie commented 4 years ago

First of all, thanks for this, really great project!

I noticed that right now when we do zz build, it would generate the C code, then invoke a C compiler. The problem here, is that we are doing cross-compilation to RISC-V, hence we need a gcc that supports RISC-V. While I could of course set CC environment variable, I noticed zz hardcoded certain compiler flags that might not be supported well in different environments.

So the question now is: is there a mode that we can just use zz to emit the C code, the at a later stage manually compile the C source code to binary?

aep commented 4 years ago

Yes There's several ways to do what you want.

The "standard" one is to just set the CC environment variable to your C compiler.

CC=riscv-gcc zz build --release

The next option is to export to a different build system like cmake by using a cmake artifact type in zz.toml

Finally I can re-add the zz export command which really only emits C.

I'd welcome any feedback on your experience with using zz on riscv :)

xxuejie commented 4 years ago

Thanks for your quick response! Yes I've tried setting CC environment variable, the problem is there is just more than just CC that needs customization. In addition, our workflow doesn't complete when the binary is generated, we have to post-process it, so a custom build flow still exists.

I do recommend re-adding the zz export command back, but of course you know this project better than I do, and you might have other considerations :P

aep commented 4 years ago

Right. Export it is! You can temporarily work around that by just using the cmake artifact type

xxuejie commented 4 years ago

Hmm, I must've done something wrong, I tried the following config:

[project]
version   = "0.1"
name      = "ckb-zz-demo"
cincludes = [".", "src"]
artifacts = [
  { name = "main1", main = "main1.zz", type = "cmake" }
]

The build succeeds, but no C file has been produced:

$ zz build
$ tree target
target
β”œβ”€β”€ repos
β”‚Β Β  └── index
└── test
    β”œβ”€β”€ c
    β”œβ”€β”€ include
    β”‚Β Β  └── zz
    β”‚Β Β      └── ckb_zz_demo
    └── zz
        └── ckb_zz_demo_main1.c.parsecache

7 directories, 2 files

Maybe I've configured something wrong here?

aep commented 4 years ago

that's odd....the toml syntax you used isnt accepted, although i think that's correct?

anyway, this works:

[project]
version   = "0.1"
name      = "ckb-zz-demo"
cincludes = [".", "src"]

[[artifacts]]
name = "main1"
main = "ckb_zz_demo::main1"
type = "cmake"
xxuejie commented 4 years ago

Hmm I think you are right, not sure why I came up that previous syntax, thanks for all the help!

EDIT: I think the problem with my example, is that artifacts end up being a field in project, while the correct version has artifacts positioned at the same level of project.

aep commented 4 years ago

this has changed again. does zz build --export fit your needs?

aep commented 4 years ago

there are many ways now to export C only code. closing this.

feel free to reopen if you have more questions