# OPEN-ISSUE: Testsuite does not work due to the absolute paths in configuration.

# The test suite isn't normally run. It can be enabled with "--without=check".
%bcond_with check

# Upstream source information.
%global upstream_owner             AdaCore
%global upstream_name              spark2014
%global upstream_commit_date       20250125
%global upstream_commit            1d27d7cf1e19633390beb92a9ea9f11ba601f773
%global upstream_shortcommit       %(c=%{upstream_commit}; echo ${c:0:7})

%global upstream_name_why3         why3
%global upstream_commit_why3       70ed0a8608a7a605e35ac14fdea723ccdf3e4e6e
%global upstream_shortcommit_why3  %(c=%{upstream_commit_why3}; echo ${c:0:7})

# Major version must match the targeted version SPARK's FSF branch
# (i.e., "fsf-xy"). The minor version is of limited interest as the
# GNAT front-end is rarely updated on a GCC release branch.
%global gcc_version  15.0.1-20250204
%global gcc_sha512   33b9175db47e892b60d9de6d2bbe48b44d7e44ac36f36e08a522cbf020919fe2dc2ef2239fa4c75be63c788fde9725106e64f76663ce1330f984ee3c03fc1ac9

Name:           spark2014
Version:        15.0
Release:        %autorelease
Summary:        Software development technology for engineering high-reliability applications

License:        GPL-3.0-or-later AND LGPL-2.1-only AND LGPL-2.0-only WITH OCaml-LGPL-linking-exception
# The license of the SPARK 2014 tooling is GPLv3+.
# The license of the bundled GNAT compiler code is GPLv3+.
# The license of the bundled Why3 software is LGPLv2.1, except for
# - why3/src/util/extmap.mli : LGPLv2.0 with OCaml LGPL linking exception
# - why3/src/util/extmap.ml  : LGPLv2.0 with OCaml LGPL linking exception
#
# The Why3 IDE depends on the "FatCow" icon set, which is included in the Why3
# source package and licensed separately. However, as the Why3 IDE is not in the
# spark2014 package, the license of the "FatCow" icon set is not mentioned.

URL:            https://www.adacore.com/about-spark
Source0:        https://github.com/%{upstream_owner}/%{upstream_name}/archive/%{upstream_commit}.tar.gz#/%{name}-%{upstream_shortcommit}.tar.gz
Source1:        https://github.com/%{upstream_owner}/%{upstream_name_why3}/archive/%{upstream_commit_why3}.tar.gz#/%{upstream_name_why3}-%{upstream_shortcommit_why3}.tar.gz

# The gnat2why application is partly built with source code from the GNAT front-end.
Source2:        https://src.fedoraproject.org/repo/pkgs/gcc/gcc-%{gcc_version}.tar.xz/sha512/%{gcc_sha512}/gcc-%{gcc_version}.tar.xz

# Build-time configurable version of the SPARK_Install package.
Source3:        spark_install.ads.in

# --- Patches for SPARK and GNATprove.

# [Fedora-specific] Make (search) paths configurable (GNATprove).
Patch0:         %{name}-prep-fix-paths-gnatprove.patch
# [Fedora-specific] Allow additional build options for gnatprove.
Patch1:         %{name}-add-build-options-for-gnatprove.patch
# [Fedora-specific] Colibri solver is not in Fedora.
Patch2:         %{name}-colibri-not-available-for-testing.patch
# [Fedora-specific] Add ppc64le and s390x targets.
Patch3:         %{name}-add-ppc64le-and-s390x-targets.patch
# [Fedora-specific] Switches for Alt-Ergo use a single dash prior to v2.4.0.
#   See also: https://ocamlpro.github.io/alt-ergo/About/changes.html#version-2-4-0-january-22-2021
#             https://github.com/AdaCore/spark2014/commit/155b48d764bc0bfc1f79e980245b0fc36ef71617
Patch4:         %{name}-adapt-for-alt-ergo-free.patch
# [Alt-Ergo] Disable floating-point arithmetic (FPA).
#   See also: https://github.com/OCamlPro/alt-ergo/issues/1111
#             https://github.com/AdaCore/spark2014/commit/18112fd3cdfbe32c5b7acc795b4fd1002bc59276
Patch5:         %{name}-alt-ergo-disable-fpa.patch
# [Fedora-specific] Adapt `install' target in makefile: SPARKlib is a separate package.
Patch6:         %{name}-sparklib-is-separate.patch
# Use `gnatcoll_core.gpr' instead of `gnatcoll.gpr' to reduce dependency closure.
Patch7:         %{name}-refine-dependencies-to-gnatcoll.patch
# Adapt for recent changes in libgpr2 that are not in libgpr2 v25.0.0.
#   Revert commit: "Adjust to libgpr2 API changes for the log system"
#   https://github.com/AdaCore/spark2014/commit/72095b85873f65a8c8f38bc4bbc557f550c0f87f
Patch8:         %{name}-revert-gpr2-reporter-change.patch
# Pagefind (https://pagefind.app/) is not in Fedora (yet). Fallback to
# embedded Sphinx search (see `docs/shared/templates/search.html').
Patch9:         %{name}-pagefind-unavailable.patch

# --- Patches for Why3.

# [Fedora-specific] Make (search) paths configurable (gnatwhy3).
Patch20:        %{name}-why3-prep-fix-paths-gnatwhy3.patch
# [Fedora-specific] Enable verbose make of Why3.
Patch21:        %{name}-why3-enable-verbose-make.patch
# [Fedora-specific] Suppress "warning 70 [missing-mli]".
#   Build fails as the warning-is-error option is enabled on Fedora.
Patch22:        %{name}-why3-fix-missing-mli-error.patch
# [Fedora-specific] Fix incompatible pointer type.
#   GCC warning `-Wincompatible-pointer-types' triggers an error (C23).
Patch23:        %{name}-why3-fix-incompatible-pointer-type.patch
# Adapt for recent changes in OCaml: `effect' is now a keyword.
#   Apply commit: "effect renamed to effekt"
#   https://gitlab.inria.fr/why3/why3/-/commit/deb14b0676f3b247124c77941d4b4b5c374afe19
Patch24:        %{name}-why3-rename-effect-to-effekt.patch
# Fix incorrect merge.
#   https://github.com/AdaCore/why3/compare/cde6ba24c..707fbc43c
Patch25:        %{name}-why3-fix-incorrect-merge.patch

BuildRequires:  gcc-gnat gprbuild autoconf make sed
# A fedora-gnat-project-common that contains GPRbuild_flags is needed.
BuildRequires:  fedora-gnat-project-common >= 3.17
BuildRequires:  libgpr2-devel
# A gnatcoll-core that contains gnatcoll_core.gpr is needed.
BuildRequires:  gnatcoll-core-devel >= 25.0.0
BuildRequires:  zlib-devel
BuildRequires:  coq
# OCaml dependencies as mentioned in `Why3/fsf_build.sh'.
# -- Note: Package `ocaml-seq' not available in Fedora (yet).
BuildRequires:  ocaml-menhir
BuildRequires:  ocaml-ocamlgraph-devel
BuildRequires:  ocaml-num-devel
BuildRequires:  ocaml-re-devel
BuildRequires:  ocaml-yojson-devel
BuildRequires:  ocaml-zarith-devel
BuildRequires:  ocaml-sexplib-devel
BuildRequires:  ocaml-ppx-sexp-conv-devel
BuildRequires:  ocaml-ppx-deriving-devel
BuildRequires:  python3-sphinx
BuildRequires:  python3-sphinx-latex
BuildRequires:  python3-sphinx_rtd_theme
BuildRequires:  latexmk
%if %{with check}
BuildRequires:  python3-devel
BuildRequires:  python3-setuptools
BuildRequires:  python3-e3-testsuite
%endif

# GNATprove uses GPRbuild for providing "incremental analysis" (i.e., analyze
# only those files that changed; see comments and subprogram `Call_Gprbuild' in
# `src/gnatprove/gnatprove.adb').
Requires:       gprbuild

# Require all SAT solvers that are normally used with GNATprove.
Requires:       cvc5, z3, alt-ergo

# Recommend SPARKlib.
Recommends:     sparklib

# Recommend memcached for caching proof results.
Recommends:     memcached

# gnat2why depends on a forked version of Why3. This version is installed in a
# package specific directory in the libexec dir. It is roughly based on Why3
# 1.7.1. Common commit has author date 2024-02-19 10:32:47:
#
# - Inria        : 17bee606014b9131b71c0a779f21013e9b5f849c
# - AdaCore fork : 70704271c9a7b5b76648e0585268ead00aa63034
#
Provides:       bundled(why3)

# gnat2why is build with portions of the GNAT source code. GNAT itself is not
# included (as a binary) and can be installed alongside.
Provides:       bundled(gcc-gnat)

# Alternative names.
Provides:       spark-ada = %{version}
Provides:       gnatprove = %{version}

# Build only on architectures where GPRbuild and the OCaml compiler is
# available. Only pick the most narrow one. If you have two ExclusiveArch
# lines in a spec file, RPM ignores the first one and uses the second one!
# ExclusiveArch:  %{GPRbuild_arches}
ExclusiveArch:  %{ocaml_native_compiler}

%global common_description_en \
SPARK is a software development technology specifically designed for \
engineering high-reliability applications. It consists of a programming \
language, a verification toolset and a design method which, taken \
together, ensure that ultra-low defect software can be deployed in \
application domains where high-reliability must be assured and where \
safety and security are key requirements.

%description %{common_description_en}


#################
## Subpackages ##
#################

%package doc
Summary:        Documentation for SPARK 2014
BuildArch:      noarch
License:        GFDL-1.1-no-invariants-or-later AND MIT AND BSD-2-Clause AND GPL-3.0-or-later
# The license of the documentation itself is GFDL 1.1. Some Javascript and CSS
# files that Sphinx includes with the documentation are BSD 2-Clause and
# MIT-licensed. The examples are licensed under GPL 3.0 or later.

%description doc %{common_description_en}

This package contains the SPARK user's guide and SPARK 2014 language reference
manual in HTML and PDF format, and some examples.


#############
## Prepare ##
#############

%prep
%setup -q -n %{upstream_name}-%{upstream_commit}

# Replace the Why3 git submodule placeholder with the downloaded sources.
rmdir why3
tar --extract --gzip --file %{SOURCE1}
mv %{upstream_name_why3}-%{upstream_commit_why3} why3

# Extract the GNAT sources from the GCC source tarball. Create a symbolic link
# that points to these GNAT sources.
tar --extract --xz --file %{SOURCE2} gcc-%{gcc_version}/gcc/ada
ln --symbolic ../gcc-%{gcc_version}/gcc/ada gnat2why/gnat_src

# All sources have been setup, we can now start patching.

# Apply patches to SPARK and GNATprove.
%patch 0 -p1
%patch 1 -p1
%patch 2 -p1
%patch 3 -p1
%patch 4 -p1
%patch 5 -p1
%patch 6 -p1
%patch 7 -p1
%patch 8 -p1
%patch 9 -p1

# Apply patches to Why3.
%patch 20 -p1
%patch 21 -p1
%patch 22 -p1
%patch 23 -p1
%patch 24 -p1
#%patch 25 -p1

# Patch hard-coded (relative) paths in the source code of gnatprove.
# -- Note: Depends on the application of patch 0.
sed --expression='s,@PREFIX@,%{_prefix},'               \
    --expression='s,@LIBDIR@,%{_libdir},'               \
    --expression='s,@LIBEXECDIR@,%{_libexecdir},'       \
    --expression='s,@DATADIR@,%{_datadir},'             \
    --expression='s,@GNATPRJDIR@,%{_GNAT_project_dir},' \
    --expression='s,@NAME@,%{name},'                    \
    %{SOURCE3} > ./src/gnatprove/spark_install.ads

# Patch hard-coded (relative) paths in the source code of gnatwhy.
# -- Note: Depends on the application of patch 20.
sed --in-place \
    --expression='s,@LIBEXECDIR@,%{_libexecdir},' \
    --expression='s,@DATADIR@,%{_datadir},'       \
    --expression='s,@NAME@,%{name},'              \
    ./why3/src/gnat/gnat_util.ml

# Rename license file of Why3 to prevent collision when included later.
mv why3/LICENSE why3/LICENSE-why3

# From Fedora package `Why3':
#
# Use the correct compiler flags, keep timestamps, and harden the build due to
# network use.  Link the binaries with runtime compiled with -fPIC.
# This avoids many link-time errors.
sed -e "s|-Wall|%{build_cflags}|;s/ -O -g//" \
    -e "s/cp /cp -p /" \
    -e "s|^OLINKFLAGS =.*|& -runtime-variant _pic -ccopt \"%{build_ldflags}\"|" \
    -i why3/Makefile.in


###########
## Build ##
###########

%build

make setup
%{make_build} VERSION=%{version} \
              GPRBUILD='gprbuild %{GPRbuild_flags} -cargs -fPIE -gargs'

# Build the documentation.
make doc VERSION=%{version}


#############
## Install ##
#############

%install

# Make will install all files under a subdirectory `install' located in
# builddir. Patching all files (including some GPRbuild files) seems too
# cumbersone so we'll move everything into the correct place afterwards.
make install-all
make install-examples

# Move SPARK toolset + Why3 to the buildroot.
mkdir --parents \
      %{buildroot}%{_datadir}/%{name}        \
      %{buildroot}%{_libexecdir}/%{name}     \
      %{buildroot}%{_bindir}                 \
      %{buildroot}%{_libexecdir}/%{name}/bin \

mv ./install/share/spark/*   %{buildroot}%{_datadir}/%{name}
mv ./install/libexec/spark/* %{buildroot}%{_libexecdir}/%{name}
mv ./install/bin/gnatprove   %{buildroot}%{_bindir}
mv ./install/bin/*           %{buildroot}%{_libexecdir}/%{name}/bin

# Move all docs and examples to the buildroot.
mkdir --parents \
      %{buildroot}%{_pkgdocdir} \
      %{buildroot}%{_pkgdocdir}/examples

mv ./install/share/doc/spark/*      %{buildroot}%{_pkgdocdir}
mv ./install/share/examples/spark/* %{buildroot}%{_pkgdocdir}/examples

# Make all OCaml plugins executable to have them stripped after the build.
find %{buildroot}%{_libexecdir}/%{name} -name "*.cmxs" -exec chmod 755 {} \;

# Remove the fake prover scripts that are only used for benchmarking.
rm %{buildroot}%{_libexecdir}/%{name}/bin/fake*

# Remove duplicate Why3 commands. Why3 is build with configuration option
# --enable-relocatable which will fix `localdir' to `None' in
# `src/config.sh.in'. The Why3 executable (`src/tools/main.ml') will, as a
# result, search for commands in `../lib/why3/commands' relative to itself
# (see also output of `why3 --print-libdir').
rm %{buildroot}%{_libexecdir}/%{name}/bin/why3*.cmxs

# Remove executables that should only be in `libexec/spark2014/bin'. These are
# duplicate files because they are copied instead of moved in make target
# `install_spark2014' (see `why3/Makefile.in').
rm %{buildroot}%{_libexecdir}/%{name}/lib/why3/why3server
rm %{buildroot}%{_libexecdir}/%{name}/lib/why3/why3cpulimit

# Remove script to detect and/or invoke PVS. The version of Why3 in this package
# is build without PVS support and GNATprove doesn't support it. This script is
# only referenced in `provers-detection-data.conf'.
rm %{buildroot}%{_libexecdir}/%{name}/lib/why3/why3-call-pvs

# Remove resource files for the Why3 IDE. The IDE is not included in this
# package, but the resource files are copied unconditionally in make target
# `install_spark2014_dev' (see `why3/Makefile.in').
rm --recursive %{buildroot}%{_libexecdir}/%{name}/share/why3/images
rm --recursive %{buildroot}%{_libexecdir}/%{name}/share/why3/lang

# Show installed files (to ease debugging based on build server logs).
find ./install    -exec stat --format "%A %n" {} \;
find %{buildroot} -exec stat --format "%A %n" {} \;


###########
## Check ##
###########

%if %{with check}
%check

# Make the files installed in the buildroot visible to the testsuite.
export PATH=%{buildroot}%{_bindir}:$PATH
export LD_LIBRARY_PATH=%{buildroot}%{_libdir}:$LD_LIBRARY_PATH
export PYTHONPATH=%{buildroot}%{python3_sitearch}:%{buildroot}%{python3_sitelib}:$PYTHONPATH

# Use a file-based cache for sharing proof results between tests.
%global cachedir '%{_builddir}/%{upstream_name}-%{upstream_commit}/testsuite/result_cache'

mkdir --parents %{cachedir}
export GNATPROVE_CACHE='file:%{cachedir}'

# Run the tests.
%python3 testsuite/gnatprove/run-tests \
         --show-error-output \
         --max-consecutive-failures=8 \
         --cache

%endif


###########
## Files ##
###########

%files
%license LICENSE why3/LICENSE-why3
%doc README*

%{_bindir}/gnatprove
%{_libexecdir}/%{name}
%{_datadir}/%{name}


%files doc
%dir %{_pkgdocdir}
%{_pkgdocdir}/html
%{_pkgdocdir}/pdf
%{_pkgdocdir}/examples
# Remove Sphinx-generated files that aren't needed in the package.
%exclude %{_pkgdocdir}/html/ug/objects.inv
%exclude %{_pkgdocdir}/html/lrm/objects.inv


###############
## Changelog ##
###############

%changelog
%autochangelog