From 6b871b2b1dfb5663da37fc48e10b4b7a6da74b56 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Jan=20R=C4=99korajski?= Date: Mon, 5 Jun 2017 23:25:41 +0000 Subject: [PATCH] - up to 8.6 --- coq-lablgtk2.patch | 66 +++++++++++++++------------------------------- coq.spec | 25 ++++++++---------- 2 files changed, 32 insertions(+), 59 deletions(-) diff --git a/coq-lablgtk2.patch b/coq-lablgtk2.patch index 1102759..3fa6075 100644 --- a/coq-lablgtk2.patch +++ b/coq-lablgtk2.patch @@ -1,46 +1,22 @@ ---- coq-8.1pl4/configure~ 2008-10-09 11:40:41.000000000 +0200 -+++ coq-8.1pl4/configure 2009-02-16 14:03:00.496249846 +0100 -@@ -634,7 +634,7 @@ - # Beware of the final \r in Win32 - lablgtkdirtmp="$(ocamlfind query lablgtk2 2> /dev/null | tr -d '\r')" - if [ "$lablgtkdirtmp" != "" ]; then -- if [ -f "$lablgtkdirtmp/glib.cmi" -a -f "$lablgtkdirtmp/glib.mli" ]; then -+ if [ -f "$lablgtkdirtmp/glib.cmi" -o -f "$lablgtkdirtmp/glib.mli" ]; then - lablgtkdirfoundmsg="LabelGtk2 found by ocamlfind" - lablgtkdir=$lablgtkdirtmp - LABLGTKLIB=$lablgtkdir # Pour le message utilisateur -@@ -652,7 +652,7 @@ - echo "$lablgtkdir is not a valid directory." - echo "Configuration script failed!" - exit 1 -- elif [ -f "$lablgtkdir/glib.cmi" -a -f "$lablgtkdir/glib.mli" ]; then -+ elif [ -f "$lablgtkdir/glib.cmi" -o -f "$lablgtkdir/glib.mli" ]; then - lablgtkdirfoundmsg="LablGtk2 directory found" - LABLGTKLIB=$lablgtkdir # Pour le message utilisateur - else -@@ -664,9 +664,6 @@ - if [ "$lablgtkdir" = "" ]; then - echo "LablGtk2 not found: CoqIde will not be available." - COQIDE=no -- elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then -- echo "$lablgtkdirfoundmsg but too old: CoqIde will not be available." -- COQIDE=no; - elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then - echo "$lablgtkdirfoundmsg, bytecode CoqIde will be used as requested." - COQIDE=byte -@@ -855,15 +852,7 @@ - #################################################### +--- coq-8.6/configure.ml~ 2016-12-08 15:13:52.000000000 +0000 ++++ coq-8.6/configure.ml 2017-06-05 23:04:32.311195087 +0000 +@@ -669,8 +669,8 @@ + yell (sprintf "No such directory '%s' (%s)." dir msg) + else if not (Sys.file_exists (dir/"gSourceView2.cmi")) then + yell (sprintf "Incomplete LablGtk2 (%s): no %s/gSourceView2.cmi." msg dir) +- else if not (Sys.file_exists (dir/"glib.mli")) then +- yell (sprintf "Incomplete LablGtk2 (%s): no %s/glib.mli." msg dir) ++ else if not (Sys.file_exists (dir/"glib.cmi")) then ++ yell (sprintf "Incomplete LablGtk2 (%s): no %s/glib.cmi." msg dir) + else true - if [ ! "$COQIDE" = "no" ]; then -- if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then -- if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then - cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli -- else -- cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli -- fi -- else -- cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli -- fi - fi - - ################################################## + (** Detect and/or verify the Lablgtk2 location *) +@@ -701,7 +701,7 @@ + | Manual | Stdlib -> + let test accu f = + if accu then +- let test = sprintf "grep -q -w %s %S/glib.mli" f dir in ++ let test = sprintf "grep -q -w %s %S/glib.cmi" f dir in + Sys.command test = 0 + else false + in diff --git a/coq.spec b/coq.spec index a8b512a..1a70cbc 100644 --- a/coq.spec +++ b/coq.spec @@ -13,12 +13,12 @@ Summary: The Coq Proof Assistant Summary(pl.UTF-8): Coq - narzędzie pomagające w udowadnianiu Name: coq -Version: 8.4pl6 -Release: 3 +Version: 8.6 +Release: 1 License: LGPL v2.1 Group: Applications/Math Source0: http://coq.inria.fr/distrib/V%{version}/files/%{name}-%{version}.tar.gz -# Source0-md5: 2334a98b64578cb81d2b4127e327b368 +# Source0-md5: e7f1704b85d648468160abe03338f1bd Source1: coqide.desktop Source2: coqide.xpm Patch0: %{name}-lablgtk2.patch @@ -30,6 +30,7 @@ BuildRequires: netpbm-progs BuildRequires: ocaml >= 3.09.0 BuildRequires: camlp5 >= 5.01 BuildRequires: ocaml-lablgtk2-devel >= 2.12.0 +BuildRequires: ocaml-lablgtk2-gtksourceview2-devel BuildRequires: sed >= 4.0 BuildRequires: texlive-fonts-cmextra BuildRequires: texlive-fonts-cmsuper @@ -106,8 +107,8 @@ Styl dokumentacji Coq dla latexa. -browser "xdg-open %s" \ -emacslib %{_datadir}/emacs/site-lisp \ %{?with_ocaml_opt:-opt} \ - --coqdocdir %{_datadir}/texmf/tex/latex/misc \ - --coqide %{?with_ocaml_opt:opt}%{!?with_ocaml_opt:byte} + -coqdocdir %{_datadir}/texmf/tex/latex/misc \ + -coqide %{?with_ocaml_opt:opt}%{!?with_ocaml_opt:byte} %{__make} -j1 world VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun %{?with_tests:%{__make} -j1 check VERBOSE=1 CAML_LD_LIBRARY_PATH=kernel/byterun} # Use native coq to compile theories @@ -123,9 +124,7 @@ install -d $RPM_BUILD_ROOT{%{_desktopdir},%{_pixmapsdir}} install %{SOURCE1} $RPM_BUILD_ROOT%{_desktopdir} install %{SOURCE2} $RPM_BUILD_ROOT%{_pixmapsdir} -# pdf is enough -%{__rm} -r $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version}/ps -cp -p CHANGES COMPATIBILITY COPYRIGHT CREDITS README $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version} +cp -p CHANGES COMPATIBILITY COPYRIGHT CREDITS README.md $RPM_BUILD_ROOT%{_docdir}/%{name}-%{version} %clean rm -rf $RPM_BUILD_ROOT @@ -134,20 +133,18 @@ rm -rf $RPM_BUILD_ROOT %defattr(644,root,root,755) %doc %{_docdir}/%{name}-%{version} %dir %{_sysconfdir}/%{name} -%config(noreplace) %verify(not md5 mtime size) %{_sysconfdir}/%{name}/coqide-gtk2rc %attr(755,root,root) %{_bindir}/coq_makefile %attr(755,root,root) %{_bindir}/coq-tex %attr(755,root,root) %{_bindir}/coqc %attr(755,root,root) %{_bindir}/coqchk -%{?with_ocaml_opt:%attr(755,root,root) %{_bindir}/coqchk.opt} %attr(755,root,root) %{_bindir}/coqdep %attr(755,root,root) %{_bindir}/coqdoc %attr(755,root,root) %{_bindir}/coqide* %attr(755,root,root) %{_bindir}/coqmktop %attr(755,root,root) %{_bindir}/coqtop %attr(755,root,root) %{_bindir}/coqtop.byte -%{?with_ocaml_opt:%attr(755,root,root) %{_bindir}/coqtop.opt} %attr(755,root,root) %{_bindir}/coqwc +%attr(755,root,root) %{_bindir}/coqworkmgr %attr(755,root,root) %{_bindir}/gallina %dir %{_libdir}/coq %{_libdir}/coq/* @@ -170,11 +167,11 @@ rm -rf $RPM_BUILD_ROOT %files emacs %defattr(644,root,root,755) -%{_datadir}/emacs/site-lisp/coq.el -%{_datadir}/emacs/site-lisp/coq-db.el %{_datadir}/emacs/site-lisp/coq-font-lock.el %{_datadir}/emacs/site-lisp/coq-inferior.el -%{_datadir}/emacs/site-lisp/coq-syntax.el +%{_datadir}/emacs/site-lisp/gallina-db.el +%{_datadir}/emacs/site-lisp/gallina-syntax.el +%{_datadir}/emacs/site-lisp/gallina.el %files latex %defattr(644,root,root,755) -- 2.43.0