diff --git a/coq-sphinxcontrib-bibtex.patch b/coq-sphinxcontrib-bibtex.patch deleted file mode 100644 index 34f9508..0000000 --- a/coq-sphinxcontrib-bibtex.patch +++ /dev/null @@ -1,10 +0,0 @@ ---- a/doc/sphinx/conf.py.orig 2020-12-11 01:46:08.000000000 -0700 -+++ b/doc/sphinx/conf.py 2020-12-22 20:40:30.560758128 -0700 -@@ -110,6 +110,7 @@ master_doc = "index" - project = 'Coq' - copyright = '1999-2020, Inria, CNRS and contributors' - author = 'The Coq Development Team' -+bibtex_bibfiles = ['biblio.bib'] - - # The version info for the project you're documenting, acts as replacement for - # |version| and |release|, also used in various other places throughout the diff --git a/coq.spec b/coq.spec index e0f51ac..0532345 100644 --- a/coq.spec +++ b/coq.spec @@ -14,30 +14,30 @@ ExcludeArch: s390x Name: coq -Version: 8.12.2 -Release: 2%{?dist} +Version: 8.13.0 +Release: 1%{?dist} Summary: Proof management system License: LGPLv2 URL: https://coq.inria.fr/ Source0: https://github.com/coq/coq/archive/V%{version}/%{name}-%{version}.tar.gz -Source1: coqide.desktop +Source1: fr.inria.coqide.desktop Source2: coq.xml -Source3: coqide.appdata.xml -# Adapt to sphinxcontrib-bibtex 2.x -Patch0: %{name}-sphinxcontrib-bibtex.patch +Source3: fr.inria.coqide.metainfo.xml -BuildRequires: ocaml >= 4.08.0 -BuildRequires: ocaml-dune -BuildRequires: ocaml-findlib +BuildRequires: ocaml >= 4.05.0 +BuildRequires: ocaml-dune >= 2.5.0 +BuildRequires: ocaml-findlib >= 1.8.1 BuildRequires: ocaml-lablgtk3-devel >= 3.0 BuildRequires: ocaml-lablgtk3-sourceview3-devel >= 3.0 -BuildRequires: ocaml-num-devel BuildRequires: ocaml-ocamldoc BuildRequires: ocaml-ounit-devel +BuildRequires: ocaml-zarith-devel >= 1.10 BuildRequires: csdp-tools BuildRequires: desktop-file-utils +BuildRequires: libappstream-glib BuildRequires: libicns-utils +BuildRequires: make BuildRequires: rsync BuildRequires: time @@ -45,7 +45,6 @@ BuildRequires: time BuildRequires: antlr4 BuildRequires: hevea BuildRequires: latexmk -BuildRequires: make BuildRequires: python3-devel BuildRequires: %{py3_dist antlr4-python3-runtime} BuildRequires: %{py3_dist beautifulsoup4} @@ -81,10 +80,14 @@ BuildRequires: tex-zapfchan BuildRequires: tex-zapfding Requires: csdp-tools +Requires: ocaml-findlib Requires: texlive-base Recommends: emacs-proofgeneral +# Exclude private ocaml interfaces that we don't Provide +%global __requires_exclude ocamlx?\\\((Configwin_types|Interface|Richpp|Serialize|Xml_p(arser|rinter)|Xmlprotocol)\\\) + %global _desc %{expand: Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems @@ -146,10 +149,14 @@ fixtimestamp() { rm -f $1.orig } -# Use Fedora compiler and linker flags -sed -e 's|-Wall.*-O2|%{optflags} -Wno-unused|' \ - -e "s|-lunix|& -ccopt '$RPM_LD_FLAGS'|" \ - -i configure.ml +# Fix a Makefile rule that causes installation to fail +sed -ri '/FULLCONFIGDIR/s/OLDROOT|COQINSTALLPREFIX/&2/g' Makefile.install + +# Use Fedora compiler flags +sed -i 's|-Wall.*-O2|%{build_cflags} -Wno-unused|' configure.ml + +# Use Fedora link flags +sed -i "s|-oc|-ccopt '%{build_ldflags}' -g &|" Makefile.build # Make sure debuginfo is generated sed -i 's,-shared,& -g,g' tools/CoqMakefile.in Makefile.build @@ -165,98 +172,88 @@ for f in $(grep -Frl '%{_bindir}/env'); do fixtimestamp $f done -# Work around a bad path -sed -i.orig "s,-q,& --coqlib_path $PWD/_build/default," doc/stdlib/dune - -# Change dune's configure invocation -%ifarch %{ocaml_native_compiler} -%global opt_option -native-compiler yes -natdynlink yes -coqide opt -%else -%global opt_option -bytecode-compiler yes -byte-only -coqide byte -%endif - +%build %global coqdocdir %{?_pkgdocdir}%{!?_pkgdocdir:%{_docdir}/coq-%{version}} -sed -i 's,-native-compiler no,-prefix %{_prefix} -libdir %{_libdir}/ocaml/coq -docdir %{coqdocdir} -configdir %{_sysconfdir}/xdg/%{name} -coqdocdir %{_texmf_main}/tex/latex/misc %{opt_option} -browser "xdg-open %s" -with-doc yes,' config/dune - -%build # Regenerate ANTLR files cd doc/tools/coqrst/notations antlr4 -Dlanguage=Python3 -visitor -no-listener TacticNotations.g cd - -export SPHINXWARNOPT="-w$PWD/sphinx-warn.log" -dune build %{?_smp_mflags} - -# Relink the stublib with RPM_LD_FLAGS -cd _build/default/kernel/byterun -ocamlmklib -g -ldopt "$RPM_LD_FLAGS" -o byterun_stubs $(ar t libbyterun_stubs.a) -cd - - -# Undo the bad path workaround now that we're done -mv doc/stdlib/dune.orig doc/stdlib/dune - -%install -# Installing with dune fails due to https://github.com/ocaml/dune/issues/1868. -# We fake dune out by telling it not to install documentation, install, then -# put the original file back. -cp -p _build/default/coq-doc.install _build/default/coq-doc.install.orig -chmod u+w _build/default/coq-doc.install -sed -ri '/(html|pdf)/d' _build/default/coq-doc.install -dune install --destdir=%{buildroot} -mv _build/default/coq-doc.install.orig _build/default/coq-doc.install - -# Fix permissions %ifarch %{ocaml_native_compiler} -find %{buildroot}%{_libdir}/ocaml -name \*.cmxs -exec chmod a+x {} \+ +%global opt_option -native-compiler yes -coqide opt +%else +%global opt_option -byte-only -coqide byte +%endif +%ifarch %{ocaml_natdynlink} +%global opt_option %{opt_option} -natdynlink yes %endif -chmod a+x %{buildroot}%{_libdir}/ocaml/coq/tools/make*.py -# Install the LaTeX style file -mkdir -p %{buildroot}%{_texmf_main}/tex/latex/misc -cp -p tools/coqdoc/coqdoc.sty %{buildroot}%{_texmf_main}/tex/latex/misc +# Set our configuration options +./configure -prefix %{_prefix} \ + -libdir %{_libdir}/ocaml/coq \ + -bindir %{_bindir} \ + -mandir %{_mandir} \ + -docdir %{coqdocdir} \ + -configdir %{_sysconfdir}/xdg/%{name} \ + -coqdocdir %{_texmf_main}/tex/latex/misc \ + %{opt_option} \ + -browser "xdg-open %s" \ + -with-doc yes + +# Build the binary artifacts +export SPHINXWARNOPT="-w$PWD/sphinx-warn.log" +make world VERBOSE=1 -# Make a directory for site-wide configuration files -mkdir -p %{buildroot}%{_sysconfdir}/xdg/coq +%install +make COQINSTALLPREFIX="%{buildroot}%{_prefix}" OLDROOT="%{_prefix}" \ + COQINSTALLPREFIX2="%{buildroot}%{_sysconfdir}" OLDROOT2="%{_sysconfdir}" \ + install -# We install the documentation with the doc macro -rm -fr %{buildroot}%{_prefix}/doc +# Fix permissions +if [ -e %{buildroot}%{_libdir}/ocaml/coq/kernel/byterun/dllcoqrun.so ]; then + chmod 0755 %{buildroot}%{_libdir}/ocaml/coq/kernel/byterun/dllcoqrun.so +fi # Prepare the documentation for installation -cp -Lpr _build/install/default/doc/coq-doc/html html -find html -name .buildinfo -o -name .doctrees -exec rm -fr {} \+ +find doc/sphinx/_build/html -name .buildinfo -delete # Use links rather than copying binaries %ifarch %{ocaml_native_compiler} -for fil in coqtop; do +for fil in coqtop coqidetop; do rm -f %{buildroot}%{_bindir}/$fil ln %{buildroot}%{_bindir}/$fil.%{camlsuffix} %{buildroot}%{_bindir}/$fil done -rm %{buildroot}%{_libdir}/ocaml/coq/user-contrib/Ltac2/ltac2_plugin.cmxs -ln -s ../../plugins/ltac2/ltac2_plugin.cmxs \ - %{buildroot}%{_libdir}/ocaml/coq/user-contrib/Ltac2 %endif -# Install desktop icons -pushd ide/MacOS +# Install desktop and file type icons +pushd ide/coqide/MacOS icns2png -x coqide.icns for sz in 16 32 256 512; do mkdir -p %{buildroot}%{_datadir}/icons/hicolor/${sz}x${sz}/apps mv coqide_${sz}x${sz}x32.png \ %{buildroot}%{_datadir}/icons/hicolor/${sz}x${sz}/apps/coq.png done +icns2png -x coqfile.icns +for sz in 16 32 128 256 512; do + mkdir -p %{buildroot}%{_datadir}/icons/hicolor/${sz}x${sz}/mimetypes + mv coqfile_${sz}x${sz}x32.png \ + %{buildroot}%{_datadir}/icons/hicolor/${sz}x${sz}/mimetypes/coqfile.png +done popd +# Make a MIME type for .v files +mkdir -p %{buildroot}%{_datadir}/mime/packages +cp -p %{SOURCE2} %{buildroot}%{_datadir}/mime/packages + # Install desktop file desktop-file-install --dir=%{buildroot}%{_datadir}/applications %{SOURCE1} # Install AppData file -mkdir -p %{buildroot}%{_datadir}/appdata -install -pm 644 %{SOURCE3} %{buildroot}%{_datadir}/appdata - -# Make a MIME type for .v files -mkdir -p %{buildroot}%{_datadir}/mime/packages -cp -p %{SOURCE2} %{buildroot}%{_datadir}/mime/packages +mkdir -p %{buildroot}%{_metainfodir} +install -pm 644 %{SOURCE3} %{buildroot}%{_metainfodir} +appstream-util validate-relax --nonet \ + %{buildroot}%{_metainfodir}/fr.inria.coqide.metainfo.xml # Install the language bindings mkdir -p %{buildroot}%{_datadir}/gtksourceview-3.0/language-specs @@ -268,14 +265,30 @@ done mkdir -p %{buildroot}%{_datadir}/gtksourceview-3.0/styles ln -s ../../coq/coq_style.xml %{buildroot}%{_datadir}/gtksourceview-3.0/styles +# We don't need both PostScript and PDF documentation +rm -fr %{buildroot}%{coqdocdir}/ps + +# Install documentation not installed by install-doc in Makefile +cp -p dev/doc/changes.md CREDITS README.md %{buildroot}%{coqdocdir} + # Byte compile the tools %py_byte_compile %{python3} %{buildroot}%{_libdir}/ocaml/coq/tools +# Install opam files +cp -p coq.opam %{buildroot}%{_libdir}/ocaml/coq/opam + +mkdir -p %{buildroot}%{_libdir}/ocaml/coq-doc +cp -p coq-doc.opam %{buildroot}%{_libdir}/ocaml/coq-doc/opam + +mkdir -p %{buildroot}%{_libdir}/ocaml/coqide-server +cp -p coqide-server.opam %{buildroot}%{_libdir}/ocaml/coqide-server/opam + +mkdir -p %{buildroot}%{_libdir}/ocaml/coqide +cp -p coqide.opam %{buildroot}%{_libdir}/ocaml/coqide-server/opam + %files -%doc CREDITS README.md dev/doc/changes.md %license LICENSE %{_libdir}/ocaml/coq/ -%{_libdir}/ocaml/stublibs/dllbyterun_stubs.so %{_bindir}/coqc* %{_bindir}/coqdep %{_bindir}/coqdoc @@ -288,7 +301,6 @@ ln -s ../../coq/coq_style.xml %{buildroot}%{_datadir}/gtksourceview-3.0/styles %{_bindir}/coqtop* %{_bindir}/coqwc %{_bindir}/coqworkmgr -%{_bindir}/csdpcert %{_bindir}/ocamllibdep %{_bindir}/votour %{_mandir}/man1/coqc.1* @@ -308,31 +320,39 @@ ln -s ../../coq/coq_style.xml %{buildroot}%{_datadir}/gtksourceview-3.0/styles %files coqide-server %{_bindir}/coqidetop* -%{_bindir}/fake_ide %{_libdir}/ocaml/coqide-server/ %files coqide -%doc ide/FAQ %{_bindir}/coqide %{_datadir}/%{name}/ %{_datadir}/icons/hicolor/16x16/apps/coq.png +%{_datadir}/icons/hicolor/16x16/mimetypes/coqfile.png %{_datadir}/icons/hicolor/32x32/apps/coq.png +%{_datadir}/icons/hicolor/32x32/mimetypes/coqfile.png +%{_datadir}/icons/hicolor/128x128/mimetypes/coqfile.png %{_datadir}/icons/hicolor/256x256/apps/coq.png +%{_datadir}/icons/hicolor/256x256/mimetypes/coqfile.png %{_datadir}/icons/hicolor/512x512/apps/coq.png +%{_datadir}/icons/hicolor/512x512/mimetypes/coqfile.png %{_mandir}/man1/coqide.1* %{_libdir}/ocaml/coqide/ -%{_datadir}/appdata/coqide.appdata.xml -%{_datadir}/applications/coqide.desktop +%{_metainfodir}/fr.inria.coqide.metainfo.xml +%{_datadir}/applications/fr.inria.coqide.desktop %{_datadir}/gtksourceview-3.0/language-specs/coq*.lang %{_datadir}/gtksourceview-3.0/styles/coq_style.xml %{_datadir}/mime/packages/coq.xml %{_sysconfdir}/xdg/coq/ %files doc -%doc doc/README.md html %license doc/LICENSE +%{coqdocdir} %changelog +* Sat Feb 20 2021 Jerry James - 8.13.0-1 +- Version 8.13.0 +- Revert to make; dune is unable to build the native compilation version +- Install into the metainfo dir instead of the appdata dir + * Tue Jan 26 2021 Fedora Release Engineering - 8.12.2-2 - Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild diff --git a/coq.xml b/coq.xml index ad631ee..fb51a5b 100644 --- a/coq.xml +++ b/coq.xml @@ -4,5 +4,6 @@ Coq theory files + diff --git a/coqide.appdata.xml b/coqide.appdata.xml deleted file mode 100644 index a1156bc..0000000 --- a/coqide.appdata.xml +++ /dev/null @@ -1,45 +0,0 @@ - - - coqide.desktop - CC0-1.0 - LGPL-2.1 - coqide - Coq graphical interface - -

- Coq is a formal proof management system. It allows for the development of - theorems through first order logic that are mechanically checked by the - machine. Sets of definitions and theorems can be saved as compiled modules - and loaded into the system. -

-

- This package provides Coqide, a lightweight IDE for Coq. -

- - - - https://coq.inria.fr/files/coqide/images/capture1.jpg - Tactic list - - - https://coq.inria.fr/files/coqide/images/capture2.jpg - Template list - - - https://coq.inria.fr/files/coqide/images/capture3.jpg - Query list - - - https://coq.inria.fr/files/coqide/images/capture4.jpg - Query result - - - https://coq.inria.fr/files/coqide/images/capture5.jpg - Tactics wizard - - - loganjerry@gmail.com - https://coq.inria.fr/ - https://coq.inria.fr/bugs/ - https://coq.inria.fr/documentation - diff --git a/coqide.desktop b/coqide.desktop deleted file mode 100644 index 89aa6d2..0000000 --- a/coqide.desktop +++ /dev/null @@ -1,8 +0,0 @@ -[Desktop Entry] -Name=CoqIDE -Comment=Examine and develop Coq .v files -Exec=coqide -Icon=coq -Type=Application -Categories=Development; -MimeType=application/x-coq; diff --git a/fr.inria.coqide.desktop b/fr.inria.coqide.desktop new file mode 100644 index 0000000..89aa6d2 --- /dev/null +++ b/fr.inria.coqide.desktop @@ -0,0 +1,8 @@ +[Desktop Entry] +Name=CoqIDE +Comment=Examine and develop Coq .v files +Exec=coqide +Icon=coq +Type=Application +Categories=Development; +MimeType=application/x-coq; diff --git a/fr.inria.coqide.metainfo.xml b/fr.inria.coqide.metainfo.xml new file mode 100644 index 0000000..7e22484 --- /dev/null +++ b/fr.inria.coqide.metainfo.xml @@ -0,0 +1,51 @@ + + + fr.inria.coqide + CC0-1.0 + LGPL-2.1 + coqide + Coq graphical interface + +

+ Coq is a formal proof management system. It allows for the development of + theorems through first order logic that are mechanically checked by the + machine. Sets of definitions and theorems can be saved as compiled + modules and loaded into the system. +

+

+ This package provides Coqide, a lightweight IDE for Coq. +

+ + fr.inria.coqide.desktop + + + https://coq.inria.fr/files/coqide/images/capture1.jpg + Tactic list + + + https://coq.inria.fr/files/coqide/images/capture2.jpg + Template list + + + https://coq.inria.fr/files/coqide/images/capture3.jpg + Query list + + + https://coq.inria.fr/files/coqide/images/capture4.jpg + Query result + + + https://coq.inria.fr/files/coqide/images/capture5.jpg + Tactics wizard + + + loganjerry@gmail.com + https://coq.inria.fr/ + https://github.com/coq/coq/issues + https://coq.inria.fr/documentation + https://coq.inria.fr/consortium + + + coqide + + diff --git a/sources b/sources index 2541cd4..bd46820 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (coq-8.12.2.tar.gz) = 6b524edbceb5795f04bbd2b52f191bfcf10b611f7a2fa0450c30b72c944f88418d261729476b64603faacfe2be5f7992a2997541e54e6f8691d4dc8b4969198d +SHA512 (coq-8.13.0.tar.gz) = c355f0a9183f3669debd5f8f4ab96786215d0cccc37d1c2ac95a2d3c6115c8b0ee7ff7e23464b18444e2648ef3f8c221f0f3a28acf91199751cea2b74ee3fe8e