Skip to content

Commit

Permalink
Update the OS build. (kframework#406)
Browse files Browse the repository at this point in the history
  • Loading branch information
chathhorn authored and h0nzZik committed May 20, 2019
1 parent c755c42 commit 9aa00fa
Showing 8 changed files with 53 additions and 60 deletions.
11 changes: 0 additions & 11 deletions Dockerfile
Original file line number Diff line number Diff line change
@@ -21,8 +21,6 @@ ENV LC_ALL en_US.UTF-8

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

RUN curl -sSL https://get.haskellstack.org/ | sh

RUN cpan install App::FatPacker Getopt::Declare String::Escape String::ShellQuote UUID::Tiny

ARG USER_ID=1000
@@ -31,12 +29,3 @@ RUN groupadd -g $GROUP_ID user \
&& useradd -m -u $USER_ID -s /bin/sh -g user user

USER $USER_ID:$GROUP_ID

RUN curl https://sh.rustup.rs -sSf | sh -s -- -y --default-toolchain 1.28.0

ADD .build/k/k-distribution/src/main/scripts/bin/k-configure-opam-dev .build/k/k-distribution/src/main/scripts/bin/k-configure-opam-common /home/user/.tmp-opam/bin/
ADD .build/k/k-distribution/src/main/scripts/lib/opam /home/user/.tmp-opam/lib/opam/
RUN cd /home/user \
&& ./.tmp-opam/bin/k-configure-opam-dev

RUN opam install linenoise
14 changes: 4 additions & 10 deletions INSTALL.md
Original file line number Diff line number Diff line change
@@ -11,19 +11,13 @@ do any installation steps not listed explicitly.

We recommend using Linux or OSX on a computer with at least 1 GB of memory.

On Ubuntu 16.04, the installation process for our C semantics can be summarized as:
On Ubuntu 18.04, the installation process for our C semantics can be summarized as:
```
$ 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 libxml-libxml-perl libstring-escape-perl libstring-shellquote-perl libgetopt-declare-perl opam pkg-config libapp-fatpacker-perl
$ git clone --depth=1 https://github.com/runtimeverification/k.git
$ cd k
$ mvn package
$ export PATH=$PATH:`pwd`/k-distribution/target/release/k/bin
$ mvn dependency:copy -Dartifact=com.runtimeverification.rv_match:ocaml-backend:1.0-SNAPSHOT -DoutputDirectory=k-distribution/target/release/k/lib/java
$ cd ..
$ 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 --depth=1 https://github.com/kframework/c-semantics.git
$ k-configure-opam-dev
$ eval `opam config env`
$ cd c-semantics
$ make ocaml-deps
$ eval $(opam config env)
$ make -j4
$ export PATH=$PATH:`pwd`/dist
```
7 changes: 3 additions & 4 deletions Jenkinsfile
Original file line number Diff line number Diff line change
@@ -17,11 +17,10 @@ pipeline {
steps {
ansiColor('xterm') {
sh '''
make ocaml-deps
eval $(opam config env)
cd .build/k
mvn verify -U -Dcheckstyle.skip -DskipKTest -Dllvm.backend.skip -Dhaskell.backend.skip -DbuildProfile=x86_64-gcc-glibc
cd ../..
make os-check -j`nproc`
make -j4
make -C tests/unit-pass -j$(nproc) os-comparison
'''
}
}
27 changes: 15 additions & 12 deletions Makefile
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
BUILD_DIR = $(CURDIR)/.build
K_SUBMODULE = $(BUILD_DIR)/k
export K_OPTS := -Xmx8g -Xss32m
export K_BIN ?= $(K_SUBMODULE)/k-distribution/target/release/k/bin
export K_SUBMODULE_DIST := $(K_SUBMODULE)/k-distribution/target/release/k
export K_SUBMODULE_BIN := $(K_SUBMODULE_DIST)/bin
export K_BIN ?= $(K_SUBMODULE_BIN)
export KOMPILE = $(K_BIN)/kompile -O2
export KDEP = $(K_BIN)/kdep

@@ -28,6 +30,7 @@ FILES_TO_DIST = \
clang-tools/clang-kast \
clang-tools/call-sites \
scripts/cdecl-3.6/src/cdecl \
$(K_SUBMODULE_DIST) \
LICENSE \
licenses

@@ -48,21 +51,24 @@ define timestamp_of
dist/profiles/$(PROFILE)/$(1)-kompiled/$(1)-kompiled/timestamp
endef

.PHONY: default check-vars semantics clean stdlibs deps c-cpp-semantics test-build pass fail fail-compile parser/cparser clang-tools/clang-kast $(PROFILE)-native
.PHONY: default check-vars semantics clean stdlibs c-cpp-semantics test-build pass fail fail-compile parser/cparser clang-tools/clang-kast $(PROFILE)-native

default: test-build

deps: $(K_BIN)/kompile

$(K_BIN)/kompile:
$(K_SUBMODULE)/pom.xml:
@echo "== submodule: $@"
git submodule update --init -- $(K_SUBMODULE)

$(K_SUBMODULE_DIST): $(K_SUBMODULE)/pom.xml
cd $(K_SUBMODULE) \
&& mvn package -q -Dhaskell.backend.skip -Dllvm.backend.skip -DskipTests -U
$(K_BIN)/k-configure-opam-dev
eval `opam config env`

check-vars: deps
$(K_SUBMODULE_BIN)/kompile: $(K_SUBMODULE_DIST)

ocaml-deps: $(K_SUBMODULE)/pom.xml
$(K_SUBMODULE)/k-distribution/src/main/scripts/bin/k-configure-opam-dev

check-vars: $(K_BIN)/kompile
@if ! ocaml -version > /dev/null 2>&1; then echo "ERROR: You don't seem to have ocaml installed. You need to install this before continuing. Please see INSTALL.md for more information."; false; fi
@if ! $(CC) -v > /dev/null 2>&1; then if ! clang -v > /dev/null 2>&1; then echo "ERROR: You don't seem to have gcc or clang installed. You need to install this before continuing. Please see INSTALL.md for more information."; false; fi fi
@perl scripts/checkForModules.pl
@@ -165,7 +171,7 @@ test-build: stdlibs
@rm -f dist/testProgram.out
@echo "Done."

parser/cparser:
parser/cparser: ocaml-deps
@echo "Building the C parser..."
@$(MAKE) -C parser

@@ -211,9 +217,6 @@ fail: test-build
fail-compile: test-build
@$(MAKE) -C tests/unit-fail-compilation comparison

os-check: test-build
@$(MAKE) -C tests/unit-pass os-comparison

clean:
-$(MAKE) -C parser clean
-$(MAKE) -C clang-tools clean
25 changes: 18 additions & 7 deletions scripts/RV_Kcc/Files.pm
Original file line number Diff line number Diff line change
@@ -13,17 +13,18 @@ our $VERSION = 1.00;
our @ISA = qw(Exporter);
our @EXPORT = qw();
our @EXPORT_OK = qw(
profileDir
nativeCC
nativeCXX
distDir
currentProfile
defaultProfile
getProfiles
tempFile
tempDir
distDir
error
getProfiles
IS_CYGWIN
kBinDir
nativeCC
nativeCXX
profileDir
tempDir
tempFile
);

use constant IS_CYGWIN => $^O eq "cygwin" || $^O eq "msys";
@@ -92,6 +93,16 @@ sub profileDir {
return catfile($prof, @_);
}

sub kBinDir {
my $path = defined($ENV{'K_BIN'})? $ENV{'K_BIN'} : distDir('k', 'bin');
if (IS_CYGWIN) {
$path = shell("cygpath -w $path")->stdout()->run();
chop($path);
}

return catfile($path, @_);
}

sub nativeCC {
return profileDir("cc");
}
4 changes: 2 additions & 2 deletions scripts/RV_Kcc/Shell.pm
Original file line number Diff line number Diff line change
@@ -11,12 +11,12 @@ use File::Spec::Functions qw(catfile);
use String::ShellQuote qw(shell_quote_best_effort);
use Exporter;

use RV_Kcc::Files qw(tempFile IS_CYGWIN);
use RV_Kcc::Files qw(tempFile kBinDir IS_CYGWIN);

use constant NULL => '/dev/null';

use constant KBIN2TEXT => do {
my $path = defined($ENV{'K_BIN'})? catfile($ENV{'K_BIN'}, 'k-bin-to-text') : 'k-bin-to-text';
my $path = kBinDir('k-bin-to-text');
my $ext = IS_CYGWIN? '.bat' : '';
$path . $ext;
};
10 changes: 6 additions & 4 deletions scripts/kcc
Original file line number Diff line number Diff line change
@@ -14,7 +14,7 @@ use MIME::Base64 qw(encode_base64);
use String::Escape qw(quote backslash printable);
use UUID::Tiny qw(:std);

use RV_Kcc::Files qw(profileDir nativeCC nativeCXX distDir tempFile tempDir error IS_CYGWIN);
use RV_Kcc::Files qw(profileDir nativeCC nativeCXX distDir kBinDir tempFile tempDir error IS_CYGWIN);
use RV_Kcc::Opts qw(
getopts arg classify
cppArgs suppressions ifdefs ldArgs nativeObjFiles srcFiles objFiles trampolineFiles breakpoints
@@ -33,7 +33,7 @@ $SIG{'STOP'} = 'interruptHandler';
$SIG{'INT'} = 'interruptHandler'; # Handle control-c.

use constant KRUN => do {
my $path = defined($ENV{'K_BIN'})? catfile($ENV{'K_BIN'}, 'krun') : 'krun';
my $path = kBinDir('krun');
my $ext = IS_CYGWIN? '.bat' : '';
$path . $ext;
};
@@ -127,8 +127,10 @@ sub main {
close(FILE);

my $profDir = profileDir();
$template =~ s?EXTERN_SCRIPTS_DIR?$profDir?g;
$template =~ s?EXTERN_HEAP_SIZE?$heapSize?g;
my $krun = KRUN;
$template =~ s?__EXTERN_SCRIPTS_DIR__?$profDir?g;
$template =~ s?__EXTERN_HEAP_SIZE__?$heapSize?g;
$template =~ s?__EXTERN_KRUN__?$krun?g;

open(my $programRunner, '>', $oval) or error("Couldn't open file: $!\n");
print $programRunner "$template\n";
15 changes: 5 additions & 10 deletions scripts/program-runner
Original file line number Diff line number Diff line change
@@ -23,23 +23,18 @@ $SIG{'INT'} = 'interruptHandler'; # handle control-c

# Set heap and stack size of krun

my $HEAP_SIZE = "EXTERN_HEAP_SIZE";
my $HEAP_SIZE = "__EXTERN_HEAP_SIZE__";

$ENV{K_OPTS} = "-Xms64m -Xmx$HEAP_SIZE -Xss32m -XX:+TieredCompilation";

my $SCRIPTS_DIR = "EXTERN_SCRIPTS_DIR";
my $SCRIPTS_DIR = "__EXTERN_SCRIPTS_DIR__";

my $KRUN = "__EXTERN_KRUN__";

my $EXEC_DEF = catfile($SCRIPTS_DIR, "c-cpp-kompiled");
my $EXEC_ND_DEF = catfile($SCRIPTS_DIR, "c-nd-kompiled");
my $EXEC_ND_THREAD_DEF = catfile($SCRIPTS_DIR, "c-nd-thread-kompiled");

use constant IS_CYGWIN => $^O eq "cygwin" || $^O eq "msys";
use constant KRUN => do {
my $path = defined($ENV{'K_BIN'})? catfile($ENV{'K_BIN'}, 'krun') : 'krun';
my $ext = IS_CYGWIN? '.bat' : '';
$path . $ext;
};

my @temporaryFiles = ();

exit main();
@@ -150,7 +145,7 @@ sub main {

# Execute krun with the arguments in @cmd
print("'krun' '" . join("' '", @cmd) . "'\n") if defined $ENV{VERBOSE};
my $ret = system(KRUN, @cmd) >> 8;
my $ret = system($KRUN, @cmd) >> 8;

if (defined $ENV{LTLMC} | defined $ENV{PROVE}) {
return 0;

0 comments on commit 9aa00fa

Please sign in to comment.