Zulip Chat Archive

Stream: lean4

Topic: Cross-compiling Init

Locria Cyber (Feb 20 2023 at 02:37):

How to cross-compile Init to other architecture? This is needed to cross-compile Lean programs.

Locria Cyber (Feb 23 2023 at 06:11):

bump

Reid Barton (Feb 23 2023 at 06:13):

Does Lean support cross-compiling at all?

Locria Cyber (Feb 23 2023 at 06:13):

Not yet.

Locria Cyber (Feb 23 2023 at 06:14):

libleancpp need to be cross-compiled too. Currently the default installation only ship with compiled static library for native platform

Locria Cyber (Feb 23 2023 at 06:15):

To do:

  1. Ship C++ source code

  2. compile to target platform on the fly
    Currently leanc is a dumb Clang wrapper.

  3. lake support

Reid Barton (Feb 23 2023 at 06:20):

How would e.g. compiled tactics work?

Last updated: Dec 20 2023 at 11:08 UTC