Update makefile and ci to generate all bundles

.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

Makefile

 .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))

README.md

 # 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
 

test.sh

 #!/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

tools/colibri_for_bundle.ml

+
 let coldir = Filename.dirname Sys.executable_name
 
 let conf = ref "true"