2019-09-25 11:10:33 +02:00
|
|
|
#
|
|
|
|
|
# spec file for package coq
|
|
|
|
|
#
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
# Copyright (c) 2021 SUSE LLC
|
2019-09-25 11:10:33 +02:00
|
|
|
# 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/
|
|
|
|
|
#
|
|
|
|
|
|
2020-02-15 20:32:26 +01:00
|
|
|
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
%bcond_without ide
|
|
|
|
|
|
2019-09-25 11:10:33 +02:00
|
|
|
Name: coq
|
2021-05-01 23:33:33 +02:00
|
|
|
Version: 8.13.2
|
2019-09-25 11:10:33 +02:00
|
|
|
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
|
2021-09-04 14:54:51 +02:00
|
|
|
Source50: coq-refman-%{version}.tar.xz
|
|
|
|
|
Source51: coq-stdlib-%{version}.tar.xz
|
2019-09-25 11:10:33 +02:00
|
|
|
Source100: %{name}-rpmlintrc
|
|
|
|
|
BuildRequires: desktop-file-utils
|
|
|
|
|
BuildRequires: make >= 3.81
|
2020-02-15 20:32:26 +01:00
|
|
|
BuildRequires: ocaml >= 4.05.0
|
2019-09-25 11:10:33 +02:00
|
|
|
BuildRequires: ocaml-camlp5-devel >= 5.08
|
2020-02-15 20:32:26 +01:00
|
|
|
BuildRequires: ocamlfind(findlib)
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
BuildRequires: ocamlfind(zarith)
|
|
|
|
|
%if %{with ide}
|
|
|
|
|
BuildRequires: update-desktop-files
|
2020-02-15 20:32:26 +01:00
|
|
|
BuildRequires: ocamlfind(lablgtk3)
|
|
|
|
|
BuildRequires: pkgconfig(gdk-3.0)
|
|
|
|
|
BuildRequires: pkgconfig(gtk+-3.0)
|
|
|
|
|
BuildRequires: pkgconfig(gtksourceview-3.0)
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
%endif
|
2019-09-25 11:10:33 +02:00
|
|
|
|
|
|
|
|
%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}
|
2020-02-15 20:32:26 +01:00
|
|
|
Requires: ocaml >= 4.05.0
|
2021-05-01 23:33:33 +02:00
|
|
|
Requires: ocamlfind(findlib)
|
2019-09-25 11:10:33 +02:00
|
|
|
|
|
|
|
|
%description devel
|
|
|
|
|
This package contains development files for Coq.
|
|
|
|
|
|
2021-09-04 14:54:51 +02:00
|
|
|
%package doc
|
|
|
|
|
Summary: Documentation for coq
|
|
|
|
|
Group: Documentation/HTML
|
|
|
|
|
Requires: %{name} = %{version}
|
|
|
|
|
|
|
|
|
|
%description doc
|
|
|
|
|
HTML reference manual for Coq and full documentation of the standard library.
|
|
|
|
|
|
2019-09-25 11:10:33 +02:00
|
|
|
%prep
|
2021-09-04 14:54:51 +02:00
|
|
|
%setup -q -a 50 -a 51
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
# META for ocamlfind doesn't contain a version, so configure.ml fails. We patch that.
|
|
|
|
|
sed -i 's/v, _ = tryrun camlexec.find \["query"; "-format"; "%v"; "lablgtk3"\]/v = "%{pkg_version ocamlfind(lablgtk3)}"/' \
|
|
|
|
|
configure.ml
|
2019-09-25 11:10:33 +02:00
|
|
|
|
|
|
|
|
%build
|
|
|
|
|
export CFLAGS='%{optflags}'
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
# TODO: Add -with-doc yes
|
2019-09-25 11:10:33 +02:00
|
|
|
./configure \
|
|
|
|
|
-bindir %{_bindir} \
|
|
|
|
|
-libdir %{_libdir}/coq \
|
|
|
|
|
-mandir %{_mandir} \
|
|
|
|
|
-datadir %{_datadir}/%{name} \
|
|
|
|
|
-docdir %{_docdir}/%{name} \
|
|
|
|
|
-configdir %{_sysconfdir}/xdg/%{name} \
|
|
|
|
|
-coqdocdir %{_datadir}/texmf/tex/latex/misc \
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
%if %{with ide}
|
|
|
|
|
-coqide opt \
|
|
|
|
|
%else
|
|
|
|
|
-coqide no \
|
|
|
|
|
%endif
|
2019-09-25 11:10:33 +02:00
|
|
|
-native-compiler yes \
|
|
|
|
|
-natdynlink yes \
|
|
|
|
|
-browser "xdg-open %s"
|
|
|
|
|
|
2019-11-03 19:30:53 +01:00
|
|
|
make %{?_smp_mflags} world
|
2019-09-25 11:10:33 +02:00
|
|
|
|
|
|
|
|
%install
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
%if %{with ide}
|
2019-11-03 19:30:53 +01:00
|
|
|
# Fixup dependencies before we install. Some are apparently not detected.
|
|
|
|
|
sed -i 's#^ide/ide_MLLIB_DEPENDENCIES:=.*$#& ide/configwin_types ide/protocol/richpp#' \
|
|
|
|
|
.mllibfiles.d
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
%endif
|
2019-11-03 19:30:53 +01:00
|
|
|
|
2019-09-25 11:10:33 +02:00
|
|
|
make COQINSTALLPREFIX=%{buildroot} install
|
|
|
|
|
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
%if %{with ide}
|
2019-09-25 11:10:33 +02:00
|
|
|
%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
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
mkdir -p %{buildroot}%{_datadir}/icons/hicolor/256x256/apps
|
|
|
|
|
ln -s %{_datadir}/coq/coq.png %{buildroot}%{_datadir}/icons/hicolor/256x256/apps/coq.png
|
|
|
|
|
%else
|
|
|
|
|
rm %{buildroot}%{_bindir}/coqidetop{,.opt} %{buildroot}%{_mandir}/man1/coqide.1
|
|
|
|
|
%endif
|
2019-09-25 11:10:33 +02:00
|
|
|
|
|
|
|
|
# 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
|
|
|
|
|
|
2020-02-15 20:32:26 +01:00
|
|
|
# Remove unneeded empty *.vos files.
|
|
|
|
|
find %{buildroot}%{_libdir}/coq -empty -name '*.vos' -delete
|
|
|
|
|
|
2019-09-25 11:10:33 +02:00
|
|
|
# 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
|
|
|
|
|
|
2021-09-04 14:54:51 +02:00
|
|
|
# Until we can build it, we fetch the documentation from the official website:
|
|
|
|
|
# svn export https://github.com/coq/doc/trunk/V%{version}/refman
|
|
|
|
|
# svn export https://github.com/coq/doc/trunk/V%{version}/stdlib
|
|
|
|
|
# tar --sort=name --owner=0 --group=0 --mtime="@$(stat -c %%Y refman/index.html)" \
|
|
|
|
|
# --pax-option=exthdr.name=%d/PaxHeaders/%f,delete=atime,delete=ctime \
|
|
|
|
|
# -cJf coq-refman-%{version}.tar.xz refman
|
|
|
|
|
# tar --sort=name --owner=0 --group=0 --mtime="@$(stat -c %%Y stdlib/index.html)" \
|
|
|
|
|
# --pax-option=exthdr.name=%d/PaxHeaders/%f,delete=atime,delete=ctime \
|
|
|
|
|
# -cJf coq-stdlib-%{version}.tar.xz stdlib
|
|
|
|
|
|
|
|
|
|
# Drop some CSS files and headers in stdlib documentation, add some margin directly.
|
|
|
|
|
find stdlib/ -name '*.html' -exec sed -i '
|
|
|
|
|
s#//coq.inria.fr/sites/all/themes/coq/coqdoc.css#/usr/lib64/coq/tools/coqdoc/coqdoc.css#
|
|
|
|
|
/<link type="text\/css" rel="stylesheet" media="all" href="\/\/coq.inria.fr\/.*.css" \/>/d
|
|
|
|
|
/<div id="container">/s/>/ style="margin:1em;">/
|
|
|
|
|
/^ <div id="headertop">$/,/^ <\/div>$/d
|
|
|
|
|
/^ <div id="header">$/,/^ <\/div>$/d
|
|
|
|
|
' {} +
|
|
|
|
|
cp -r refman stdlib %{buildroot}%{_docdir}/coq
|
|
|
|
|
rm -r %{buildroot}%{_docdir}/coq/refman/{.doctrees,_sources}
|
|
|
|
|
|
2019-09-25 11:10:33 +02:00
|
|
|
%files -f runtime.list
|
|
|
|
|
%license LICENSE CREDITS
|
2020-02-15 20:32:26 +01:00
|
|
|
%doc README.md
|
2019-09-25 11:10:33 +02:00
|
|
|
|
|
|
|
|
%{_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
|
2020-08-05 23:55:19 +02:00
|
|
|
%{_bindir}/ocamllibdep
|
2020-02-15 20:32:26 +01:00
|
|
|
%{_bindir}/votour
|
2019-09-25 11:10:33 +02:00
|
|
|
|
|
|
|
|
%dir %{_libdir}/coq
|
|
|
|
|
%{_libdir}/coq/META
|
2020-02-15 20:32:26 +01:00
|
|
|
%{_libdir}/coq/revision
|
2019-09-25 11:10:33 +02:00
|
|
|
%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}
|
|
|
|
|
|
|
|
|
|
%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
|
|
|
|
|
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
%if %{with ide}
|
2019-09-25 11:10:33 +02:00
|
|
|
%files ide
|
|
|
|
|
%{_bindir}/coqide
|
|
|
|
|
%{_bindir}/coqidetop
|
|
|
|
|
%{_bindir}/coqidetop.opt
|
|
|
|
|
%{_mandir}/man1/coqide.1%{ext_man}
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
%{_datadir}/%{name}
|
2019-09-25 11:10:33 +02:00
|
|
|
%{_datadir}/applications/coq.desktop
|
|
|
|
|
%{_datadir}/icons/hicolor/256x256/apps/coq.png
|
|
|
|
|
%{_datadir}/mime/packages/coq.xml
|
Accepting request 870151 from home:aaronpuchert
- Update to version 8.13.0.
* Introduction of primitive persistent arrays in the core
language, implemented using imperative persistent arrays.
* Introduction of definitional proof irrelevance for the equality
type defined in the SProp sort.
* Cumulative record and inductive type declarations can now
specify the variance of their universes.
* Various bugfixes and uniformization of behavior with respect to
the use of implicit arguments and the handling of existential
variables in declarations, unification and tactics.
* New warning for unused variables in catch-all match branches
that match multiple distinct patterns.
* New warning for Hint commands outside sections without a
locality attribute, whose goal is to eventually remove the
fragile default behavior of importing hints only when using
Require. The recommended fix is to declare hints as export,
instead of the current default global, meaning that they are
imported through Require Import only, not Require.
* General support for boolean attributes.
* Many improvements to the handling of notations, including
number notations, recursive notations and notations with
bindings. A new algorithm chooses the most precise notation
available to print an expression, which might introduce changes
in printing behavior.
* Tactic improvements in lia and its zify preprocessing step,
now supporting reasoning on boolean operators such as Z.leb and
supporting primitive integers Int63.
* Typing flags can now be specified per-constant / inductive.
* Improvements to the reference manual including updated syntax
descriptions that match Coq's grammar in several chapters, and
splitting parts of the tactics chapter to independent sections.
- Add build flag to turn off building of the IDE.
OBS-URL: https://build.opensuse.org/request/show/870151
OBS-URL: https://build.opensuse.org/package/show/science/coq?expand=0&rev=26
2021-02-08 00:06:30 +01:00
|
|
|
%{_docdir}/%{name}/FAQ-CoqIde
|
|
|
|
|
%endif
|
2019-09-25 11:10:33 +02:00
|
|
|
|
|
|
|
|
%files devel -f devel.list
|
|
|
|
|
%{_libdir}/coq/tools/CoqMakefile.in
|
|
|
|
|
|
2021-09-04 14:54:51 +02:00
|
|
|
%files doc
|
|
|
|
|
%{_docdir}/coq/refman
|
|
|
|
|
%{_docdir}/coq/stdlib
|
|
|
|
|
|
2019-09-25 11:10:33 +02:00
|
|
|
%changelog
|
