diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 527468dbaa8aeeb4c927c02ca0b4ab8b6359ff6a..cc8d46803142e1364f718dcb84cf7eb6e9d78724 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,9 +1,14 @@ +variables: + PROJECT: 'colibri' + ID: '804' + PROJECT_URI: 'https://git.frama-c.com/api/v4/projects/$ID' + stages: - build - test build: - image: ocaml/opam@sha256:aabf10d76f588677f6ee8007aae3d4dd45d28000501abce5aabda9de50e88dc7 + image: ocaml/opam:debian-10-ocaml-4.14 stage: build script: - sudo apt-get update @@ -13,15 +18,17 @@ build: - make clean_bundle - make - make bundle + - make bundle.tbz artifacts: paths: - bundle + - bundle.tbz expire_in: 1 week tags: - docker test: - image: debian@sha256:7ceacc4462a98718b236cbdeb850d4b7603afe4bab791336a0ed1c030f769f02 + image: debian:10 stage: test needs: [build] script: @@ -35,3 +42,47 @@ test: tags: - docker +prepare-release: + image: debian:10 + needs: [build] + rules: + - if: $CI_PIPELINE_SOURCE == "trigger" + variables: + ARCHIVE_NAME: '$PROJECT.$TAG.tbz' + PACKAGE_URI: '$PROJECT_URI/$PROJECT/$TAG/$ARCHIVE_NAME' + script: + - apt-get update + - apt-get install -y curl + - sed -n -f changelog.sed CHANGES.md > description.txt + - | + curl --header "PRIVATE-TOKEN: $CI_JOB_TOKEN" --upload-file bundle.tbz "$PACKAGE_URI" + artifacts: + paths: + - description.txt + tags: + - docker + +release: + image: registry.gitlab.com/gitlab-org/release-cli:latest + needs: [prepare-release] + rules: + - if: $CI_PIPELINE_SOURCE == "trigger" + variables: + ARCHIVE_NAME: '$PROJECT.$TAG.tbz' + PACKAGE_URI: '$PROJECT_URI/$PROJECT/$TAG/$ARCHIVE_NAME' + script: + - echo "Release job for tag $TAG" + release: + name: "Release $TAG" + description: description.txt + tag_name: "$TAG" + ref: '$CI_COMMIT_SHA' + milestones: [] + assets: + links: + - name: '$ARCHIVE_NAME' + url: '$PACKAGE_URI' + filepath: '/bundle' + link_type: 'other' + tags: + - docker diff --git a/CHANGES.md b/CHANGES.md new file mode 100644 index 0000000000000000000000000000000000000000..0f729bc8a276dbb4c0a503f8476080ffbee4bb47 --- /dev/null +++ b/CHANGES.md @@ -0,0 +1,8 @@ +## Release 2024.02 + * Use dune for ocaml tools + * Make release job on CI + +## Release 2023.12 + * Fix build + * Deploy a publicly downloadable bundle + diff --git a/Makefile b/Makefile index 0b9dfd4abe10185563b7abafe45945935640d68a..eb567f594e0e78d7bd0dec47b90b381b99711a77 100644 --- a/Makefile +++ b/Makefile @@ -30,7 +30,9 @@ endef # $(2): destination # define require_copy + $(eval $(call add_copy_rule,$(1),$(2))) + endef # ================================================== @@ -75,7 +77,7 @@ simplex: $(ECLIPSEBIN) cd $(COLIBRI)/simplex_ocaml && dune build $(SIMPLEX) simplex_ocaml.pl simplex_epilog : simplex $(COPY_DEPS) - @true + @echo COPY_DEPS=$(COPY_DEPS) # ================================================== # FLOAT LIBRARY @@ -89,6 +91,7 @@ CPP_FILES := \ $(ROOT)/Floats/Floatcpp-3.0_SimFloat2.2.cpp $(FLOAT_LIB) : $(CPP_FILES) + mkdir -p $(dir $@) g++ $(CPP_FLAGS) $(CPP_FILES) -o $@ # ================================================== @@ -100,9 +103,11 @@ clean: rm -f $(COLIBRI)/simplex_ocaml.pl rm -f $(FLOAT_LIB) rm -f compile_colibri + rm -rf $(PWD)/tools/_build/ -compile_colibri : compile_colibri.ml - ocamlopt -o $@ -I +unix unix.cmxa $^ +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 ./compile_colibri --eclipsedir $(ECLIPSEBIN) @@ -116,9 +121,9 @@ BUNDLE_SRC := \ Src/COLIBRI/filter_smtlib_file \ Src/COLIBRI/filter_smtlib_file.exe -$(BUNDLE)/colibri.exe : colibri_for_bundle.ml - ocamlopt -o $@ -I +unix unix.cmxa $^ - chmod u+x $@ +$(BUNDLE)/colibri.exe : + cd tools/ && dune build colibri_for_bundle.exe + cp -a $(PWD)/tools/_build/default/colibri_for_bundle.exe $@ clean_bundle: rm -fr $(BUNDLE) @@ -126,8 +131,10 @@ clean_bundle: $(BUNDLE): mkdir -p $(BUNDLE) -bundle: $(BUNDLE) $(BUNDLE)/colibri.exe - cp $(BUNDLE)/colibri.exe $(BUNDLE)/colibri +$(BUNDLE)/colibri: $(BUNDLE)/colibri.exe + cp -ra $< $@ + +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/ @@ -135,5 +142,38 @@ bundle: $(BUNDLE) $(BUNDLE)/colibri.exe cp -ra version $(BUNDLE)/ cp -ra $(ECLIPSEBIN) $(BUNDLE)/ECLIPSE/ +bundle.tbz: bundle + tar cvfj $@ $< + +# ================================================== +# TEST +# ================================================== + test: ./test.sh -j2 + +# ================================================== +# RELEASE +# ================================================== + +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: + @echo '' + @echo 'RELEASE' + $(if $(RELEASE_TOKEN),,$(error Call script with RELEASE_TOKEN set)) + $(if $(GIT_TAG),,$(error No git tag associated with current commit; set GIT_TAG or add a tag)) + @echo REF: $(RELEASE_REF) + @echo TAG: $(GIT_TAG) + @echo -n "Confirm? [y/N] " && read ans && [ $${ans:-N} = y ] + +release: check_release + @echo RELEASING + curl --request POST \ + --form token="$(RELEASE_TOKEN)" \ + --form ref="$(RELEASE_REF)" \ + --form variables[TAG]="$(GIT_TAG)" \ + "$(PROJECT_URL)/trigger/pipeline" diff --git a/changelog.sed b/changelog.sed new file mode 100644 index 0000000000000000000000000000000000000000..dca53eb1ac7088b50846581a11350803377a1e79 --- /dev/null +++ b/changelog.sed @@ -0,0 +1,44 @@ +# Read from markdown the first release section and its content. The +# expected format is a subset of Markdown that follows this pattern: +# +# ## Title containing "release" .... +# * only text +# * items can span multiple +# lines if necessary +# * other sections in the file are ignored + + +/^## .*\(r\|R\)elease/ b block +d # skip to next cyle + +:block +h # append line in hold space + +:next +z # zap (clear) pattern space +n # read next line + +# end of block? +/^ *$/ { + z # zap line (so that next exchange clears hold space) + x # exchange with hold space + + # use NUL to separate bullet points + s/\n *[*] */\d0/g + # join other lines together + s/ *\n */ /g + # trim lines + s/ *$//g + # Replace NUL by newlines and bullets + s/\d0/\n * /g + + # print and quit (replace q by d to list all releases) + p + q +} + +# line is not empty, append to hold space (with newline) +H + +# read next line +b next diff --git a/tools/.gitignore b/tools/.gitignore new file mode 100644 index 0000000000000000000000000000000000000000..c6a151b325b25cf78938a717b8dd1b86ef5ab382 --- /dev/null +++ b/tools/.gitignore @@ -0,0 +1 @@ +_build/ \ No newline at end of file diff --git a/tools/Makefile b/tools/Makefile new file mode 100644 index 0000000000000000000000000000000000000000..f4db3b71736ccd6123610c91598ec912e5fb20c6 --- /dev/null +++ b/tools/Makefile @@ -0,0 +1,2 @@ +all: + dune build diff --git a/colibri_for_bundle.ml b/tools/colibri_for_bundle.ml similarity index 100% rename from colibri_for_bundle.ml rename to tools/colibri_for_bundle.ml diff --git a/tools/colibri_for_bundle.opam b/tools/colibri_for_bundle.opam new file mode 100644 index 0000000000000000000000000000000000000000..339fb27ca1d0a7f25fe92b23cb7244fcc08d0d40 --- /dev/null +++ b/tools/colibri_for_bundle.opam @@ -0,0 +1,27 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "0.4.0" +synopsis: "Executable around colibri when used in bundle" +maintainer: ["Christophe Junke"] +authors: ["François Bobot" "Bruno Marre" "Christophe Junke"] +license: "MIT" +homepage: "https://colibri.frama-c.com" +bug-reports: "https://git.frama-c.com/pub/colibri/issues" +depends: [ + "dune" {>= "3.0"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] diff --git a/compile_colibri.ml b/tools/compile_colibri.ml similarity index 97% rename from compile_colibri.ml rename to tools/compile_colibri.ml index fc21fda0dd83a43959650287e177b10691ff9c26..d645a10616294a52e038d9fb7fb7cc2f8fe24f33 100644 --- a/compile_colibri.ml +++ b/tools/compile_colibri.ml @@ -27,7 +27,7 @@ let argspec = let () = Arg.parse (Arg.align argspec) - (fun s -> invalid_arg "No anonymous argument") + (fun _ -> invalid_arg "No anonymous argument") "compile_colibri" let arch = if Sys.win32 then "x86_64_nt" else "x86_64_linux" diff --git a/tools/compile_colibri.opam b/tools/compile_colibri.opam new file mode 100644 index 0000000000000000000000000000000000000000..18832f1c0553ca73d10f1aa3cc215ad3b2ba8577 --- /dev/null +++ b/tools/compile_colibri.opam @@ -0,0 +1,27 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "0.4.0" +synopsis: "Compile all dependencies for colibri" +maintainer: ["Christophe Junke"] +authors: ["François Bobot" "Bruno Marre" "Christophe Junke"] +license: "MIT" +homepage: "https://colibri.frama-c.com" +bug-reports: "https://git.frama-c.com/pub/colibri/issues" +depends: [ + "dune" {>= "3.0"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] diff --git a/tools/dune b/tools/dune new file mode 100644 index 0000000000000000000000000000000000000000..d43eeb7f1b09e90bf855a262c73112fc2a03eb01 --- /dev/null +++ b/tools/dune @@ -0,0 +1,20 @@ +(env + (static + (ocamlopt_flags + :standard -O3 + -ccopt -static + -ccopt -no-pie)) + (_ (ocamlopt_flags + :standard -O3))) + +(executable + (public_name colibri_for_bundle) + (package colibri_for_bundle) + (modules colibri_for_bundle) + (libraries unix)) + +(executable + (public_name compile_colibri) + (package compile_colibri) + (modules compile_colibri) + (libraries unix)) diff --git a/tools/dune-project b/tools/dune-project new file mode 100644 index 0000000000000000000000000000000000000000..884f47590809911bab908bdb1b6838fef9aab4eb --- /dev/null +++ b/tools/dune-project @@ -0,0 +1,25 @@ +(lang dune 3.0) + +(name colibri_tools) +(version 0.4.0) +(license "MIT") + +(generate_opam_files true) +(strict_package_deps true) + +(authors "François Bobot" + "Bruno Marre" + "Christophe Junke") +(homepage "https://colibri.frama-c.com") +(bug_reports "https://git.frama-c.com/pub/colibri/issues") + +(package + (name colibri_for_bundle) + (synopsis "Executable around colibri when used in bundle") + (maintainers "Christophe Junke")) + +(package + (name compile_colibri) + (synopsis "Compile all dependencies for colibri") + (maintainers "Christophe Junke")) +