Skip to content

Commit

Permalink
Merge pull request #171 from imitator-model-checker/develop
Browse files Browse the repository at this point in the history
Develop
  • Loading branch information
etienneandre committed Mar 21, 2024
2 parents cf5c1f1 + a0fcfa0 commit 655201c
Show file tree
Hide file tree
Showing 777 changed files with 58,742 additions and 34,180 deletions.
3 changes: 2 additions & 1 deletion .dockerignore
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@
.dockerignore
.git
_oasis
bin
comparator
scripts
.gitignore
Expand All @@ -14,4 +13,6 @@ interfaceCV.py
LICENSE
paquito.yml
README.md
INSTALL.md
RELEASES.md
.DS_Store
11 changes: 0 additions & 11 deletions .github/patches/META.ppl.patch

This file was deleted.

99 changes: 24 additions & 75 deletions .github/patches/gmp.patch
Original file line number Diff line number Diff line change
@@ -1,12 +1,17 @@
diff --git a/Makefile b/Makefile
index 2e54a3c..b357aa7 100644
index 2e54a3c..6cee915 100644
--- a/Makefile
+++ b/Makefile
@@ -5,7 +5,7 @@ OCAML_LIBDIR:= $(shell ocamlc -where)
# GMP_INCLUDES= -I/opt/gmp-4.1.2/include -I/users/absint2/local/include -I$(HOME)/packages/gmp/include
@@ -2,10 +2,10 @@
RANLIB= ranlib

# GMP_LIBDIR=/opt/gmp-4.1.2/lib
OCAML_LIBDIR:= $(shell ocamlc -where)
-# GMP_INCLUDES= -I/opt/gmp-4.1.2/include -I/users/absint2/local/include -I$(HOME)/packages/gmp/include
+GMP_INCLUDES= -I$(shell brew --prefix)/include

-# GMP_LIBDIR=/opt/gmp-4.1.2/lib
-DESTDIR= $(OCAML_LIBDIR)/gmp
+GMP_LIBDIR= $(shell brew --prefix)/lib
+DESTDIR= $(shell opam var lib)/gmp

#RLIBFLAGS= -cclib "-Wl,-rpath $(GMP_LIBDIR)" # Linux, FreeBSD
Expand All @@ -16,80 +21,24 @@ index 2e54a3c..b357aa7 100644
# LIBFLAGS= -cclib -L. -cclib -L$(GMP_LIBDIR) $(RLIBFLAGS) \
# -cclib -lmpfr -cclib -lgmp -cclib -L$(DESTDIR)
-LIBFLAGS = -cclib -L$(shell pwd) -cclib -lgmp -cclib -lmpfr
+LIBFLAGS = -cclib -L. -cclib -lgmp -cclib -lmpfr
+LIBFLAGS = -cclib -L. -cclib -lgmp -cclib -lmpfr

#CC= icc
-CFLAGS_MISC= -Wall -Wno-unused -Werror -g -O3
+CFLAGS_MISC= -Wall -Wno-unused -Werror -g -O3 -Wno-incompatible-pointer-types-discards-qualifiers
+CFLAGS_MISC= -Wall -Wno-unused -Werror -g -O3 -fcommon
#CFLAGS_MISC=
CFLAGS_INCLUDE= -I $(OCAML_LIBDIR) $(GMP_INCLUDES)
CFLAGS= $(CFLAGS_MISC) $(CFLAGS_INCLUDE)
diff --git a/gmp.ml b/gmp.ml
index 678426d..c63d2b1 100644
--- a/gmp.ml
+++ b/gmp.ml
@@ -410,16 +410,18 @@ module F = struct
let to_string_base_digits ~base: base ~digits: digits x =
let mantissa, exponent =
to_string_exp_base_digits ~base: base ~digits: digits (abs x)
- in let sign = sgn x in
- if sign = 0 then "0" else
- ((if sign < 0 then "-" else "")
+ in
+ let sign = sgn x in
+ if sign = 0 then "0"
+ else
+ ((if sign < 0 then "-" else "")
^ (let lm=String.length mantissa
in if lm > 1
- then let tmp = String.create (succ lm)
- in String.blit mantissa 0 tmp 0 1;
- String.blit mantissa 1 tmp 2 (pred lm);
- String.set tmp 1 '.';
- tmp
+ then let tmp = Bytes.create (succ lm)
+ in Bytes.blit_string mantissa 0 tmp 0 1;
+ Bytes.blit_string mantissa 1 tmp 2 (pred lm);
+ Bytes.set tmp 1 '.';
+ Bytes.to_string tmp
else mantissa)
^ (if base <= 10 then "E" else "@")
^ (string_of_int (pred exponent)));;
@@ -603,19 +605,24 @@ module FR = struct
~base: base ~digits: digits x =
let mantissa, exponent =
to_string_exp_base_digits ~mode: mode ~base: base ~digits: digits x
- in let i = (if (sgn x) < 0 then 1 else 0) in
- (if mantissa = "Inf"
- then "Inf"
- else (let lm=String.length mantissa
- in if lm > 1
- then let tmp = String.create (succ lm)
- in String.blit mantissa 0 tmp 0 (1+i);
- String.blit mantissa (1+i) tmp (2+i) ((pred lm)-i);
- String.set tmp (1+i) '.';
- tmp
- else mantissa)
- ^ (if base <= 10 then "E" else "@")
- ^ (string_of_int (pred exponent)));;
+ in
+ let i = (if (sgn x) < 0 then 1 else 0) in
+ let prefix : string =
+ if mantissa = "Inf" then "Inf"
+ else
+ let lm=String.length mantissa in
+ if lm > 1 then
+ let tmp = Bytes.create (succ lm) in
+ Bytes.blit_string mantissa 0 tmp 0 (1+i);
+ Bytes.blit_string mantissa (1+i) tmp (2+i) ((pred lm)-i);
+ Bytes.set tmp (1+i) '.';
+ Bytes.to_string tmp
+ else mantissa
+ in
+ prefix
+ ^ (if base <= 10 then "E" else "@")
+ ^ (string_of_int (pred exponent))
+;;

let to_string = to_string_base_digits ~mode: GMP_RNDN ~base: 10 ~digits: 10;;

@@ -86,10 +86,10 @@
$(OCAMLOPT) $+ -o $@

test_suite: gmp.cma test_suite.cmo
- $(OCAMLC) -custom $+ -o $@
+ $(OCAMLC) -custom -I $(GMP_LIBDIR) $+ -o $@

test_suite.opt: gmp.cmxa test_suite.cmx
- $(OCAMLOPT) $+ -o $@
+ $(OCAMLOPT) -I $(GMP_LIBDIR) $+ -o $@

clean:
rm -f *.o *.cm* $(PROGRAMS) *.a
126 changes: 58 additions & 68 deletions .github/scripts/build.sh
Original file line number Diff line number Diff line change
@@ -1,86 +1,76 @@
# PPL version
PPL_VERSION=1.2
#!/bin/bash

# Patches folder
PATCH_FOLDER="${GITHUB_WORKSPACE}/.github/patches"
set -a

if [[ "$RUNNER_OS" = "Linux" ]]; then
sudo apt-get update -qq
sudo apt-get install -qq wget unzip curl build-essential g++ m4 ocaml-native-compilers camlp4-extra ocaml oasis ocaml-findlib \
libextlib-ocaml libextlib-ocaml-dev libfileutils-ocaml-dev \
libgmp-dev libgmp-ocaml libgmp-ocaml-dev libmpfr-dev \
libppl-dev \
graphviz plotutils
# check OS
case $(uname) in
'Linux')
RUNNER_OS='Linux'
;;
'Darwin')
RUNNER_OS='macOS'
;;
*)
echo "This script only supports Linux or OSX"
exit 1
;;
esac

if [[ "$DISTRIBUTED" = "True" ]]; then
sudo apt-get install -qq openmpi-bin openmpi-common libopenmpi-dev
# ignore sudo commands when the user is root
sudo() {
[[ $EUID = 0 ]] || set -- command sudo "$@"
"$@"
}

# installing version without Bytes package
git clone https://github.com/xavierleroy/ocamlmpi
(cd ocamlmpi; git reset --hard c6eaf91; make clean; make MPIINCDIR=/usr/lib/openmpi/include; make opt; sudo make install)
rm -rf ocamlmpi
# script folder
if [ -z "${GITHUB_WORKSPACE}" ]; then
SCRIPT_FOLDER=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" &>/dev/null && pwd)
PATCH_FOLDER="$(dirname $SCRIPT_FOLDER)/patches"
ROOT_FOLDER="$(dirname $(dirname $SCRIPT_FOLDER))"
cd "$ROOT_FOLDER"
else
SCRIPT_FOLDER="${GITHUB_WORKSPACE}/.github/scripts"
PATCH_FOLDER="${GITHUB_WORKSPACE}/.github/patches"
fi

# Installting Bytes Package
git clone https://github.com/chambart/ocaml-bytes.git
(cd ocaml-bytes; ./configure --prefix=/usr --libdir=/usr/lib/ocaml/; make; sudo make install)
rm -rf ocaml-bytes
fi
# install dependencies
if [[ "$RUNNER_OS" = "Linux" ]]; then
DEBIAN_FRONTEND=noninteractive
sudo apt-get update -qq
sudo apt-get install -qq wget unzip curl build-essential libtinfo-dev g++ m4 opam python3 \
libgmp-dev libmpfr-dev libppl-dev \
graphviz plotutils
elif [[ "$RUNNER_OS" = "macOS" ]]; then
brew install opam gmp plotutils ppl

# install opam and ocaml libraries
opam init -a
opam install -y extlib fileutils oasis
eval $(opam env)

# install mlgmp
git clone https://github.com/monniaux/mlgmp.git && cd mlgmp
git apply "${PATCH_FOLDER}/gmp.patch"
make && sudo make install && cd ..
rm -rf mlgmp
sudo cp METAS/META.gmp $(opam var lib)/gmp/META
brew install opam gmp ppl graphviz plotutils
fi

# installing PPL
wget -q --no-check-certificate https://www.bugseng.com/products/ppl/download/ftp/releases/${PPL_VERSION}/ppl-${PPL_VERSION}.zip
unzip -qq ppl-${PPL_VERSION}.zip
# python fix
[ ! -x "$(command -v python)" ] && sudo ln -s $(which python3) "/usr/bin/python"

cd ppl-${PPL_VERSION}
if [[ "$RUNNER_OS" = "Linux" ]]; then
./configure --prefix=/usr
elif [[ "$RUNNER_OS" = "macOS" ]]; then
# patch clang
patch -p0 < "${PATCH_FOLDER}/clang5.patch"
# install opam and ocaml libraries
[[ ${DOCKER_RUNNING} ]] && opam init -a --disable-sandboxing || opam init -a

# compile ppl
./configure --prefix=$(opam var prefix) --with-mlgmp=$(opam var lib)/gmp --disable-documentation --enable-interfaces=ocaml
make
fi
cd interfaces/OCaml && make -j 4 && sudo make install && cd ../../..
rm -rf ppl-${PPL_VERSION}*
opam install -y extlib fileutils oasis alcotest
eval $(opam env)

# Build IMITATOR
if [[ "$RUNNER_OS" = "Linux" ]]; then
sudo cp METAS/META.ppl /usr/lib/ocaml/METAS/
elif [[ "$RUNNER_OS" = "macOS" ]]; then
# patch oasis
patch -p0 < "${PATCH_FOLDER}/oasis-config.patch"
# install mlgmp
[ ! -d "$(opam var lib)/gmp" ] && bash "${SCRIPT_FOLDER}/install-mlgmp.sh"

# patch ppl META file
patch -p0 < "${PATCH_FOLDER}/META.ppl.patch"
# instal ppl
[ ! -d "$(opam var lib)/ppl" ] && bash "${SCRIPT_FOLDER}/install-ppl.sh"

echo $(ls -al)
sudo cp METAS/META.ppl $(opam var lib)/ppl/META
# patch oasis for OSX
if [[ "$RUNNER_OS" = "macOS" ]]; then
patch -p0 <"${PATCH_FOLDER}/oasis-config.patch"
fi

platform=`echo "${RUNNER_OS}" | awk '{print tolower($1)}'`
tag="${GITHUB_REF_NAME##*/}"
if [[ "$DISTRIBUTED" = "True" ]]; then
sh build-patator.sh
cd bin
mv "patator" "patator-${tag}-${platform}-amd64"
else
sh build.sh
# Build IMITATOR
dune build

# rename artefact
if [ ! -z "${GITHUB_WORKSPACE}" ]; then
cd bin
platform=$(echo "${RUNNER_OS}" | awk '{print tolower($1)}')
tag="${GITHUB_REF_NAME##*/}"
mv "imitator" "imitator-${tag}-${platform}-amd64"
fi
14 changes: 14 additions & 0 deletions .github/scripts/install-mlgmp.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
#!/bin/bash

# clone mlgmp from github
git clone https://github.com/monniaux/mlgmp.git && cd mlgmp

# apply patch for Ocaml > 4.05.0
git apply "${PATCH_FOLDER}/gmp.patch"

# compile and install
make && make install && cd ..
rm -rf mlgmp

# copy META file
cp METAS/META.gmp "$(opam var lib)/gmp/META"
27 changes: 27 additions & 0 deletions .github/scripts/install-ppl.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
#!/bin/bash

# PPL version
PPL_VERSION=1.2

# download PPL
wget -q --no-check-certificate https://www.bugseng.com/products/ppl/download/ftp/releases/${PPL_VERSION}/ppl-${PPL_VERSION}.zip
unzip -qq ppl-${PPL_VERSION}.zip

cd ppl-${PPL_VERSION}

# Patch clang for OSX
if [[ "$RUNNER_OS" = "macOS" ]]; then
# patch clang
patch -p0 <"${PATCH_FOLDER}/clang5.patch"
EXTRA_ARGS="--with-gmp=$(brew --prefix)"
fi

# compile ppl
./configure --prefix=$(opam var prefix) --with-mlgmp=$(opam var lib)/gmp ${EXTRA_ARGS} --disable-documentation --enable-interfaces=ocaml

# compile Ocaml interface
cd interfaces/OCaml && make -j 4 && make install && cd ../../..
rm -rf ppl-${PPL_VERSION}*

# copy META file
cp METAS/META.ppl "$(opam var lib)/ppl/META"
34 changes: 31 additions & 3 deletions .github/workflows/workflow.yml
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,9 @@ jobs:
fail-fast: false
matrix:
os:
- ubuntu-latest
- ubuntu-20.04
- macos-latest
runs-on: ${{ matrix.os }}
env:
DISTRIBUTED: False
steps:
# setup repository
- name: Checkout
Expand All @@ -39,6 +37,7 @@ jobs:
deploy:
if: startsWith(github.ref, 'refs/tags/')
name: Publish - Github Release
runs-on: ubuntu-latest
needs: build
steps:
Expand All @@ -59,3 +58,32 @@ jobs:
imitator-ubuntu-latest/doc/IMITATOR-not-developer-manual.pdf
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

docker:
if: startsWith(github.ref, 'refs/tags/') || (github.ref == 'refs/heads/develop')
name: Publish - Docker Hub
needs: build
runs-on: ubuntu-latest
steps:
- name: Check out the repo
uses: actions/checkout@v3

- name: Log in to Docker Hub
uses: docker/login-action@v2
with:
username: ${{ secrets.DOCKER_HUB_USERNAME }}
password: ${{ secrets.DOCKER_HUB_TOKEN }}

- name: Extract metadata (tags, labels) for Docker
id: meta
uses: docker/metadata-action@v4
with:
images: imitator/imitator

- name: Build and push Docker image
uses: docker/build-push-action@v4
with:
context: .
push: ${{ github.event_name != 'pull_request' }}
tags: ${{ steps.meta.outputs.tags }}
labels: ${{ steps.meta.outputs.labels }}
Loading

0 comments on commit 655201c

Please sign in to comment.