From 7dd929141977205d50baa7b1429ba7dd7f58e7cd Mon Sep 17 00:00:00 2001 From: Etienne Kneuss <ekneuss@gmail.com> Date: Mon, 18 May 2015 16:16:34 +0200 Subject: [PATCH] Mention compilation to bytecode --- doc/faq.rst | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/doc/faq.rst b/doc/faq.rst index d687e1b0c..b3e1ec040 100644 --- a/doc/faq.rst +++ b/doc/faq.rst @@ -36,3 +36,17 @@ large, so, if the input list had the size `Int.MaxValue + 1` around and produce `Int.MinValue` (that is, -2^31), so the `ensuring` clause would not hold. +Compiling Leon programs to bytecode +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +If you don't use special constructs such as ``choose``, you should be able to +compile Leon programs to `.class` using `scalac` and execute them directly on +the JVM, or integrate them as part as other Scala-based projects. + +Beware that you need to explicitly include files files from the Leon library +(that are implicitly bundled when you use the `./leon` script): + +.. code-block:: bash + + $ mkdir out + $ scalac $(find path/to/leon/library/ -name "*.scala" | xargs) MyFile.scala -d out -- GitLab