leoprover / Leo-III

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
http://inf.fu-berlin.de/~lex/leo3
BSD 3-Clause "New" or "Revised" License
41 stars 10 forks source link

Native Image using Graal #61

Closed mziener closed 5 years ago

mziener commented 5 years ago

Hi all,

i have used the GraalVM tooling in order to create a native binary. Preliminary tests suggest a decent speed up. For instance on sur_cantor.p from the test suite:

The build instructions can be found in the INSTALL.md.

In case of any questions or comments, feel free to reach out.

Best regards, Marco

Ryugoron commented 5 years ago

The build in the Makefile only works for Linux Distributions.

MacOS (DARWIN) does not allow statical linking of libraries.

lex-lex commented 5 years ago

Cool, thanks for the work! I'll do some tests on machine this week.