diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 4d08bfada64d2928a80df082d59b01fc6326a0da..68d31e6ef0c6b2224fcde0afa38bfd5c36cf80ca 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -14,15 +14,12 @@ build: - sudo apt-get update - sudo apt-get install -y make libgmp-dev - opam install dune.3.12.1 fmt.0.9.0 gen.1.1 menhir.20230608 ocplib-simplex.0.5 parsexp.v0.16.0 spelll.0.4 uutf.1.0.3 zarith.1.13 - - make clean - - make clean_bundle - - make - - make bundle - - make bundle.tbz + - make archives artifacts: paths: - bundle - - bundle.tbz + - bundle-v5.tbz + - bundle-v7.tbz expire_in: 1 week tags: - docker @@ -34,7 +31,7 @@ test: script: - apt-get update - apt-get install -y make parallel - - make test + - make tests artifacts: paths: - logs @@ -48,14 +45,19 @@ prepare-release: rules: - if: $CI_PIPELINE_SOURCE == "trigger" variables: - ARCHIVE_NAME: '$PROJECT.$TAG.tbz' - PACKAGE_URI: '$PROJECT_URI/packages/generic/$PROJECT/$TAG/$ARCHIVE_NAME' + PREFIX: '$PROJECT_URI/packages/generic/$PROJECT/$TAG' + ARCHIVE_V5_NAME: '$PROJECT.$TAG-e5.tbz' + ARCHIVE_V7_NAME: '$PROJECT.$TAG-e7.tbz' + PACKAGE_V5_URI: '$PREFIX/$ARCHIVE_V5_NAME' + PACKAGE_V7_URI: '$PREFIX/$ARCHIVE_V7_NAME' script: - apt-get update - apt-get install -y curl - sed -n -f changelog.sed CHANGES.md > description.txt - | - curl --fail --header "JOB-TOKEN: ${CI_JOB_TOKEN}" --upload-file bundle.tbz "$PACKAGE_URI" + curl --fail --header "JOB-TOKEN: ${CI_JOB_TOKEN}" --upload-file bundle-v5.tbz "$PACKAGE_V5_URI" + - | + curl --fail --header "JOB-TOKEN: ${CI_JOB_TOKEN}" --upload-file bundle-v7.tbz "$PACKAGE_V7_URI" artifacts: paths: - description.txt @@ -68,8 +70,11 @@ release: rules: - if: $CI_PIPELINE_SOURCE == "trigger" variables: - ARCHIVE_NAME: '$PROJECT.$TAG.tbz' - PACKAGE_URI: '$PROJECT_URI/packages/generic/$PROJECT/$TAG/$ARCHIVE_NAME' + PREFIX: '$PROJECT_URI/packages/generic/$PROJECT/$TAG' + ARCHIVE_V5_NAME: '$PROJECT.$TAG-e5.tbz' + ARCHIVE_V7_NAME: '$PROJECT.$TAG-e7.tbz' + PACKAGE_V5_URI: '$PREFIX/$ARCHIVE_V5_NAME' + PACKAGE_V7_URI: '$PREFIX/$ARCHIVE_V7_NAME' script: - echo "Release job for tag $TAG" release: @@ -80,9 +85,14 @@ release: milestones: [] assets: links: - - name: '$ARCHIVE_NAME' - url: '$PACKAGE_URI' - filepath: '/bundle' + - name: '$ARCHIVE_V5_NAME' + url: '$PACKAGE_V5_URI' + filepath: '/bundle-v5' + link_type: 'other' + links: + - name: '$ARCHIVE_V7_NAME' + url: '$PACKAGE_V5_URI' + filepath: '/bundle-v7' link_type: 'other' tags: - docker diff --git a/Makefile b/Makefile index b7e1225d311df6e62ffa27336f1de87563882f6d..6652798681e9ab580891b63829359bee89962423 100644 --- a/Makefile +++ b/Makefile @@ -1,39 +1,30 @@ .PHONY: all bundle clean clean_bundle simplex simplex_epilog +# NB. This makefile uses rules like v5-% and v7-% to setup +# the required environment before executing the associated +# rule %. +# +# This makes it easy to have a common script for the +# different cases, but unfortunately this forces the +# makefile to rebuild everything: the contextual variables +# cannot appear as dependencies or targets of rules, because +# these are evaluated at rule-definition-time. That's why +# the rules are basically just keywords like "prepare-build" +# and "archive", etc. +# +# A different approach should be possible here, but for now +# this is what is being done. + # Bundle prefix, override to specify a different directory BUNDLE ?= $(PWD)/bundle -# Which eclipse version to use, among {v5|v7} -# (v5 is currently broken) -ECL_VERSION ?= v7 +all : build_all +build_all: v5-build v7-build -all : build - -# ================================================== -# MACRO -# ================================================== - -# Target of copy dependencies are added to this variable. -COPY_DEPS := - -define add_copy_rule -COPY_DEPS += $(2) -$(2) : $(1) - mkdir -p $(dir $(2)) - cp $(1) $(2) -endef - -# Add a rule to copy a file from a source to a destination, while -# ensuring that the target directory exists. -# -# $(1): source -# $(2): destination -# -define require_copy +VERSION := $(shell cat version) -$(eval $(call add_copy_rule,$(1),$(2))) - -endef +show_version: + echo "version file contains: $(VERSION)" # ================================================== # CONFIGURATION @@ -42,32 +33,38 @@ endef ROOT := $(realpath Src/) COLIBRI := $(ROOT)/COLIBRI SIMPLEX_BUILD := $(COLIBRI)/simplex_ocaml/_build/default -$(call require_copy,$(SIMPLEX_BUILD)/simplex_ocaml.pl,$(COLIBRI)/simplex_ocaml.pl) - -ifeq ($(ECL_VERSION),v7) -export ECLIPSEBIN=$(PWD)/Bin/ECLIPSE_V7.0_45 -LIBDIR=$(COLIBRI)/lib/v7 -SIMPLEX := simplex_ocaml_mod_v7.so -FLOAT_LIB := $(LIBDIR)/x86_64_linux/float_util.so -$(call require_copy,$(SIMPLEX_BUILD)/simplex_ocaml_mod_v7.so,$(LIBDIR)/x86_64_linux/simplex_ocaml.so) -endif - -ifeq ($(ECL_VERSION),v5) -export ECLIPSEBIN=$(PWD)/Bin/ECLiPSe_5.10 -LIBDIR=$(COLIBRI)/lib/v5 -SIMPLEX := simplex_ocaml_mod.so -FLOAT_LIB := $(LIBDIR)/x86_64_linux/float_util.so -$(call require_copy,$(SIMPLEX_BUILD)/simplex_ocaml_mod.so,$(LIBDIR)/x86_64_linux/simplex_ocaml.so) -endif -# ================================================== -# INFOS -# ================================================== - -$(info BUNDLE=$(BUNDLE)) -$(info ECL_VERSION=$(ECL_VERSION)) -$(info COLIBRI=$(COLIBRI)) -$(info ECLIPSEBIN=$(ECLIPSEBIN)) +$(COLIBRI)/simplex_ocaml.pl: $(SIMPLEX_BUILD)/simplex_ocaml.pl + mkdir -p $(dir $@) + cp $< $@ + +infos: + $(info BUNDLE=$(BUNDLE)) + $(info ECL_VERSION=$(ECL_VERSION)) + $(info COLIBRI=$(COLIBRI)) + $(info ECLIPSEBIN=$(ECLIPSEBIN)) + +v5-%: ECL_VERSION = v5 +v5-%: export ECLIPSEBIN = $(PWD)/Bin/ECLiPSe_5.10 +v5-%: LIBDIR = $(COLIBRI)/lib/v5 +v5-%: SIMPLEX = simplex_ocaml_mod.so +v5-%: FLOAT_LIB = $(LIBDIR)/x86_64_linux/float_util.so +v5-%: BUNDLE_ROOT = $(BUNDLE)/$(ECL_VERSION) +v5-%: CPP_FLAGS = -fPIC -O -D__LINUX__ -shared -I $(ECLIPSEBIN)/include/x86_64_linux +v5-%: ARCHIVE = colibri-$(VERSION)-$(ECL_VERSION) +v5-%: infos % + @ echo $@ done + +v7-%: ECL_VERSION = v7 +v7-%: export ECLIPSEBIN = $(PWD)/Bin/ECLIPSE_V7.0_45 +v7-%: LIBDIR = $(COLIBRI)/lib/v7 +v7-%: SIMPLEX = simplex_ocaml_mod_v7.so +v7-%: FLOAT_LIB = $(LIBDIR)/x86_64_linux/float_util.so +v7-%: BUNDLE_ROOT = $(BUNDLE)/$(ECL_VERSION) +v7-%: CPP_FLAGS = -fPIC -O -D__LINUX__ -shared -I $(ECLIPSEBIN)/include/x86_64_linux +v7-%: ARCHIVE = colibri-$(VERSION)-$(ECL_VERSION) +v7-%: infos % + @ echo $@ done # ================================================== # SIMPLEX_OCAML @@ -75,24 +72,22 @@ $(info ECLIPSEBIN=$(ECLIPSEBIN)) simplex: $(ECLIPSEBIN) cd $(COLIBRI)/simplex_ocaml && dune build $(SIMPLEX) simplex_ocaml.pl + mkdir -p $(LIBDIR)/x86_64_linux/ + cp $(SIMPLEX_BUILD)/$(SIMPLEX) $(LIBDIR)/x86_64_linux/simplex_ocaml.so -simplex_epilog : simplex $(COPY_DEPS) - @echo COPY_DEPS=$(COPY_DEPS) +simplex_epilog : simplex $(COLIBRI)/simplex_ocaml.pl # ================================================== # FLOAT LIBRARY # ================================================== -CPP_FLAGS := -fPIC -O -D__LINUX__ -shared -CPP_FLAGS += -I $(ECLIPSEBIN)/include/x86_64_linux - CPP_FILES := \ $(ROOT)/Floats/EclipseInterfaceSimFloat2.2.cpp \ $(ROOT)/Floats/Floatcpp-3.0_SimFloat2.2.cpp -$(FLOAT_LIB) : $(CPP_FILES) - mkdir -p $(dir $@) - g++ $(CPP_FLAGS) $(CPP_FILES) -o $@ +float_lib : $(CPP_FILES) + mkdir -p $(dir $(FLOAT_LIB)) + g++ $(CPP_FLAGS) $(CPP_FILES) -o $(FLOAT_LIB) # ================================================== # BUILD @@ -105,11 +100,11 @@ clean: rm -f compile_colibri rm -rf $(PWD)/tools/_build/ -compile_colibri : +compile_colibri: cd tools/ && dune build compile_colibri.exe cp -a $(PWD)/tools/_build/default/compile_colibri.exe $@ -build: simplex_epilog $(FLOAT_LIB) compile_colibri +build: simplex_epilog float_lib compile_colibri ./compile_colibri --eclipsedir $(ECLIPSEBIN) # ================================================== @@ -121,36 +116,43 @@ BUNDLE_SRC := \ Src/COLIBRI/filter_smtlib_file \ Src/COLIBRI/filter_smtlib_file.exe -$(BUNDLE)/colibri.exe : +prepare_build: + mkdir -p $(BUNDLE_ROOT) + +colibri_executables: cd tools/ && dune build colibri_for_bundle.exe - cp -a $(PWD)/tools/_build/default/colibri_for_bundle.exe $@ + cp -af $(PWD)/tools/_build/default/colibri_for_bundle.exe $(BUNDLE_ROOT)/colibri.exe + cp -af $(PWD)/tools/_build/default/colibri_for_bundle.exe $(BUNDLE_ROOT)/colibri clean_bundle: - rm -fr $(BUNDLE) + rm -fr $(BUNDLE_ROOT) -$(BUNDLE): - mkdir -p $(BUNDLE) +bundle: prepare_build build colibri_executables + mkdir -p $(BUNDLE_ROOT)/COLIBRI/lib/ + cp -ra $(LIBDIR) $(BUNDLE_ROOT)/COLIBRI/lib/ + cp -ra $(BUNDLE_SRC) $(BUNDLE_ROOT)/COLIBRI/ + cp -ra compile_flag.pl $(BUNDLE_ROOT)/COLIBRI/ + cp -ra version $(BUNDLE_ROOT)/ + cp -ra $(ECLIPSEBIN) $(BUNDLE_ROOT)/ECLIPSE/ -$(BUNDLE)/colibri: $(BUNDLE)/colibri.exe - cp -ra $< $@ +archive: bundle +# generate name for user + tar cfj $(ARCHIVE).tbz --transform="s,^.,$(ARCHIVE)," -C $(BUNDLE_ROOT) . +# for continuous integration + ln -f $(ARCHIVE).tbz bundle-$(ECL_VERSION).tbz -bundle: build $(BUNDLE) $(BUNDLE)/colibri.exe $(BUNDLE)/colibri - mkdir -p $(BUNDLE)/COLIBRI/lib/ - cp -ra $(LIBDIR) $(BUNDLE)/COLIBRI/lib/ - cp -ra $(BUNDLE_SRC) $(BUNDLE)/COLIBRI/ - cp -ra compile_flag.pl $(BUNDLE)/COLIBRI/ - cp -ra version $(BUNDLE)/ - cp -ra $(ECLIPSEBIN) $(BUNDLE)/ECLIPSE/ - -bundle.tbz: bundle - tar cvfj $@ $< +archives: + make v5-archive + make v7-archive # ================================================== # TEST # ================================================== test: - ./test.sh -j2 + ./test.sh $(BUNDLE_ROOT)/colibri -j2 + +tests: v5-test v7-test # ================================================== # RELEASE @@ -161,7 +163,7 @@ PROJECT_URL := https://git.frama-c.com/api/v4/projects/804 RELEASE_REF ?= master GIT_TAG ?= $(shell git describe --tags --candidates=0 2> /dev/null) -check_release: +check_release: show_version @echo '' @echo 'RELEASE' $(if $(RELEASE_TOKEN),,$(error Call script with RELEASE_TOKEN set)) diff --git a/README.md b/README.md index 5c7966a9eaff4e7ba63303fbacb3fa4315e0e296..fe93563235b53d285578e0b1611b7df59cbc1a9c 100644 --- a/README.md +++ b/README.md @@ -1,9 +1,17 @@ # COLIBRI -## Bundle +## Bundles -The command `make bundle` will create a relocalisable directory named -`bundle` containing the ` colibri` executables. +The Makefile can produce a relocalisable directory for version 5 and 7 +of ECLiPSe, in `bundle/v5` and `bundle/v7`, with respectively `make v5-build` +and `make v7-build`. + +Inside each bundle directory there is a `colibri` executable. + +Also, `make v5-archive` and `make v7-archive` create `.tbz` archives +of the respective bundle directories. + +The command `make archives` will create both archives. ## Dependencies diff --git a/test.sh b/test.sh index 036efc3384dbbbd8d965087195db6da47da0f091..9653bdda2ab4fd2e1ca68819be901f7074bbbda5 100755 --- a/test.sh +++ b/test.sh @@ -1,5 +1,10 @@ #!/bin/sh -eu +NENO=$(readlink -f ./neno) + +SOLVER=$1 +shift + STEPS=100000 FAIL=false TIMEOUT=200 @@ -13,7 +18,7 @@ run_tests() { local log=$2 local redirect=$3 echo $path - if find ${path} -name "*.smt2" | parallel ${PARALLEL_OPTIONS} --timeout ${TIMEOUT} --joblog ${log} "./neno ${redirect} bundle/colibri --max-steps ${STEPS} {}"; then + if find ${path} -name "*.smt2" | parallel ${PARALLEL_OPTIONS} --timeout ${TIMEOUT} --joblog ${log} "${NENO} ${redirect} ${SOLVER} --max-steps ${STEPS} {}"; then echo OK else echo KO diff --git a/tools/colibri_for_bundle.ml b/tools/colibri_for_bundle.ml index 3d75c4df491580077a789699f6309207511ca9a7..4a2ac564471d45d7ce438120ff953073945e82c8 100644 --- a/tools/colibri_for_bundle.ml +++ b/tools/colibri_for_bundle.ml @@ -1,3 +1,4 @@ + let coldir = Filename.dirname Sys.executable_name let conf = ref "true"