[Pkg-ocaml-maint-commits] [frama-c] 02/07: Add 2 new fixes from upstream's repository
Mehdi Dogguy
mehdi at moszumanska.debian.org
Sun Sep 10 11:59:28 UTC 2017
This is an automated email from the git hooks/post-receive script.
mehdi pushed a commit to branch master
in repository frama-c.
commit 8684293d3be55e5498d765cd3d0b0e35c183db09
Author: Mehdi Dogguy <mehdi at debian.org>
Date: Sun Sep 10 12:32:26 2017 +0200
Add 2 new fixes from upstream's repository
---
...0009-Better-handling-of-dynlink-detection.patch | 235 +++++++++++++++++++++
debian/patches/0010-Add-zsh-completion-file.patch | 185 ++++++++++++++++
debian/patches/series | 2 +
3 files changed, 422 insertions(+)
diff --git a/debian/patches/0009-Better-handling-of-dynlink-detection.patch b/debian/patches/0009-Better-handling-of-dynlink-detection.patch
new file mode 100644
index 0000000..3d9ec05
--- /dev/null
+++ b/debian/patches/0009-Better-handling-of-dynlink-detection.patch
@@ -0,0 +1,235 @@
+From: Mehdi Dogguy <mehdi at debian.org>
+Date: Sun, 10 Sep 2017 12:27:25 +0200
+Subject: Better handling of dynlink detection
+
+---
+ configure | 70 ++++++++++++++++++++++++++++++++++++------------------------
+ configure.in | 63 ++++++++++++++++++++++++++++++++----------------------
+ 2 files changed, 80 insertions(+), 53 deletions(-)
+
+diff --git a/configure b/configure
+index 687ec71..285b4ea 100755
+--- a/configure
++++ b/configure
+@@ -2881,11 +2881,34 @@ $as_echo "ok" >&6; }
+ fi
+ fi
+
++# In case we have a native compiler, check that native dynlink works.
++# Otherwise, fall back to bytecode-only compilation
++
++if test "$OCAMLBEST" = opt; then
++ echo "let f x y =" > test_dynlink.ml
++ echo " Dynlink.loadfile \"foo\"; " >> test_dynlink.ml
++ echo " ignore (Dynlink.is_native);" >> test_dynlink.ml
++ echo " abs_float (x -. y)" >> test_dynlink.ml
++ if ($OCAMLOPT -shared -linkall -o test_dynlink.cmxs test_dynlink.ml) \
++ 2> /dev/null ; \
++then
++ { $as_echo "$as_me:${as_lineno-$LINENO}: result: native dynlink works fine. Great." >&5
++$as_echo "native dynlink works fine. Great." >&6; }
++else
++ { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Native dynlink does not work, disabling native compilation." >&5
++$as_echo "$as_me: WARNING: Native dynlink does not work, disabling native compilation." >&2;}
++ OCAMLBEST=byte
++fi
++rm -f test_dynlink.*
++fi
++
+ if test "$OCAMLBEST" = "opt"; then
+ LIB_SUFFIX=cmxa
++ DYN_SUFFIX=cmxs
+ OBJ_SUFFIX=cmx;
+ else
+ LIB_SUFFIX=cma
++ DYN_SUFFIX=cma
+ OBJ_SUFFIX=cmo;
+ fi
+
+@@ -3370,7 +3393,7 @@ fi
+ $as_echo_n "checking for Apron... " >&6; }
+
+ APRON_PATH=$($OCAMLFIND query apron 2>/dev/null | tr -d '\r\n')
+-if test -f "$APRON_PATH/apron.cmxs"; then
++if test -f "$APRON_PATH/apron.$DYN_SUFFIX"; then
+ HAS_APRON="yes";
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: found" >&5
+ $as_echo "found" >&6; }
+@@ -3396,7 +3419,7 @@ if test "$ENABLE_LANDMARKS" = yes ; then
+ $as_echo_n "checking for Landmarks... " >&6; }
+ LANDMARKS_PATH=$($OCAMLFIND query landmarks 2>/dev/null | tr -d '\r\n')
+ LANDMARKS_PPX_PATH=$($OCAMLFIND query landmarks.ppx 2>/dev/null | tr -d '\r\n')
+- if test -f "$LANDMARKS_PATH/landmarks.cmxs" -a -f "$LANDMARKS_PPX_PATH/ppx_landmarks"; then
++ if test -f "$LANDMARKS_PATH/landmarks.$DYN_SUFFIX" -a -f "$LANDMARKS_PPX_PATH/ppx_landmarks"; then
+ HAS_LANDMARKS="yes";
+ { $as_echo "$as_me:${as_lineno-$LINENO}: result: found" >&5
+ $as_echo "found" >&6; }
+@@ -3482,22 +3505,26 @@ $as_echo "Unix" >&6; }
+ EXE=
+ fi
+
+- # OCaml native threads
+- { $as_echo "$as_me:${as_lineno-$LINENO}: checking OCaml native threads" >&5
++ if test "$OCAMLBEST" = opt; then
++ # OCaml native threads
++ { $as_echo "$as_me:${as_lineno-$LINENO}: checking OCaml native threads" >&5
+ $as_echo_n "checking OCaml native threads... " >&6; }
+- echo "let f = Thread.create (fun () -> ())" > test_native_threads.ml
+- if ($OCAMLOPT -thread -o test_native_threads unix.cmxa threads.cmxa \
+- test_native_threads.ml) 2> /dev/null ; \
+- then
+- HAS_NATIVE_THREADS=yes
+- { $as_echo "$as_me:${as_lineno-$LINENO}: result: ok." >&5
+-$as_echo "ok." >&6; }
++ echo "let f = Thread.create (fun () -> ())" > test_native_threads.ml
++ if ($OCAMLOPT -thread -o test_native_threads unix.cmxa threads.cmxa \
++ test_native_threads.ml) 2> /dev/null ;
++ then
++ HAS_NATIVE_THREADS=yes
++ { $as_echo "$as_me:${as_lineno-$LINENO}: result: ok." >&5
++$as_echo "ok." >&6; };
++ else
++ HAS_NATIVE_THREADS=no
++ { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: unsupported." >&5
++$as_echo "$as_me: WARNING: unsupported." >&2;};
++ fi
++ rm -f test_native_threads*;
+ else
+- HAS_NATIVE_THREADS=no
+- { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: unsupported." >&5
+-$as_echo "$as_me: WARNING: unsupported." >&2;}
++ HAS_NATIVE_THREADS=no; # no native compilation anyway
+ fi
+- rm -f test_native_threads*
+ fi
+
+ # C and POSIX standard headers used by C bindings.
+@@ -11175,19 +11202,6 @@ fi
+ # Checking some other things which cannot be done too early
+ ###########################################################
+
+-# Check that native dynlink works
+-
+-echo "let f x y = Dynlink.loadfile \"foo\"; ignore (Dynlink.is_native); abs_float (x -. y)" > test_dynlink.ml
+-if ($OCAMLOPT -shared -linkall -o test_dynlink.cmxs test_dynlink.ml) \
+- 2> /dev/null ; \
+-then
+- { $as_echo "$as_me:${as_lineno-$LINENO}: result: native dynlink works fine. Great." >&5
+-$as_echo "native dynlink works fine. Great." >&6; }
+-else
+- as_fn_error $? "native dynlink does not work." "$LINENO" 5
+-fi
+-rm -f test_dynlink.*
+-
+ # Native version of ptests can be used only if
+ # - a native compiler exists
+ # - native threads are usable
+diff --git a/configure.in b/configure.in
+index e695815..98d46fc 100644
+--- a/configure.in
++++ b/configure.in
+@@ -138,11 +138,32 @@ else
+ fi
+ fi
+
++# In case we have a native compiler, check that native dynlink works.
++# Otherwise, fall back to bytecode-only compilation
++
++if test "$OCAMLBEST" = opt; then
++ echo "let f x y =" > test_dynlink.ml
++ echo " Dynlink.loadfile \"foo\"; " >> test_dynlink.ml
++ echo " ignore (Dynlink.is_native);" >> test_dynlink.ml
++ echo " abs_float (x -. y)" >> test_dynlink.ml
++ if ($OCAMLOPT -shared -linkall -o test_dynlink.cmxs test_dynlink.ml) \
++ 2> /dev/null ; \
++then
++ AC_MSG_RESULT([native dynlink works fine. Great.])
++else
++ AC_MSG_WARN([Native dynlink does not work, disabling native compilation.])
++ OCAMLBEST=byte
++fi
++rm -f test_dynlink.*
++fi
++
+ if test "$OCAMLBEST" = "opt"; then
+ LIB_SUFFIX=cmxa
++ DYN_SUFFIX=cmxs
+ OBJ_SUFFIX=cmx;
+ else
+ LIB_SUFFIX=cma
++ DYN_SUFFIX=cma
+ OBJ_SUFFIX=cmo;
+ fi
+
+@@ -286,7 +307,7 @@ AC_CHECK_PROG(OTAGS,otags,otags,)
+ AC_MSG_CHECKING(for Apron)
+
+ APRON_PATH=$($OCAMLFIND query apron 2>/dev/null | tr -d '\r\n')
+-if test -f "$APRON_PATH/apron.cmxs"; then
++if test -f "$APRON_PATH/apron.$DYN_SUFFIX"; then
+ HAS_APRON="yes";
+ AC_MSG_RESULT(found)
+ else
+@@ -307,7 +328,7 @@ if test "$ENABLE_LANDMARKS" = yes ; then
+ AC_MSG_CHECKING(for Landmarks)
+ LANDMARKS_PATH=$($OCAMLFIND query landmarks 2>/dev/null | tr -d '\r\n')
+ LANDMARKS_PPX_PATH=$($OCAMLFIND query landmarks.ppx 2>/dev/null | tr -d '\r\n')
+- if test -f "$LANDMARKS_PATH/landmarks.cmxs" -a -f "$LANDMARKS_PPX_PATH/ppx_landmarks"; then
++ if test -f "$LANDMARKS_PATH/landmarks.$DYN_SUFFIX" -a -f "$LANDMARKS_PPX_PATH/ppx_landmarks"; then
+ HAS_LANDMARKS="yes";
+ AC_MSG_RESULT(found)
+ else
+@@ -349,19 +370,23 @@ else
+ EXE=
+ fi
+
+- # OCaml native threads
+- AC_MSG_CHECKING([OCaml native threads])
+- echo "let f = Thread.create (fun () -> ())" > test_native_threads.ml
+- if ($OCAMLOPT -thread -o test_native_threads unix.cmxa threads.cmxa \
+- test_native_threads.ml) 2> /dev/null ; \
+- then
+- HAS_NATIVE_THREADS=yes
+- AC_MSG_RESULT([ok.])
++ if test "$OCAMLBEST" = opt; then
++ # OCaml native threads
++ AC_MSG_CHECKING([OCaml native threads])
++ echo "let f = Thread.create (fun () -> ())" > test_native_threads.ml
++ if ($OCAMLOPT -thread -o test_native_threads unix.cmxa threads.cmxa \
++ test_native_threads.ml) 2> /dev/null ;
++ then
++ HAS_NATIVE_THREADS=yes
++ AC_MSG_RESULT([ok.]);
++ else
++ HAS_NATIVE_THREADS=no
++ AC_MSG_WARN([unsupported.]);
++ fi
++ rm -f test_native_threads*;
+ else
+- HAS_NATIVE_THREADS=no
+- AC_MSG_WARN([unsupported.])
++ HAS_NATIVE_THREADS=no; # no native compilation anyway
+ fi
+- rm -f test_native_threads*
+ fi
+
+ # C and POSIX standard headers used by C bindings.
+@@ -875,18 +900,6 @@ configure_tool([DOT],[dot],[dot not found: you should install GraphViz],no)
+ # Checking some other things which cannot be done too early
+ ###########################################################
+
+-# Check that native dynlink works
+-
+-echo "let f x y = Dynlink.loadfile \"foo\"; ignore (Dynlink.is_native); abs_float (x -. y)" > test_dynlink.ml
+-if ($OCAMLOPT -shared -linkall -o test_dynlink.cmxs test_dynlink.ml) \
+- 2> /dev/null ; \
+-then
+- AC_MSG_RESULT([native dynlink works fine. Great.])
+-else
+- AC_MSG_ERROR([native dynlink does not work.])
+-fi
+-rm -f test_dynlink.*
+-
+ # Native version of ptests can be used only if
+ # - a native compiler exists
+ # - native threads are usable
diff --git a/debian/patches/0010-Add-zsh-completion-file.patch b/debian/patches/0010-Add-zsh-completion-file.patch
new file mode 100644
index 0000000..9d5dad1
--- /dev/null
+++ b/debian/patches/0010-Add-zsh-completion-file.patch
@@ -0,0 +1,185 @@
+From: Mehdi Dogguy <mehdi at debian.org>
+Date: Sun, 10 Sep 2017 12:28:35 +0200
+Subject: Add zsh completion file
+
+---
+ Makefile | 3 +-
+ share/_frama-c | 148 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+ 2 files changed, 150 insertions(+), 1 deletion(-)
+ create mode 100644 share/_frama-c
+
+diff --git a/Makefile b/Makefile
+index 1fdf715..6651900 100644
+--- a/Makefile
++++ b/Makefile
+@@ -231,6 +231,7 @@ DISTRIB_FILES:=\
+ VERSION $(wildcard licenses/*) \
+ $(LIBC_FILES) \
+ $(wildcard share/emacs/*.el) share/autocomplete_frama-c \
++ share/_frama-c \
+ share/configure.ac \
+ share/Makefile.config.in share/Makefile.common \
+ share/Makefile.generic \
+@@ -1535,7 +1536,7 @@ install:: install-lib
+ $(wildcard share/*.c share/*.h) \
+ share/Makefile.dynamic share/Makefile.plugin.template share/Makefile.kernel \
+ share/Makefile.config share/Makefile.common share/Makefile.generic \
+- share/configure.ac share/autocomplete_frama-c \
++ share/configure.ac share/autocomplete_frama-c share/_frama-c \
+ $(FRAMAC_DATADIR)
+ $(MKDIR) $(FRAMAC_DATADIR)/emacs
+ $(CP) $(wildcard share/emacs/*.el) $(FRAMAC_DATADIR)/emacs
+diff --git a/share/_frama-c b/share/_frama-c
+new file mode 100644
+index 0000000..51ac788
+--- /dev/null
++++ b/share/_frama-c
+@@ -0,0 +1,148 @@
++#compdef frama-c frama-c-gui frama-c.byte frama-c-gui.byte
++##########################################################################
++# #
++# This file is part of Frama-C. #
++# #
++# Copyright (C) 2007-2017 #
++# 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). #
++# #
++##########################################################################
++
++# zsh completion for Frama-C
++# ==========================
++#
++# Installation
++# ============
++#
++# This file must be placed in a directory listed in the $fpath variable.
++# You can add a directory to $fpath by adding a line like the following
++# to your ~/.zshrc file:
++#
++# fpath=(~/newdir $fpath)
++#
++# It also works with relative paths, such as 'bin/frama-c'.
++#
++#
++# The autocompletion can benefit from the caching system offered by zsh:
++# `zstyle ':completion:*' use-cache on` to enable caching for all commands
++# `zstyle ':completion:*:*:frama-c*:*' use-cache on` only for frama-c
++#
++# -----------------------------------------------------------------------------
++
++# TODO:
++# - use _call_program to call frama-c instead of calling frama-c directly ?
++# - other ideas when to renew cache ?
++
++#local curcontext="$curcontext" state state_descr line # expl ret=1 ??
++#typeset -A opt_args
++
++# filter_load takes a command line calling frama-c and
++# removes everything not a -load-module or -load-script
++# argument 1 is the variable name of the input
++# argument 2 is the variable name of the output
++function filter_load () {
++ local next=0
++ local -a my_args
++ my_args=(${(P)1[1]})
++ for w in ${(P)1}; do
++ if [[ $next -eq 1 ]]; then
++ my_args+=($w)
++ next=0
++ else
++ # very strange behaviour when ' is used instead of " around -load-*
++ # actually not related to this
++ if [[ $w = '-load-module' ]] || [[ $w = '-load-script' ]]; then
++ my_args+=("$w")
++ next=1
++ fi
++ fi
++ done
++ eval "$2=($my_args)"
++}
++
++function _frama_c () {
++ local ret=1 # the return value (1 if no autocompletion is done, 0 otherwise)
++
++ local -a my_words
++ my_words=($words)
++ my_words[1]=${my_words[1]//%-gui} # call frama-c instead of frama-c-gui
++
++ # we do not waste our time on computation if we are not completing an option
++ if [[ -prefix -* ]]; then # if the first character of the current word is a '-'
++ # is the first word on the line executable ?
++ if $my_words[1] 2>/dev/null; then
++ local -a the_args
++ local -a the_previous_args
++ # we keep only parts of the command line relevant to -load-module/-load-script
++ filter_load my_words the_args
++ # we load the previous filtered command from cache if available
++ _retrieve_cache frama-c_previous_command # can overwrite the_previous_args
++ # some gymnastics because the name of the variable matters
++ local -a tmp
++ tmp=($the_previous_args)
++ the_previous_args=($the_args)
++ _store_cache frama-c_previous_command the_previous_args
++ the_previous_args=($tmp)
++
++ # if the time of the most recent modification in
++ # `frama-c -print-plugin-path` is not the same as the one
++ # in the cache, we deduce that it is not the same "frama-c"
++ # as before and recompute the cache.
++ # We put the new date in the cache and store
++ # this information in $recompute
++ local last_change
++ _retrieve_cache frama-c_last_change
++ zmodload -F zsh/stat b:zstat 2>/dev/null
++ local current_last_change=$(zstat +mtime $($my_words[1] -print-plugin-path)/**/*(.om[1]))
++ local recompute
++ (( recompute = $current_last_change != ${last_change:-0} ))
++ if (( $recompute )); then
++ last_change=$current_last_change
++ _store_cache frama-c_last_change last_change
++ fi
++
++ # if something in `frama-c -print-plugin-path` changed,
++ # if the filtered current command is different from the remembered one or
++ # if the cache is unavailable, recompute the list of options,
++ # otherwise just load the cache
++ if (( $recompute )) ||
++ [[ $the_args != $the_previous_args ]] ||
++ _cache_invalid frama-c_autocompletion ||
++ ! _retrieve_cache frama-c_autocompletion
++ then
++ local -a autocompletion
++ local autocomp
++ # call frama-c with all the -load-module ; if it fails, test without the load-modules ;
++ # if it fails again, abort
++ autocomp=$($the_args -autocomplete 2>/dev/null) || autocomp=$($my_words[1] -autocomplete 2>/dev/null) || unset autocomp
++ (( $+autocomp )) && autocompletion=($(grep -o "\-[^ ]*" <<< $autocomp | sort))
++ (( $#autocompletion )) || _message "$my_words[1] exists, but no option was detected"
++ _store_cache frama-c_autocompletion autocompletion
++ fi
++ _describe 'options' autocompletion && ret=0
++ else
++ _message "$my_words[1] not found, dynamic autocompletion aborted"
++ _files && ret=0 # defaults to _files
++ fi
++ else
++ # if we complete a file (not sure if '_files' is the best default)
++ _files && ret=0
++ fi
++ return $ret
++}
++
++# call _frama_c when autocompletion is requested
++_frama_c "$@"
diff --git a/debian/patches/series b/debian/patches/series
index 20a6604..481369d 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -6,3 +6,5 @@
0006-gui.byte-needs-TARGETS_GUI_BYTE-only.patch
0007-Fix-FTBFS-with-OCaml-4.05.0.patch
0008-More-fixes-of-spelling-errors.patch
+0009-Better-handling-of-dynlink-detection.patch
+0010-Add-zsh-completion-file.patch
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/frama-c.git
More information about the Pkg-ocaml-maint-commits
mailing list