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

Wed Dec 24 16:41:48 UTC 2008

Author: amdunn

Update of /cvs/pkgs/rpms/why/F-10
In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv13599/F-10

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:
Minor changes in patches to allow them to still work properly, spec file
update, both for new version 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/F-10/.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:41:17 -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/F-10/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:41:17 -0000	1.2
@@ -1 +1,2 @@
 why-2_14-2_fc9:HEAD:why-2.14-2.fc9.src.rpm:1217954050
+why-2_17-1_fc10:F-10:why-2.17-1.fc10.src.rpm:1230136285


Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/why/F-10/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:41:17 -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/F-10/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:41:17 -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 ---


