diff --git a/Dockerfile b/Dockerfile index 2d8f713bd..24627cef1 100644 --- a/Dockerfile +++ b/Dockerfile @@ -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 diff --git a/INSTALL.md b/INSTALL.md index 1780e441d..1acea61cd 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -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 ``` diff --git a/Jenkinsfile b/Jenkinsfile index dc9a7b2df..dbb9e54f9 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -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 ''' } } diff --git a/Makefile b/Makefile index 1a86b5982..f6eb1dfda 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/scripts/RV_Kcc/Files.pm b/scripts/RV_Kcc/Files.pm index 1ecf803de..1710663ba 100644 --- a/scripts/RV_Kcc/Files.pm +++ b/scripts/RV_Kcc/Files.pm @@ -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"); } diff --git a/scripts/RV_Kcc/Shell.pm b/scripts/RV_Kcc/Shell.pm index 350a93253..2590be447 100644 --- a/scripts/RV_Kcc/Shell.pm +++ b/scripts/RV_Kcc/Shell.pm @@ -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; }; diff --git a/scripts/kcc b/scripts/kcc index 590797ad9..5c2e3d253 100755 --- a/scripts/kcc +++ b/scripts/kcc @@ -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"; diff --git a/scripts/program-runner b/scripts/program-runner index 5d17bf1b5..b711003c5 100755 --- a/scripts/program-runner +++ b/scripts/program-runner @@ -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;