From 928f86c4f8d25fde04f735714bda2d86ea44655a32141d6a361f549484f77697 Mon Sep 17 00:00:00 2001 From: Christian Goll Date: Wed, 25 Sep 2019 09:10:33 +0000 Subject: [PATCH] Accepting request 733035 from home:aaronpuchert - Initial release based on version 8.9.1. OBS-URL: https://build.opensuse.org/request/show/733035 OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=1 --- .gitattributes | 23 +++++ .gitignore | 1 + coq-8.9.1.tar.gz | 3 + coq-rpmlintrc | 7 ++ coq.changes | 212 +++++++++++++++++++++++++++++++++++++++++++++++ coq.desktop | 10 +++ coq.spec | 197 +++++++++++++++++++++++++++++++++++++++++++ coq.xml | 12 +++ 8 files changed, 465 insertions(+) create mode 100644 .gitattributes create mode 100644 .gitignore create mode 100644 coq-8.9.1.tar.gz create mode 100644 coq-rpmlintrc create mode 100644 coq.changes create mode 100644 coq.desktop create mode 100644 coq.spec create mode 100644 coq.xml diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..9b03811 --- /dev/null +++ b/.gitattributes @@ -0,0 +1,23 @@ +## Default LFS +*.7z filter=lfs diff=lfs merge=lfs -text +*.bsp filter=lfs diff=lfs merge=lfs -text +*.bz2 filter=lfs diff=lfs merge=lfs -text +*.gem filter=lfs diff=lfs merge=lfs -text +*.gz filter=lfs diff=lfs merge=lfs -text +*.jar filter=lfs diff=lfs merge=lfs -text +*.lz filter=lfs diff=lfs merge=lfs -text +*.lzma filter=lfs diff=lfs merge=lfs -text +*.obscpio filter=lfs diff=lfs merge=lfs -text +*.oxt filter=lfs diff=lfs merge=lfs -text +*.pdf filter=lfs diff=lfs merge=lfs -text +*.png filter=lfs diff=lfs merge=lfs -text +*.rpm filter=lfs diff=lfs merge=lfs -text +*.tbz filter=lfs diff=lfs merge=lfs -text +*.tbz2 filter=lfs diff=lfs merge=lfs -text +*.tgz filter=lfs diff=lfs merge=lfs -text +*.ttf filter=lfs diff=lfs merge=lfs -text +*.txz filter=lfs diff=lfs merge=lfs -text +*.whl filter=lfs diff=lfs merge=lfs -text +*.xz filter=lfs diff=lfs merge=lfs -text +*.zip filter=lfs diff=lfs merge=lfs -text +*.zst filter=lfs diff=lfs merge=lfs -text diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..57affb6 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +.osc diff --git a/coq-8.9.1.tar.gz b/coq-8.9.1.tar.gz new file mode 100644 index 0000000..4753476 --- /dev/null +++ b/coq-8.9.1.tar.gz @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:87251327e8a1e25c6b08b5c0ae8e7cdf3a91a5f30832bbe74ccc4f0bde9618ea +size 6001970 diff --git a/coq-rpmlintrc b/coq-rpmlintrc new file mode 100644 index 0000000..1a0ddc9 --- /dev/null +++ b/coq-rpmlintrc @@ -0,0 +1,7 @@ +# This line is mandatory to access the configuration functions +from Config import * + +# Unfortunate choice, but we can't easily change that. +addFilter("hidden-file-or-dir .*/.coq-native") +# These are loaded manually by the OCaml runtime and need no dependency information. +addFilter("shared-lib-without-dependency-information .*\.cmxs") diff --git a/coq.changes b/coq.changes new file mode 100644 index 0000000..b282f06 --- /dev/null +++ b/coq.changes @@ -0,0 +1,212 @@ +------------------------------------------------------------------- +Tue Sep 24 22:13:12 UTC 2019 - Aaron Puchert + +- Change license tag to LGPL-2.1-only. +- Remove obsolete %defattr and other spec-cleaner suggestions. + +------------------------------------------------------------------- +Sat Aug 3 13:22:18 UTC 2019 - Aaron Puchert + +- Update to version 8.9.0. + * Kernel: mutually recursive records are now supported. + * Notations: + + Support for autonomous grammars of terms called “custom + entries”. + + Deprecated notations of the standard library will be removed + in the next version of Coq, see the next subsection for a + script to ease porting. + + Added the "Numeral Notation" command for registering decimal + numeral notations for custom types. + * Tactics: Introduction tactics intro/intros on a goal that is an + existential variable now force a refinement of the goal into a + dependent product rather than failing. + * Decision procedures: deprecation of tactic romega in favor of + lia and removal of fourier, replaced by lra which subsumes it. + * Proof language: focusing bracket { now supports named goals, + e.g. [x]:{ will focus on a goal (existential variable) named x. + * SSReflect: the implementation of delayed clear was simplified: + the variables are always renamed using inaccessible names when + the clear switch is processed and finally cleared at the end of + the intro pattern. In addition to that, the use-and-discard + flag {} typical of rewrite rules can now be also applied to + views, e.g. => {}/v applies v and then clears v. + See Section Introduction in the context. + * Vernacular: + + Experimental support for attributes on commands, as in + "#[local] Lemma foo : bar". Tactics and tactic notations now + support the deprecated attribute. + + Removed deprecated commands "Arguments Scope" and "Implicit + Arguments" in favor of "Arguments (scopes)" and "Arguments + (implicits)". + + New flag "Uniform Inductive Parameters" to avoid repeating + uniform parameters in constructor declarations. + + New commands "Hint Variables" and "Hint Constants" for + controlling the opacity status of variables and constants in + hint databases. It is recommended to always use these + commands after creating a hint database with Create HintDb. + + Multiple sections with the same name are now allowed. + * Library: additions and changes in the VectorDef, Ascii, and + String libraries. Syntax notations are now available only when + using "Import" of libraries and not merely "Require". + (Source of incompatibility, see Change Log for details) + * Toplevels: coqtop and coqide can now display diffs between + proof steps in color, using the Diffs option. + * Documentation: we integrated a large number of fixes to the new + Sphinx documentation. + * Tools: removed gallina utility and homebrewed Emacs mode. +- Update to version 8.9.1, which contains + * some quality-of-life bug fixes, + * many improvements to the documentation, + * a critical bug fix related to primitive projections and + native_compute. +- Remove unnecessary dependencies: ncurses-devel is no longer + needed, and the docs aren't build with TeX and hevea anymore. +- Remove dependencies that are automatically detected. +- Remove icon that is also available from the tarball. +- Replace some identical files by symlinks. +- Fix executable bits and shebangs. +- Separate runtime from devel files by ending. +- Use %license for LICENSE and CREDITS. +- Be more explicit in %files. +- Add mime type for Coq source files so they open with the IDE. +- Add rpmlintrc for issues that are hard to fix. + +------------------------------------------------------------------- +Thu Oct 11 09:35:41 UTC 2018 - ptrommler@icloud.com + +- update to 8.8.2 + +------------------------------------------------------------------- +Sun Jan 7 10:41:00 UTC 2018 - ptrommler@icloud.com + +- update to 8.7.1 + +------------------------------------------------------------------- +Thu Nov 2 15:32:20 UTC 2017 - ptrommler@icloud.com + +- update to 8.7.0 + * I need this in class b/c coq-ide reads _CoqProject files + +------------------------------------------------------------------- +Thu Apr 13 11:34:12 UTC 2017 - peter.trommler@ohm-hochschule.de + +- update to 8.6 from upstream + +------------------------------------------------------------------- +Fri Dec 2 14:30:06 UTC 2016 - peter.trommler@ohm-hochschule.de + +- update to 8.5pl3 from upstream + +------------------------------------------------------------------- +Fri Oct 21 18:11:31 UTC 2016 - peter.trommler@ohm-hochschule.de + +- update to 8.5pl2 from upstream + +------------------------------------------------------------------- +Sun Apr 10 10:32:12 UTC 2016 - peter.trommler@ohm-hochschule.de + +- update to 8.5 from upstream + +------------------------------------------------------------------- +Sat May 31 18:46:45 UTC 2014 - peter.trommler@ohm-hochschule.de + +- update to 8.4pl4 from upstream + +------------------------------------------------------------------- +Sun Jan 12 11:17:04 UTC 2014 - peter.trommler@ohm-hochschule.de + +- update to 8.4pl3 from upstream +- follow upstream versioning + +------------------------------------------------------------------- +Sun Nov 10 08:45:53 UTC 2013 - peter.trommler@ohm-hochschule.de + +- revert to our own lablgtk on older systems +* coq-ide cannot be built using 12.2 lablgtk2 + +------------------------------------------------------------------- +Wed Nov 6 19:53:49 UTC 2013 - peter.trommler@ohm-hochschule.de + +- use system provided lablgtk2 + +------------------------------------------------------------------- +Mon Apr 8 11:31:02 UTC 2013 - peter.trommler@ohm-hochschule.de + +- update to 8.4pl2 +- coqtop: handle interrupt signals reliably +- restor old behavior for code extraction (AccessOpaque) + +------------------------------------------------------------------- +Wed Dec 26 19:49:24 UTC 2012 - peter.trommler@ohm-hochschule.de + +- update to 8.4pl1 from upstream +- dropped f0b93...055.patch (integrated upstream) +- use ocamlfind to find lablgtk2 + +------------------------------------------------------------------- +Mon Dec 3 10:14:09 UTC 2012 - peter.trommler@ohm-hochschule.de + +- add patch for lablgtk2 v 2.16 + +------------------------------------------------------------------- +Thu Nov 29 20:18:17 UTC 2012 - peter.trommler@ohm-hochschule.de + +- mark config file + +------------------------------------------------------------------- +Sun Nov 11 18:53:41 UTC 2012 - peter.trommler@ohm-hochschule.de + +- give up on old ocaml names and require ocaml-lablgtk2-devel +- clean up spec file + +------------------------------------------------------------------- +Thu Oct 18 13:28:32 UTC 2012 - peter.trommler@ohm-hochschule.de + +- remove requires and rely on automatic dependency generation + for ocaml + +------------------------------------------------------------------- +Wed Oct 17 16:01:25 UTC 2012 - peter.trommler@ohm-hochschule.de + +- packaged new file coq.png + +------------------------------------------------------------------- +Sun Oct 7 15:59:53 UTC 2012 - peter.trommler@ohm-hochschule.de + +- update to 8.4 from upstream + +------------------------------------------------------------------- +Thu Apr 12 12:14:04 UTC 2012 - peter.trommler@ohm-hochschule.de + +- add ocaml- prefix to lablgtk-devel Buildrequires + +------------------------------------------------------------------- +Wed Apr 11 17:32:25 UTC 2012 - peter.trommler@ohm-hochschule.de + +- add Buildrequires hevea needed for documentation + +------------------------------------------------------------------- +Wed Apr 11 16:56:52 UTC 2012 - peter.trommler@ohm-hochschule.de + +- cleaned up spec file (BuildRequires and Requires one each line) +- SPDX license tag + +------------------------------------------------------------------- +Wed Apr 11 16:26:24 UTC 2012 - peter.trommler@ohm-hochschule.de + +- upgraded to 8.3pl4 from upstream +Bug fixes: + +- #2724 (using notations with binders in cases patterns was provoking an anomaly) +- #2723 (alpha-conversion bug #2723 introduced in r12485-12486) +- #2732 (anomaly when using the tolerance for writing "f atomic_tac" + as a short-hand for "f ltac:(atomic_tac)") +- #2729 (vm_compute: function used to decompose constructors did not handle let-ins) +- #2728 (compatibility with camlp5 6.05) +- #2682 (Fail discard the effects of a successful command) +- #2703 (Undetected universe inconsistency) +- #2667 (Coq crashes when "Arguments Scope" has too many parameters) +- Compilation of coqide under MacOS with gtk >= 2.24.11 +- Coqdoc: Fixing missing newline when using "Proof term." + + diff --git a/coq.desktop b/coq.desktop new file mode 100644 index 0000000..c0b12d8 --- /dev/null +++ b/coq.desktop @@ -0,0 +1,10 @@ +[Desktop Entry] +Encoding=UTF-8 +Type=Application +Name=Coq IDE +GenericName=Proof Assistant +Comment=Proof Assistant based on the Calculus of Inductive Constructions +Categories=Education;Science;Math; +MimeType=text/x-coqsrc; +Exec=coqide %F +Icon=coq diff --git a/coq.spec b/coq.spec new file mode 100644 index 0000000..72718ad --- /dev/null +++ b/coq.spec @@ -0,0 +1,197 @@ +# +# spec file for package coq +# +# Copyright (c) 2019 SUSE LINUX GmbH, Nuernberg, Germany. +# Copyright (c) 2012-2018 Peter Trommler, peter.trommler at ohm-hochschule.de +# +# All modifications and additions to the file contributed by third parties +# remain the property of their copyright owners, unless otherwise agreed +# upon. The license for this file, and modifications and additions to the +# file, is the same license as for the pristine package itself (unless the +# license for the pristine package is not an Open Source License, in which +# case the license is the MIT License). An "Open Source License" is a +# license that conforms to the Open Source Definition (Version 1.9) +# published by the Open Source Initiative. + +# Please submit bugfixes or comments via https://bugs.opensuse.org/ +# + +Name: coq +Version: 8.9.1 +Release: 0 +Summary: Proof Assistant based on the Calculus of Inductive Constructions +License: LGPL-2.1-only +Group: Productivity/Scientific/Math +URL: https://coq.inria.fr/ +Source: https://github.com/coq/coq/archive/V%{version}.tar.gz#/%{name}-%{version}.tar.gz +Source1: coq.desktop +Source2: coq.xml +Source100: %{name}-rpmlintrc +BuildRequires: desktop-file-utils +# Required for standard coq: +BuildRequires: make >= 3.81 +BuildRequires: ocaml >= 3.10.2 +BuildRequires: ocaml-camlp5-devel >= 5.08 +# TODO: Build docs when antlr4-python3-runtime becomes available. +#BuildRequires: python3-Sphinx +#BuildRequires: python3-pexpect +#BuildRequires: antlr4-python3-runtime +#BuildRequires: python3-beautifulsoup4 +# Required for coq-ide: +BuildRequires: ocaml-findlib +BuildRequires: ocamlfind(lablgtk2) +BuildRequires: update-desktop-files + +%global __requires_exclude ocaml\\\((Interface|Sos_types|GtkSourceView2_types)\\\) + +%description +Proof assistant which allows to handle calculus assertions, check mechanically +proofs of these assertions, helps to find formal proofs and extracts a certified +program from the constructive proof of its formal specification. + +This package contains shared files and the command line interface. +For a graphical interface install %{name}-ide. + +%package ide +Summary: IDE for The Coq Proof Assistant +Group: Productivity/Scientific/Math +Requires: %{name} = %{version}-%{release} + +%description ide +The Coq Integrated Development Interface is a graphical interface for the Coq proof assistant. + +%package devel +Summary: Development files for coq +Group: Development/Libraries/Other +Requires: %{name} = %{version}-%{release} +Requires: ocaml >= 3.10.2 + +%description devel +This package contains development files for Coq. + +%prep +%setup -q + +%build +export CFLAGS='%{optflags}' +./configure \ + -bindir %{_bindir} \ + -libdir %{_libdir}/coq \ + -mandir %{_mandir} \ + -datadir %{_datadir}/%{name} \ + -docdir %{_docdir}/%{name} \ + -configdir %{_sysconfdir}/xdg/%{name} \ + -coqdocdir %{_datadir}/texmf/tex/latex/misc \ + -native-compiler yes \ + -natdynlink yes \ + -browser "xdg-open %s" + +make %{?_smp_mflags} world + +%install +make COQINSTALLPREFIX=%{buildroot} install + +%suse_update_desktop_file -i %{SOURCE1} +install -D -m 644 %{SOURCE1} %{buildroot}%{_datadir}/applications/coq.desktop +install -D -m 644 %{SOURCE2} %{buildroot}%{_datadir}/mime/packages/coq.xml +install -D -m 644 ide/coq.png %{buildroot}%{_datadir}/icons/hicolor/256x256/apps/coq.png + +# Sometimes we get identical x and x.opt files, replace by symlink x -> x.opt. +for bin in %{buildroot}%{_bindir}/*.opt +do + if [ -f ${bin%.opt} ] && diff $bin ${bin%.opt} + then + rm ${bin%.opt} + ln -s ${bin#%{buildroot}} ${bin%.opt} + fi +done + +# Fix executable bit and shebangs, preferring python3. +# (https://www.python.org/dev/peps/pep-0394/#for-python-runtime-distributors) +chmod -x %{buildroot}%{_libdir}/%{name}/tools/TimeFileMaker.py +sed -i '1s|^#!/usr/bin/env *|#!/usr/bin/|;1s|^#!/usr/bin/python$|#!/usr/bin/python3|' \ + %{buildroot}%{_libdir}/%{name}/tools/make-{one-time-file,both-{time,single-timing}-files}.py + +# Remove superfluous man page. +rm %{buildroot}%{_mandir}/man1/coqtop.byte.1 + +# Build lists of runtime and devel files by ending. +# Compiled theories and shared objects are needed at runtime. +find %{buildroot}%{_libdir}/coq/{plugins,theories} -type d | \ + sed "s|%{buildroot}|%%dir |g" >runtime.list +find %{buildroot}%{_libdir}/coq -name '*.cmxs' \ + -or -name '*.so' \ + -or -name '*.vo' | sed "s|%{buildroot}||g" >>runtime.list + +# Object files, static libraries and import definitions are only needed for development. +# For now, we also put the standard library Coq sources here, since the runtime +# package contains the HTML documentation for the standard library. +find %{buildroot}%{_libdir}/coq -type d | sed "s|%{buildroot}|%%dir |g" >devel.list +find %{buildroot}%{_libdir}/coq -name '*.a' \ + -or -name '*.cma' \ + -or -name '*.cmi' \ + -or -name '*.cmx' \ + -or -name '*.cmxa' \ + -or -name '*.glob' \ + -or -name '*.o' \ + -or -name '*.v' | sed "s|%{buildroot}||g" >>devel.list + +%files -f runtime.list +%license LICENSE CREDITS +%doc CHANGES.md README.md +%{_docdir}/%{name}/FAQ-CoqIde + +%{_bindir}/coq-tex +%{_bindir}/coq_makefile +%{_bindir}/coqc +%{_bindir}/coqchk +%{_bindir}/coqdep +%{_bindir}/coqdoc +%{_bindir}/coqpp +%{_bindir}/coqproofworker.opt +%{_bindir}/coqqueryworker.opt +%{_bindir}/coqtacticworker.opt +%{_bindir}/coqtop +%{_bindir}/coqtop.opt +%{_bindir}/coqwc +%{_bindir}/coqworkmgr + +%dir %{_libdir}/coq +%{_libdir}/coq/META +%dir %{_libdir}/coq/kernel +%dir %{_libdir}/coq/kernel/byterun +%{_libdir}/coq/plugins/micromega/csdpcert +%{_libdir}/coq/tools +%exclude %{_libdir}/coq/tools/CoqMakefile.in +%dir %{_libdir}/coq/user-contrib + +%{_mandir}/man1/coq-tex.1%{ext_man} +%{_mandir}/man1/coq_makefile.1%{ext_man} +%{_mandir}/man1/coqc.1%{ext_man} +%{_mandir}/man1/coqchk.1%{ext_man} +%{_mandir}/man1/coqdep.1%{ext_man} +%{_mandir}/man1/coqdoc.1%{ext_man} +%{_mandir}/man1/coqtop.1%{ext_man} +%{_mandir}/man1/coqtop.opt.1%{ext_man} +%{_mandir}/man1/coqwc.1%{ext_man} + +%{_datadir}/%{name} +%dir %{_datadir}/texmf +%dir %{_datadir}/texmf/tex +%dir %{_datadir}/texmf/tex/latex +%dir %{_datadir}/texmf/tex/latex/misc +%{_datadir}/texmf/tex/latex/misc/coqdoc.sty + +%files ide +%{_bindir}/coqide +%{_bindir}/coqidetop +%{_bindir}/coqidetop.opt +%{_mandir}/man1/coqide.1%{ext_man} +%{_datadir}/applications/coq.desktop +%{_datadir}/icons/hicolor/256x256/apps/coq.png +%{_datadir}/mime/packages/coq.xml + +%files devel -f devel.list +%{_libdir}/coq/tools/CoqMakefile.in + +%changelog diff --git a/coq.xml b/coq.xml new file mode 100644 index 0000000..f13b303 --- /dev/null +++ b/coq.xml @@ -0,0 +1,12 @@ + + + + Coq source file + + + + + Coq object file + + +