File ocaml-coq.spec of Package ocaml-coq

#
# spec file for package ocaml-coq
#
# Copyright (c) 2025 SUSE LLC
#
# 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:           ocaml-coq
Version:        9.0.0
Release:        0
Summary:        Formal proof management system
License:        LGPL-2.1-only WITH OCaml-LGPL-linking-exception
Group:          System/Packages
URL:            https://opam.ocaml.org/packages/coq
Source0:        %name-%version.tar.xz
Patch0:         %name.patch
Obsoletes:      coq
BuildRequires:  ocaml(ocaml_base_version) >= 4.09
BuildRequires:  ocaml-dune >= 3.6
BuildRequires:  ocaml-rpm-macros >= 20240909
BuildRequires:  ocamlfind(cairo2)
BuildRequires:  ocamlfind(compiler-libs)
BuildRequires:  ocamlfind(dynlink)
BuildRequires:  ocamlfind(findlib)
BuildRequires:  ocamlfind(lablgtk3-sourceview3)
BuildRequires:  ocamlfind(str)
BuildRequires:  ocamlfind(threads)
BuildRequires:  ocamlfind(unix)
BuildRequires:  ocamlfind(zarith)

%description
The Coq proof assistant provides a formal language to write mathematical definitions, executable algorithms, and theorems, together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g., the CompCert compiler certification project and the Bedrock verified low-level programming library), the formalization of mathematics (e.g., the full formalization of the Feit-Thompson theorem and homotopy type theory) and teaching.

%package        devel
Summary:        Development files for %name
Group:          Development/Languages/OCaml
Requires:       %name = %version
Obsoletes:      coq-devel

%description    devel
The %name-devel package contains libraries and signature files for
developing applications that use %name.

%prep
%autosetup -p1

%build
mv -f theories/dune.disabled theories/dune
mv -f user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
dune_release_pkgs='coq,coq-core,coqide-server,rocq-core,rocq-prover,rocq-runtime,rocqide'
%ocaml_dune_setup
%ocaml_dune_build

%install
%ocaml_dune_install
%ocaml_create_file_list
if test -d %buildroot%ocaml_standard_library/coq-core/dev/ml_toplevel
then
	echo '%ocaml_standard_library/coq-core/dev/ml_toplevel' >> %name.files
fi
if test -d %buildroot%ocaml_standard_library/rocq-runtime/dev/ml_toplevel
then
	echo '%ocaml_standard_library/rocq-runtime/dev/ml_toplevel' >> %name.files
fi
if test -d %buildroot%ocaml_standard_library/rocq-runtime
then
	tee %buildroot%ocaml_standard_library/rocq-runtime/revision <<_EOF_
%_project/%_repository
%version
_EOF_
fi

%files -f %name.files
%_bindir/*
%_mandir/*/*
%_datadir/coq
%_datadir/texmf
%ocaml_standard_library/rocq-runtime/revision
%ocaml_standard_library/rocq-runtime/rocqnative
%ocaml_standard_library/rocq-runtime/rocqworker
%ocaml_standard_library/rocq-runtime/rocqworker.byte
%ocaml_standard_library/rocq-runtime/rocqworker_with_drop
%ocaml_standard_library/rocq-runtime/tools

%files devel -f %name.files.devel

%changelog