k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [[K-user] ] How do I use the LLVM backend?

From: Markus Völter <voelter AT gmail.com>
To: dwight.guth AT runtimeverification.com
Cc: k-user AT lists.cs.illinois.edu
Subject: Re: [[K-user] ] How do I use the LLVM backend?
Date: Wed, 14 Nov 2018 10:25:12 +0100
Authentication-results: illinois.edu; spf=pass smtp.mailfrom=voelter AT gmail.com; dkim=pass header.d=gmail.com header.s=20161025; dmarc=pass header.from=gmail.com

Hello Dwight,

thank you very much for your reply. However, since I am not a Unix/C/Build guy, I will

postpone moving to LLVM until you've built a binary.

Cheers,

Markus

On Tue, Nov 13, 2018 at 11:06 PM Dwight Guth <dwight.guth AT runtimeverification.com> wrote:

The plan eventually is to package the llvm backend with releases of k downloaded online, but we haven't had time yet. Obviously we also intend to have installation instructions, but again, haven't gotten around to it yet.

The short version is, install the dependencies, then run "mkdir build; cd build; cmake .. -DCMAKE_BUILD_TYPE=Release; make; make install" and add the bin directory under the install path to your path in the shell. I don't have an exact list of dependencies though; you will have to try to build it and see what breaks. At the very least it requires flex, bison, llvm 6 (including clang and clang++), and gmp, but there are certainly others that I can't think of off the top of my head.

Since you're on mac, I strongly suggest installing stock llvm from something like homebrew as I doubt the apple llvm that comes with the system will work.

On Tue, Nov 13, 2018 at 3:47 PM Markus Völter <voelter AT gmail.com> wrote:
Hi,

I am new to K and I am making progress with my first programs.

Grigore suggested I use the LLVM backend, I guess by specifying
--backend llvm for kompile. But I get an error that llvm-kompile is
missing. I guess I have to install https://github.com/kframework/llvm-backend

However, there is no readme and no release. Any suggestions on
how I install this on a Mac?

Thx,
Markus

--
Dr. Markus Völter

voelter - ingenieurbüro für softwaretechnologie
voelter AT acm.org | +49 (0) 171 / 86 01 869

http://voelter.de -- personal website incl. papers, talks, books
http://voelter.de/essays -- writings on language engineering
http://omegataupodcast.net -- science and engineering podcast

--
Dwight Guth
Lead Blockchain Engineer

Email: dwight.guth AT runtimeverification.com

Dr. Markus Völter

voelter - ingenieurbüro für softwaretechnologie
voelter AT acm.org | +49 (0) 171 / 86 01 869

http://voelter.de -- personal website incl. papers, talks, books
http://voelter.de/essays -- writings on language engineering
http://omegataupodcast.net -- science and engineering podcast

[[K-user] ] How do I use the LLVM backend?, Markus Völter, 11/13/2018
- Re: [[K-user] ] How do I use the LLVM backend?, Dwight Guth, 11/13/2018
  - Re: [[K-user] ] How do I use the LLVM backend?, Markus Völter, 11/14/2018