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 <[email protected]> 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 <[email protected]> +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 <[email protected]> +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 _______________________________________________ Pkg-ocaml-maint-commits mailing list [email protected] http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
