diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | python-gym-saturation.spec | 126 | ||||
| -rw-r--r-- | sources | 1 |
3 files changed, 128 insertions, 0 deletions
@@ -0,0 +1 @@ +/gym_saturation-0.10.0.tar.gz diff --git a/python-gym-saturation.spec b/python-gym-saturation.spec new file mode 100644 index 0000000..9819914 --- /dev/null +++ b/python-gym-saturation.spec @@ -0,0 +1,126 @@ +%global _empty_manifest_terminate_build 0 +Name: python-gym-saturation +Version: 0.10.0 +Release: 1 +Summary: Gymnasium environments for saturation provers +License: Apache-2.0 +URL: https://github.com/inpefess/gym-saturation +Source0: https://mirrors.nju.edu.cn/pypi/web/packages/12/7e/ff39887e7157841a3b0e73e2a128b0de572b82fe7fe364c1dfefec493f5b/gym_saturation-0.10.0.tar.gz +BuildArch: noarch + +Requires: python3-importlib_resources +Requires: python3-pexpect +Requires: python3-gymnasium + +%description +``gym-saturation`` is a collection of `Gymnasium +<https://gymnasium.farama.org/>`__ environments for reinforcement learning +(RL) agents striving to prove theorems. Currently, only theorems +written in `TPTP library <https://tptp.org>`__ formal language are +supported. +There are two environments in ``gym-saturation`` following the same API: `SaturationEnv <https://gym-saturation.readthedocs.io/en/latest/environments/saturation-env.html>`__: ``VampireEnv`` is a wrapper around a recent `Vampire +<https://github.com/vprover/vampire>`__ prover, and ``IProverEnv`` +relies on a stable version of `iProver +<https://gitlab.com/korovin/iprover/>`__. +In contrast to monolithic architecture of a typical Automated Theorem +Prover (ATP), ``gym-saturation`` gives different agents opportunities +to select clauses themselves and train from their experience. +Combined with a particular agent, ``gym-saturation`` can work as an +ATP. +``gym-saturation`` can be interesting for RL practitioners willing to +apply their experience to theorem proving without coding all the +logic-related stuff themselves. It also can be useful for automated +deduction researchers who want to create an RL-empowered ATP. + +%package -n python3-gym-saturation +Summary: Gymnasium environments for saturation provers +Provides: python-gym-saturation +BuildRequires: python3-devel +BuildRequires: python3-setuptools +BuildRequires: python3-pip +%description -n python3-gym-saturation +``gym-saturation`` is a collection of `Gymnasium +<https://gymnasium.farama.org/>`__ environments for reinforcement learning +(RL) agents striving to prove theorems. Currently, only theorems +written in `TPTP library <https://tptp.org>`__ formal language are +supported. +There are two environments in ``gym-saturation`` following the same API: `SaturationEnv <https://gym-saturation.readthedocs.io/en/latest/environments/saturation-env.html>`__: ``VampireEnv`` is a wrapper around a recent `Vampire +<https://github.com/vprover/vampire>`__ prover, and ``IProverEnv`` +relies on a stable version of `iProver +<https://gitlab.com/korovin/iprover/>`__. +In contrast to monolithic architecture of a typical Automated Theorem +Prover (ATP), ``gym-saturation`` gives different agents opportunities +to select clauses themselves and train from their experience. +Combined with a particular agent, ``gym-saturation`` can work as an +ATP. +``gym-saturation`` can be interesting for RL practitioners willing to +apply their experience to theorem proving without coding all the +logic-related stuff themselves. It also can be useful for automated +deduction researchers who want to create an RL-empowered ATP. + +%package help +Summary: Development documents and examples for gym-saturation +Provides: python3-gym-saturation-doc +%description help +``gym-saturation`` is a collection of `Gymnasium +<https://gymnasium.farama.org/>`__ environments for reinforcement learning +(RL) agents striving to prove theorems. Currently, only theorems +written in `TPTP library <https://tptp.org>`__ formal language are +supported. +There are two environments in ``gym-saturation`` following the same API: `SaturationEnv <https://gym-saturation.readthedocs.io/en/latest/environments/saturation-env.html>`__: ``VampireEnv`` is a wrapper around a recent `Vampire +<https://github.com/vprover/vampire>`__ prover, and ``IProverEnv`` +relies on a stable version of `iProver +<https://gitlab.com/korovin/iprover/>`__. +In contrast to monolithic architecture of a typical Automated Theorem +Prover (ATP), ``gym-saturation`` gives different agents opportunities +to select clauses themselves and train from their experience. +Combined with a particular agent, ``gym-saturation`` can work as an +ATP. +``gym-saturation`` can be interesting for RL practitioners willing to +apply their experience to theorem proving without coding all the +logic-related stuff themselves. It also can be useful for automated +deduction researchers who want to create an RL-empowered ATP. + +%prep +%autosetup -n gym-saturation-0.10.0 + +%build +%py3_build + +%install +%py3_install +install -d -m755 %{buildroot}/%{_pkgdocdir} +if [ -d doc ]; then cp -arf doc %{buildroot}/%{_pkgdocdir}; fi +if [ -d docs ]; then cp -arf docs %{buildroot}/%{_pkgdocdir}; fi +if [ -d example ]; then cp -arf example %{buildroot}/%{_pkgdocdir}; fi +if [ -d examples ]; then cp -arf examples %{buildroot}/%{_pkgdocdir}; fi +pushd %{buildroot} +if [ -d usr/lib ]; then + find usr/lib -type f -printf "/%h/%f\n" >> filelist.lst +fi +if [ -d usr/lib64 ]; then + find usr/lib64 -type f -printf "/%h/%f\n" >> filelist.lst +fi +if [ -d usr/bin ]; then + find usr/bin -type f -printf "/%h/%f\n" >> filelist.lst +fi +if [ -d usr/sbin ]; then + find usr/sbin -type f -printf "/%h/%f\n" >> filelist.lst +fi +touch doclist.lst +if [ -d usr/share/man ]; then + find usr/share/man -type f -printf "/%h/%f.gz\n" >> doclist.lst +fi +popd +mv %{buildroot}/filelist.lst . +mv %{buildroot}/doclist.lst . + +%files -n python3-gym-saturation -f filelist.lst +%dir %{python3_sitelib}/* + +%files help -f doclist.lst +%{_docdir}/* + +%changelog +* Wed May 17 2023 Python_Bot <Python_Bot@openeuler.org> - 0.10.0-1 +- Package Spec generated @@ -0,0 +1 @@ +8cb7eb4e7483dba17a97c8f24b01e434 gym_saturation-0.10.0.tar.gz |