Builds and a.out should find krun in $PATH

[GJDitchfield]

I built c-semantics on a computer running Ubuntu 18.04 and found some problems with file paths.

I followed INSTALL.md. In step 3 "Install K" I ran into some difficulties building K, then noticed that the instructions for installing K in Windows said to install a K deb file from https://github.com/kframework/k/releases into an Ubuntu WSL package. So I installed the deb in my Ubuntu system. The deb installed /usr/bin/kompile and /usr/bin/krun, and of course /usr/bin is in my $PATH.

Problem 1: in step 7 "Build our C tool", "make" produced this error:

/bin/sh: 1: /home/gjditchf/Desktop/c-semantics/.build/k/k-distribution/target/release/k/bin/kompile: not found
Makefile:60: recipe for target '/home/gjditchf/Desktop/c-semantics/dist/profiles/x86-gcc-limited-libc/c-cpp-linking-kompiled/c-cpp-linking-kompiled/timestamp' failed

The build looks for kompile in a specific (and to mind, odd) place instead of finding it in $PATH, even though INSTALL.md instructed me to include it in my $PATH.

Problem 2: I tried to work around this by running "make K_BIN=/usr/bin". That produced

...
cp -RLp scripts/kcc scripts/k++ scripts/kranlib scripts/merge-kcc-obj scripts/split-kcc-obj scripts/make-trampolines scripts/make-symbols scripts/gccsymdump scripts/globalize-syms scripts/ignored-flags scripts/program-runner scripts/histogram-csv parser/cparser /home/gjditchf/Desktop/c-semantics/dist/clang-tools/bin/clang-kast /home/gjditchf/Desktop/c-semantics/dist/clang-tools/bin/call-sites scripts/cdecl-3.6/src/cdecl /usr LICENSE licenses /home/gjditchf/Desktop/c-semantics/dist
cp: cannot copy cyclic symbolic link '/usr/bin/X11'
...

... and eventually caused a "disk full" error because it was trying to copy all of /usr into my workspace. This was caused by Makefile's line 39, K_DIST := $(realpath $(K_BIN)/..).

I couldn't figure out what it was supposed to be copying out of K_DIST, so I tried running "make K_BIN=/usr/bin K_DIST=". That seemed to work.

Problem 3: INSTALL.md says to execute dist/kcc tests/unitTests/helloworld.c. That C file doesn't exist.

Problem 4: I compiled hello.C instead.

$ dist/kcc tests/unit-pass/hello.C 
$ ./a.out
Can't exec "/home/gjditchf/Desktop/c-semantics/dist/k/bin/krun": No such file or directory at ./a.out line 148.

The generated a.out isn't looking for krun in $PATH. Apparently the environment variable K_BIN must be set when kcc runs.

[chathhorn]

The build system is currently in a state of flux and the INSTALL.md has unfortunately gotten out of date again. The Jenkinsfile/Dockerfile are probably the best reference for how to build things until we get everything fixed and updated. Also, note that we're dependent on a pretty particular version of K (see the submodule in .build/k), so K probably shouldn't be installed separately. If you do install a compatible version via the debian package, though, I think it should work to have K_BIN set in the environment to /usr/lib/kframework/bin while building and running kcc.

From a clean Ubuntu 18.04 (without K), I think this is a summary of all of the steps to build the current master (@charala1 let me know if I'm missing something):

$ sudo apt-get install maven git openjdk-8-jdk flex libgmp-dev libmpfr-dev build-essential cmake zlib1g-dev libclang-3.9-dev llvm-3.9 diffutils libuuid-tiny-perl libstring-escape-perl libstring-shellquote-perl libgetopt-declare-perl opam pkg-config libapp-fatpacker-perl
$ git clone https://github.com/kframework/c-semantics.git
$ cd c-semantics
$ git submodule update --init --recursive
$ .build/k/k-distribution/bin/k-configure-opam-dev
$ eval $(opam config env)
$ cd .build/k
$ mvn package -q -U -DskipTests -DskipKTest -Dhaskell.backend.skip -Dllvm.backend.skip -Dcheckstyle.skip
$ cd ..
$ make -j4
$ export PATH=$PATH:`pwd`/dist

[charala1]

Complementing Chris' response, the complete list of packages that we currently use to test the semantics (on Ubuntu 18.04) is:

bison build-essential clang++-6.0 clang-6.0 cmake coreutils curl diffutils flex git libboost-test-dev libffi-dev libgmp-dev libjemalloc-dev libmpfr-dev libstdc++6 libxml2 libyaml-cpp-dev llvm-6.0 m4 maven opam openjdk-8-jdk pkg-config python3 python-jinja2 python-pygments unifdef zlib1g-dev

You will also need these perl packages, which you can install with cpan:

App::FatPacker Getopt::Declare String::Escape String::ShellQuote UUID::Tiny

Clone the repository: git clone --recurse-submodules https://github.com/kframework/c-semantics.git, then cd into the cloned directory and follow these steps:

./.build/k/k-distribution/bin/k-configure-opam-dev
cd ./.build/k && mvn package -q -U -DskipTests -DskipKTest -Dhaskell.backend.skip -Dllvm.backend.skip -Dcheckstyle.skip

If you face java version compatibility issues with the maven command above, the following should fix it:

sudo update-alternatives --set java /usr/lib/jvm/java-8-openjdk-amd64/jre/bin/java

(and then re-run the above maven command).

At this point, you have a working installation of k. Though this is not necessary to get the semantics working, you may add ./.build/k/k-distribution/target/release/k/bin to your PATH if you wish to use this version of k independently.

To compile the semantics, you can now run

eval $(opam config env) # not necessary if you are still in the same shell session
make

This will build everything in the cloned directory under dist/. If you want the build to go a little faster, consider passing -j4 to the make invocation.