From 9640c1ab08d5ff414f8e7f260ecad54d586c9671 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 18 Jul 2024 11:27:28 +0200
Subject: [PATCH] [dev] add script to quickly produce Docker images from
current dev
---
dev/docker/Makefile | 4 ++++
dev/insta-docker-image.sh | 43 +++++++++++++++++++++++++++++++++++++++
dev/make-distrib.sh | 16 ++++++++++++---
3 files changed, 60 insertions(+), 3 deletions(-)
create mode 100755 dev/insta-docker-image.sh
diff --git a/dev/docker/Makefile b/dev/docker/Makefile
index 448e5ec9112..ecdf9e19a75 100644
--- a/dev/docker/Makefile
+++ b/dev/docker/Makefile
@@ -88,6 +88,10 @@ custom.% custom-gui.% custom-stripped.%:
exit 1
else
BUILD_ARGS += --build-arg=from_archive=$(FRAMAC_ARCHIVE)
+custom-fast.%: $(DEPS)
+ cp ../../reference-configuration.md .
+ $(DOCKER) build . -t frama-c-$@ $(BUILD_ARGS) --target frama-c
+
custom.%: $(DEPS)
cp ../../reference-configuration.md .
$(DOCKER) build . -t frama-c-$@ $(BUILD_ARGS) --target frama-c-slim
diff --git a/dev/insta-docker-image.sh b/dev/insta-docker-image.sh
new file mode 100755
index 00000000000..a360a027457
--- /dev/null
+++ b/dev/insta-docker-image.sh
@@ -0,0 +1,43 @@
+#!/usr/bin/bash -eu
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2024 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# Script used to quickly generate a Frama-C Docker image based on the
+# current state of the repository
+
+SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+
+cd "$SCRIPT_DIR/../"
+USE_STASH=yes dev/make-distrib.sh
+mv "frama-c-current.tar.gz" "$SCRIPT_DIR/docker/frama-c-current.tar.gz"
+cd "$SCRIPT_DIR/docker"
+FRAMAC_ARCHIVE="frama-c-current.tar.gz" make custom-fast.debian
+
+if command -v podman 2>&1; then
+ DOCKER=podman
+else
+ DOCKER=docker
+fi
+
+"$DOCKER" tag frama-c-custom-fast.debian frama-c-current
+
+echo "Created Docker image: frama-c-current"
diff --git a/dev/make-distrib.sh b/dev/make-distrib.sh
index f2e1da93bcb..2e599b39b4d 100755
--- a/dev/make-distrib.sh
+++ b/dev/make-distrib.sh
@@ -82,6 +82,7 @@ do
echo " VERSION_CODENAME=<name> (overriden by --codename)"
echo " OPEN_SOURCE=yes|no (overriden by --open-source and --closed-source)"
echo " CI_LINK=yes|no (also set by --ci-link)"
+ echo " USE_STASH=yes|no (default: no)"
echo ""
exit 0
;;
@@ -117,7 +118,11 @@ VERSION=$(cat VERSION)
VERSION_SAFE=${VERSION/~/-}
FRAMAC="frama-c-$VERSION_SAFE-$VERSION_CODENAME"
-FRAMAC_TAR="$FRAMAC.tar"
+if [ "$USE_STASH" == "yes" ]; then
+ FRAMAC_TAR="frama-c-current.tar"
+else
+ FRAMAC_TAR="$FRAMAC.tar"
+fi
################################################################################
# Check Opam file
@@ -164,7 +169,7 @@ echo "----------------------------------------------------------------"
# Warn if there are uncommitted changes (will not be taken into account)
GIT_STATUS="$(git status --porcelain -- $(sed 's/^./:!&/' <<< $EXTERNAL_PLUGINS))"
-if [ "" != "$GIT_STATUS" ]; then
+if [ "" != "$GIT_STATUS" -a "$USE_STASH" != "yes" ]; then
echo "WARNING: uncommitted changes will be IGNORED when making archive:"
echo "$GIT_STATUS" | sed 's/^/ /'
echo "----------------------------------------------------------------"
@@ -173,7 +178,12 @@ fi
################################################################################
# Prepare Archive
-git archive HEAD -o $FRAMAC_TAR --prefix "$FRAMAC/"
+# For the "instant Docker image" script: allow inclusion of uncommitted changes
+if [ "$USE_STASH" == "yes" ]; then
+ ARCHIVE_COMMIT=$(git stash create)
+fi
+
+git archive ${ARCHIVE_COMMIT:-HEAD} -o $FRAMAC_TAR --prefix "$FRAMAC/"
################################################################################
# Add external plugin to archive
--
GitLab