rpms/why/devel gwhy-2.17.patch, NONE, 1.1 why-2.17-Makefile.in.patch, NONE, 1.1 .cvsignore, 1.2, 1.3 import.log, 1.1, 1.2 sources, 1.2, 1.3 why.spec, 1.1, 1.2 gwhy-2.14.patch, 1.1, NONE why-2.14-Makefile.in.patch, 1.1, NONE
Alan Dunn
amdunn at fedoraproject.org
Wed Dec 24 16:37:35 UTC 2008
- Previous message (by thread): rpms/gxmms2/devel gxmms2.desktop, NONE, 1.1 gxmms2.spec, NONE, 1.1 import.log, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2
- Next message (by thread): rpms/why/F-10 gwhy-2.17.patch, NONE, 1.1 why-2.17-Makefile.in.patch, NONE, 1.1 .cvsignore, 1.2, 1.3 import.log, 1.1, 1.2 sources, 1.2, 1.3 why.spec, 1.1, 1.2 gwhy-2.14.patch, 1.1, NONE why-2.14-Makefile.in.patch, 1.1, NONE
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
Author: amdunn
Update of /cvs/pkgs/rpms/why/devel
In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv12932/devel
Modified Files:
.cvsignore import.log sources why.spec
Added Files:
gwhy-2.17.patch why-2.17-Makefile.in.patch
Removed Files:
gwhy-2.14.patch why-2.14-Makefile.in.patch
Log Message:
Changed patches slightly so that hunks match updated files in 2.17.
gwhy-2.17.patch:
--- NEW FILE gwhy-2.17.patch ---
--- bin/gwhy.sh 2008-12-17 10:03:20.000000000 -0500
+++ bin/gwhy.sh 2008-12-24 08:51:50.000000000 -0500
@@ -1,29 +1,44 @@
#!/bin/sh
-case $1 in
+if ! test $1; then
+file=`zenity --file-selection --title="Select the file you want to open with gwhy"`;
+else
+file=$1
+fi
+
+if test $file; then
+d=`dirname $file`
+cd $d
+fi
+
+case $file in
*.java)
- b=`basename $1 .java`
- krakatoa $1 || exit 1
+ b=`basename $file .java`
+ krakatoa $b.java || exit 1
echo "krakatoa on $b.java done"
jessie -locs $b.jloc -why-opt -split-user-conj $b.jc || exit 2
echo "jessie done"
make -f $b.makefile gui
;;
*.c)
- b=`basename $1 .c`
- caduceus -why-opt -split-user-conj $1 || exit 1
+ b=`basename $file .c`
+ caduceus -why-opt -split-user-conj $b.c
make -f $b.makefile gui
;;
*.jc)
- b=`basename $1 .jc`
+ b=`basename $file .jc`
jessie $b.jc || exit 1
make -f $b.makefile gui
;;
*.mlw|*.why)
- gwhy-bin -split-user-conj $1
+ b=`basename $file`
+ gwhy-bin -split-user-conj $b
+ ;;
+ ?*)
+ echo "$file does not have file type extension recognized by gwhy"
;;
*)
- echo "don't know what to do with $1"
+ echo "gwhy needs the name of a file to inspect in order to run"
esac
why-2.17-Makefile.in.patch:
--- NEW FILE why-2.17-Makefile.in.patch ---
--- Makefile.in.backup 2008-12-24 06:39:04.000000000 -0500
+++ Makefile.in 2008-12-24 06:41:47.000000000 -0500
@@ -175,6 +175,7 @@
bin/why-config.opt: $(WHYCONFIGCMX)
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ unix.cmxa str.cmxa $^
$(STRIP) $@
+ execstack -c $@
bin/why-config.byte: $(WHYCONFIGCMO)
# $(if $(QUIET), at echo 'Linking $@' &&)
@@ -207,6 +208,7 @@
bin/why.opt: $(CMX) src/why.cmx
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ unix.cmxa str.cmxa nums.cmxa graph.cmxa $^
$(STRIP) $@
+ execstack -c $@
bin/why.byte: $(CMO) src/why.cmo
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) -o $@ unix.cma str.cma nums.cma graph.cma $^
@@ -257,6 +259,7 @@
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLOPT) \
$(OFLAGS) -o $@ unix.cmxa str.cmxa graph.cmxa $^
$(STRIP) $@
+ execstack -c $@
bin/caduceus.byte: $(CCMA) $(CCMO)
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLC) \
@@ -317,6 +320,7 @@
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) $(APRONLIB) $(APRONLIBS) $(ATPLIB) -o $@ \
unix.cmxa nums.cmxa graph.cmxa $^
$(STRIP) $@
+ execstack -c $@
bin/jessie.byte: $(JCCMO)
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) $(APRONLIB) $(APRONBYTLIBS) $(ATPLIB) -o $@ \
@@ -345,6 +349,7 @@
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ \
unix.cmxa nums.cmxa graph.cmxa $^
$(STRIP) $@
+ execstack -c $@
bin/krakatoa.byte: $(KCMO)
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) -o $@ \
@@ -504,6 +509,7 @@
bin/gwhy.opt: $(GCMX)
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ unix.cmxa threads.cmxa nums.cmxa str.cmxa graph.cmxa lablgtk.cmxa gtkThread.cmx $^
$(STRIP) $@
+ execstack -c $@
bin/gwhy.byte: $(GCMO)
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) -o $@ unix.cma str.cma nums.cma graph.cma lablgtk.cma threads.cma gtkThread.cmo $^
@@ -520,6 +526,7 @@
bin/why2html.opt: tools/why2html.ml
$(OCAMLOPT) $(OFLAGS) -o $@ $^
+ execstack -c $@
SIMPLIFYTOWHYCMO=src/ident.cmo src/pp.cmo \
tools/simplify_parser.cmo tools/simplify_lexer.cmo \
@@ -531,6 +538,7 @@
bin/simplify2why.opt: $(SIMPLIFYTOWHYCMX)
$(OCAMLOPT) $(OFLAGS) -o $@ $^
+ execstack -c $@
DPCMO = tools/cvcl_split.cmo tools/simplify_split.cmo tools/smtlib_split.cmo\
tools/zenon_split.cmo tools/ergo_split.cmo tools/rv_split.cmo \
@@ -543,6 +551,7 @@
bin/why-dp.opt: $(DPCMX)
$(OCAMLOPT) $(OFLAGS) -o $@ unix.cmxa str.cmxa $^
+ execstack -c $@
bin/why-cpulimit: tools/@CPULIMIT at .c
$(CC) -o $@ $^
@@ -552,6 +561,7 @@
bin/rv_merge.opt: tools/rv_merge.ml
$(OCAMLOPT) $(OFLAGS) -o $@ $^
+ execstack -c $@
OBFCMO=src/pp.cmo src/loc.cmo src/ident.cmo src/float_lexer.cmo \
src/parser.cmo src/lexer.cmo tools/obfuscator.cmo
@@ -562,6 +572,7 @@
bin/why-obfuscator.opt: $(OBFCMX)
$(OCAMLOPT) $(OFLAGS) -o $@ $^
+ execstack -c $@
STATCMO=src/pp.cmo src/loc.cmo src/ident.cmo src/float_lexer.cmo \
src/parser.cmo src/lexer.cmo tools/whystat.cmo
@@ -572,6 +583,7 @@
bin/why-stat.opt: $(STATCMX)
$(OCAMLOPT) $(OFLAGS) -o $@ $^
+ execstack -c $@
TOOLCMO=src/loc.cmo src/pp.cmo tools/toolstat_pars.cmo \
tools/toolstat_lex.cmo tools/toolstat.cmo
@@ -760,15 +772,9 @@
cp -f $(V7FILES) $(LIBDIR)/why/coq7
cp -f $(VO7) $(LIBDIR)/why/coq7
install-coq-v8:
- if test -w $(COQLIB) ; then \
- mkdir -p $(COQLIB)/user-contrib ; \
- cp -f $(V8FILES) $(COQLIB)/user-contrib ; \
- cp -f $(VO8) $(COQLIB)/user-contrib ; \
- else \
- echo "Cannot copy to Coq standard library. Add $(LIBDIR)/why/coq to Coq include path." ;\
- mkdir -p $(LIBDIR)/why/coq ;\
- cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\
- fi
+ mkdir -p $(COQLIB)/user-contrib
+ cp -f $(V8FILES) $(COQLIB)/user-contrib
+ cp -f $(VO8) $(COQLIB)/user-contrib
install-pvs-no:
install-pvs-yes: $(PVSFILES)
Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/why/devel/.cvsignore,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -r1.2 -r1.3
--- .cvsignore 5 Aug 2008 16:49:17 -0000 1.2
+++ .cvsignore 24 Dec 2008 16:37:05 -0000 1.3
@@ -1,2 +1,2 @@
krakatoa.pdf
-why-2.14.tar.gz
+why-2.17.tar.gz
Index: import.log
===================================================================
RCS file: /cvs/pkgs/rpms/why/devel/import.log,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- import.log 5 Aug 2008 16:49:17 -0000 1.1
+++ import.log 24 Dec 2008 16:37:05 -0000 1.2
@@ -1 +1,2 @@
why-2_14-2_fc9:HEAD:why-2.14-2.fc9.src.rpm:1217954050
+why-2_17-1_fc11:HEAD:why-2.17-1.fc11.src.rpm:1230136029
Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/why/devel/sources,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -r1.2 -r1.3
--- sources 5 Aug 2008 16:49:17 -0000 1.2
+++ sources 24 Dec 2008 16:37:05 -0000 1.3
@@ -1,2 +1,2 @@
56c2e53b7ef4dae8afe4e8264ac44419 krakatoa.pdf
-d88c0577f2af4ae73631f42e2695cac0 why-2.14.tar.gz
+8508024cf174f03c463d5560318ce6b5 why-2.17.tar.gz
Index: why.spec
===================================================================
RCS file: /cvs/pkgs/rpms/why/devel/why.spec,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- why.spec 5 Aug 2008 16:49:17 -0000 1.1
+++ why.spec 24 Dec 2008 16:37:05 -0000 1.2
@@ -1,12 +1,12 @@
Name: why
-Version: 2.14
-Release: 2%{?dist}
+Version: 2.17
+Release: 1%{?dist}
Summary: Why software verification platform
Group: Applications/Engineering
License: GPLv2
URL: http://why.lri.fr/
-Source0: http://why.lri.fr/download/why-2.14.tar.gz
+Source0: http://why.lri.fr/download/why-%{version}.tar.gz
Source1: README.why-gwhy.Fedora
Source2: README.why-coq.Fedora
Source3: README.why
@@ -16,12 +16,23 @@
Source7: min_why.why.result
Source8: http://caduceus.lri.fr/manual/caduceus.ps
Source9: http://gforge.inria.fr/docman/view.php/999/5097/krakatoa.pdf
-Patch0: gwhy-2.14.patch
-Patch1: why-2.14-Makefile.in.patch
+Patch0: gwhy-%{version}.patch
+Patch1: why-%{version}-Makefile.in.patch
Patch2: why-config.patch
BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
BuildRequires: ocaml >= 3.09, ocaml-camlp4-devel, gtk2-devel, ocaml-lablgtk-devel, desktop-file-utils, dos2unix, prelink, coq
+%if 0%{?fedora} < 9
+# There's no ocaml for ppc64 in Fedora <= 8
+ExcludeArch: ppc64
+%endif
+
+%if 0%{?fedora} == 11
+# Encountering an odd ocaml ppc64 bug in F11 and don't want to stall the other platforms
+# bz:
+ExcludeArch: ppc64
+%endif
+
%description
Why is a software verification platform that applies formal proving
tools to annotated programs. It is currently capable of analysis of C
@@ -112,7 +123,7 @@
%else
%define why bin/why.byte
%endif
-export WHYLIB=lib/why
+export WHYLIB=lib
%why --why --output min min.mlw
unset WHYLIB
diff min_why.why min_why.why.result > /dev/null
@@ -142,7 +153,7 @@
mkdir -p %{buildroot}%{why_examples_dir}mlw/
mkdir -p %{buildroot}%{why_examples_dir}c/
cp -p doc/manual.ps %{buildroot}%{why_doc_dir}why-manual.ps
-cp -p caduceus.ps krakatoa.pdf README.why COPYING GPL %{buildroot}%{why_doc_dir}
+cp -p caduceus.ps krakatoa.pdf README.why COPYING LICENSE %{buildroot}%{why_doc_dir}
# Copy in the example files after converting to proper UTF-8, fix line
# encodings, leaving behind all generated files
@@ -173,14 +184,15 @@
%{_bindir}/*
%exclude %{_bindir}/gwhy*
# Data for programs
-%{_datadir}/why
+%{why_data_dir}
+%exclude %{why_data_dir}/gwhy-icon.png
%{_datadir}/caduceus
-%{_datadir}/jessie
-%{_datadir}/krakatoa
-%exclude %{_datadir}/jessie/jc.cmo
-%if %opt
-%exclude %{_datadir}/jessie/jc.cmx
-%endif
+# % {_datadir}/jessie
+# % {_datadir}/krakatoa
+# % exclude % {_datadir}/jessie/jc.cmo
+# % if % opt
+# % exclude % {_datadir}/jessie/jc.cmx
+# % endif
# Man page
%{_mandir}/man1/why.1.gz
# Documentation and examples
@@ -199,17 +211,30 @@
%files coq
%defattr(-,root,root,-)
+%dir %{_datadir}/coq
+%dir %{_datadir}/coq/user-contrib
%{_datadir}/coq/user-contrib/Why*
-%exclude %{_datadir}/coq/user-contrib/Why*.v
+# % exclude % {_datadir}/coq/user-contrib/Why*.v
%{_datadir}/coq/user-contrib/caduceus*
-%exclude %{_datadir}/coq/user-contrib/caduceus*.v
+# % exclude % {_datadir}/coq/user-contrib/caduceus*.v
%{_datadir}/coq/user-contrib/Caduceus.v*
-%exclude %{_datadir}/coq/user-contrib/Caduceus.v
+# %exclude % {_datadir}/coq/user-contrib/Caduceus.v
%{_datadir}/coq/user-contrib/jessie_why.v*
-%exclude %{_datadir}/coq/user-contrib/jessie_why.v
+# % exclude % {_datadir}/coq/user-contrib/jessie_why.v
+%{_datadir}/coq/jessie_why.v*
%doc README.why-coq.Fedora
%changelog
+* Wed Dec 24 2008 Alan Dunn <amdunn at gmail.com> 2.17-1
+- Upgrade to version 2.17 (bz: 477790)
+- Add ownership of two directories common with Coq, but neither program requires the other (bz: 474016)
+- Minor filename change in 2.17 (GPL -> LICENSE)
+- Added back Coq .v files to match policy for Coq
+- Changed directory structure re: jessie and krakatoa to match new structure in 2.17
+- Minor changes to patches to ensure they still work in 2.17
+- Corrected package location gwhy-icon.png (should only be in gwhy)
+* Tue Aug 5 2008 Alan Dunn <amdunn at gmail.com> 2.14-2.1
+- ExcludeArch ppc64 on Fedora 8 due to no ocaml.
* Fri Aug 1 2008 Alan Dunn <amdunn at gmail.com> 2.14-2
- Fixed minor issues in response to package review:
- Inclusion of COPYING, GPL license-related files
--- gwhy-2.14.patch DELETED ---
--- why-2.14-Makefile.in.patch DELETED ---
- Previous message (by thread): rpms/gxmms2/devel gxmms2.desktop, NONE, 1.1 gxmms2.spec, NONE, 1.1 import.log, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2
- Next message (by thread): rpms/why/F-10 gwhy-2.17.patch, NONE, 1.1 why-2.17-Makefile.in.patch, NONE, 1.1 .cvsignore, 1.2, 1.3 import.log, 1.1, 1.2 sources, 1.2, 1.3 why.spec, 1.1, 1.2 gwhy-2.14.patch, 1.1, NONE why-2.14-Makefile.in.patch, 1.1, NONE
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
More information about the fedora-extras-commits
mailing list